patternMinor
What are the axioms, inference rules, and (formal) semantics of lambda calculus?
Viewed 0 times
thewhatsemanticsareformalcalculusandinferenceaxiomsrules
Problem
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?
-
Since lambda calculus is a formal system, what are its
- axioms and
- inference rules?
-
Does lambda calculus have semantics? If yes, how does an interpretation of lambda calculus look like as a mapping from what subset to another?
Solution
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:
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
$$\qquad \frac{s=t}{t=s} \qquad \frac{s=t \quad t=u}{s=u}$$
$$
\frac{s=s^\prime\quad t=t^\prime}{st = s^\prime t^\prime} \quad \frac{s=t}{\lambda x.s = \lambda x.t}
$$
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.
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:
- the tokens are lambda expressions
- the reduction rules provide the techniques as required per the "digital 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
- Axiom: reflexivity $$\frac{}{s=s}$$
- Rules: symmetry and transitivity
$$\qquad \frac{s=t}{t=s} \qquad \frac{s=t \quad t=u}{s=u}$$
- Rules: application and abstraction
$$
\frac{s=s^\prime\quad t=t^\prime}{st = s^\prime t^\prime} \quad \frac{s=t}{\lambda x.s = \lambda x.t}
$$
- Axiom: $\beta$-conversion $$\frac{}{(\lambda x.s)t=s[t/x]}$$
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.
Context
StackExchange Computer Science Q#28452, answer score: 9
Revisions (0)
No revisions yet.