Wikipedia says that lambda calculus is a formal system. It defines lambda calculus by giving its alphabet, and inductively describing what is inside its formal language.
Since lambda calculus is a formal system, what are its
Does lambda calculus have semantics? If yes, how does an interpretation of lambda calculus look like as a mapping from what subset to another?
First of all, note that the notion of a formal system is an informal notion and there is no general (or generally accepted), formal definition of what a formal system is. In my opinion, the Wikipedia article on formal systems does not do a good job at explaining this and creates the illusion that formal systems are more or less the same as (the syntactic part) of logical systems, axiomatic systems, or proof systems, etc. Personally, I would rather go with the intuition given by the link at the bottom of the article, that leads to the following quote from John Haugeland's Artificial Intelligence: The Very Idea (1985), pp. 48-64.
A formal system is like a game in which tokens are manipulated according to rules in order to see what configurations can be obtained. (Examples: chess, checkers, go, tic-tac-toe. Nonexamples: marbles, billiards, baseball). All formal games have three essential features:
- They are token manipulation games;
- they are digital; and
- they are finitely playable.
where
A digital system is a set of positive and reliable techniques (methods, devices) for producing and reidentifying tokens, or configurations of tokens, from some prespecified set of types.
From this perspective, it is much easier to see lambda calculus as a formal system:
If you want to reconcile this with the Wikipedia definition of the topic, you could consider the reduction rules to be the inference rules and the set of axioms to be empty.
Another way to look at it, is by considering the equational theory of the $\lambda$-calculus, which would look something like
It is easy to show that $t =_\beta s$ (i.e. $t$ $\beta$-reduces to $s$) if and only if $t=s$ can be proved using the axioms and rules above. Using this system, it also makes sense, for example, to ask the usual "logical" question of consistency: Are there terms $s$ and $t$ for which we can not prove $s=t$.
Regarding the question of semantics, you can use the reduction rules in order to give $\lambda$-calculus operational semantics and there are also denotational semantics see Dana Scott's Data Types as Lattices For the latter, it might be easier to go via combinator algebras, see Engelers Algebras and Combinators. On a side note, this article on architectures for interpreters gives a good idea of what denotational and (small-step and big-step) operational semantics mean in this context.
In general, these questions are, however, quite hard and it might be better to first consider the simply typed $\lambda$-calculus as a starting point. Here, it is (somewhat) easy to see that it actually is a logic via the Curry-Howard correspondence. You will also find a nice answer to the question of semantics in this simple case. From the simply typed $\lambda$-calculus you can go on to consider more complicated systems in the lambda cube or things like homotopy type theory.
Also, maybe the discussion Is lambda calculus a logic? in the Lambda the Ultimate forum might also provide further insights.
Finally, this might be slightly off-topic, but if you really want to go deep down into the rabbit hole of $\lambda$-calculus, logic, and semantics, Girard's Proofs and Types and The Blind Spot might be worth a look.
This may depends on the context, as there is not a single logic based on lambda calculus. Ex. two of the most famous are Higher Order Logic and Calculus of Constructions.
An axiom is a starting point taken for granted. An inference rule is a rule by which, from an (or multiple) axiom/theorem/lemma, you can produce a new theorem or lemma, which is a proven axiom (otherwise an axiom may be supposed valid, while not proven to be so… an axiom is a starting point).
From that follows the axioms of lambda‑calculus are the syntactic rules (there also are “syntactic proofs”) and interpretations of formulas (note interpretations may vary, depending on the context) and inference rules are the rewriting and transformation rules, ex. application, abstraction, substitution, beta‑reduction and some others. Also note inference rules, are just special kind of axioms.
According to Introduction to Lambda Calculus [pdf] (Henk Barendregt, Erik Barendsen), the axiom of substitution, is the only required axiom (an inference rule is often taken for an axiom in the logician world).
For the semantics, it depends on the interpretation: denotational semantic and operational semantic, are both valid options, while two different enough options.
I'm posting this so that you at least get an answer, but please, note you can expect a better answer than mine, as I'm not a lambda‑calculus guru.
Worth reading too:
A nominal axiomatisation of the lambda-calculus [pdf] (Murdoch J. Gabbay, Aad Mathijssen)
Abstract
The lambda-calculus is fundamental in computer science. It resists an algebraic treatment because of capture-avoidance side-conditions.
Nominal algebra is a logic of equality designed for specifications involving binding. We axiomatise the lambda-calculus using nominal algebra, demonstrate how proofs with these axioms reflect the informal arguments on syntax, and we prove the axioms sound and complete. We consider both non-extensional and extensional versions (alpha-beta and alpha-beta-eta equivalence) […]
Worth to be noted in this context, to avoid confusion: the lambda calculus on it's own, is not a valid deductive system, and this is demonstrated by the existence of a function named the fixed‑point combinator [1], which introduce a paradox of one of the most common type: self‑referential paradox. However, some part of it, or at least of some kind of lambda‑calculus, may be sound. Ex. the type system of at least SML (I don't know for other concrete system of lambda‑calculus) is sound. In this example context, providing types are assigned an interpretation (which is straight‑forward with the Curry‑Howard isomorphism where a type is a logical proposition), the type system (if I understand correctly), is a sound deductive system. As an example, HOL systems (the proof checkers and proof assistants family, not the logic of the same name they are based on), rely on SML's type system to formally ensure the validity of the inferences sequence they check.
[1] As a reminder, the fixed‑point combinator is the function of this canonical form (there are other way to express it though):
val rec fix = fn f => (fn x => (f (fix f)) x)
Or more succinctly:
fun fix f x = f (fix f) x
