patternCritical
How does the Y combinator exemplify "Lambda calculus inconsistency"?
Viewed 0 times
thecalculuscombinatorinconsistencydoeshowexemplifylambda
Problem
On the Wikipedia page for Fixed Point Combinators is written the rather mysterious text
The Y combinator is an example of what makes the Lambda calculus inconsistent. So it should be regarded with suspicion. However it is safe to consider the Y combinator when defined in mathematic logic only.
Have I entered into some sort of spy novel? What in the world is meant by the statements that $\lambda$-calculus is "inconsistent" and that it should be "regarded with suspicion"?
The Y combinator is an example of what makes the Lambda calculus inconsistent. So it should be regarded with suspicion. However it is safe to consider the Y combinator when defined in mathematic logic only.
Have I entered into some sort of spy novel? What in the world is meant by the statements that $\lambda$-calculus is "inconsistent" and that it should be "regarded with suspicion"?
Solution
It's inspired from real events, but the way it's stated is barely recognizable and “should be regarded with suspicion” is nonsense.
Consistency has a precise meaning in logic: a consistent theory is one where not all statements can be proved. In classical logic, this is equivalent to the absence of a contradiction, i.e. a theory is inconsistent if and only if there is a statement $A$ such that the theory proves both $A$ and its negation $\neg A$.
So what does this mean regarding the lambda calculus? Nothing. The lambda calculus is a rewriting system, not a logical theory.
It is possible to view the lambda calculus in relation to logic. Regard variables as representing a hypothesis in a proof, lambda abstractions as proofs under a certain hypothesis (represented by the variable), and application as putting together a conditional proof and proof of the hypothesis. Then the beta rule corresponds to simplifying a proof by applying modus ponens, a fundamental principle of logic.
This, however, only works if the conditional proof is combined with a proof of the right hypothesis. If you have a conditional proof that assumes $n=3$ and you also have a proof of $n=2$, you can't combine them together. If you want to make this interpretation of the lambda calculus work, you need to add a constraint that only proofs of the proper hypothesis get applied to conditional proofs. This is called a type system, and the constraint is the typing rule that says that when you pass an argument to a function, the type of the argument must match the parameter type of the function.
The Curry-Howard correspondence is a parallel between typed calculi and proof systems.
A typed calculus that has a fixed point combinator such as $Y$ allows building a term of any type (try evaluating $Y (\lambda x.x)$), so if you take the logical interpretation through the Curry-Howard correspondence, you get an inconsistent theory. See Does the Y combinator contradict the Curry-Howard correspondence? for more details.
This is not meaningful for the pure lambda calculus, i.e. for the lambda calculus without types.
In many typed calculi, it's impossible to define a fixed point combinator. Those typed calculi are useful with respect to their logical interpretation, but not as a basis for a Turing-complete programming language. In some typed calculi, it's possible to define a fixed point combinator. Those typed calculi are useful as a basis for a Turing-complete programming language, but not with respect to their logical interpretation.
In conclusion:
Consistency has a precise meaning in logic: a consistent theory is one where not all statements can be proved. In classical logic, this is equivalent to the absence of a contradiction, i.e. a theory is inconsistent if and only if there is a statement $A$ such that the theory proves both $A$ and its negation $\neg A$.
So what does this mean regarding the lambda calculus? Nothing. The lambda calculus is a rewriting system, not a logical theory.
It is possible to view the lambda calculus in relation to logic. Regard variables as representing a hypothesis in a proof, lambda abstractions as proofs under a certain hypothesis (represented by the variable), and application as putting together a conditional proof and proof of the hypothesis. Then the beta rule corresponds to simplifying a proof by applying modus ponens, a fundamental principle of logic.
This, however, only works if the conditional proof is combined with a proof of the right hypothesis. If you have a conditional proof that assumes $n=3$ and you also have a proof of $n=2$, you can't combine them together. If you want to make this interpretation of the lambda calculus work, you need to add a constraint that only proofs of the proper hypothesis get applied to conditional proofs. This is called a type system, and the constraint is the typing rule that says that when you pass an argument to a function, the type of the argument must match the parameter type of the function.
The Curry-Howard correspondence is a parallel between typed calculi and proof systems.
- types correspond to logical statements;
- terms correspond to proofs;
- inhabited types (i.e. types such that there is a term of that type) correspond to true statements (i.e. statements such that there is a proof of that statement);
- program evaluation (i.e. rules such as beta) correspond to transformations of proofs (which had better transform correct proofs into correct proofs).
A typed calculus that has a fixed point combinator such as $Y$ allows building a term of any type (try evaluating $Y (\lambda x.x)$), so if you take the logical interpretation through the Curry-Howard correspondence, you get an inconsistent theory. See Does the Y combinator contradict the Curry-Howard correspondence? for more details.
This is not meaningful for the pure lambda calculus, i.e. for the lambda calculus without types.
In many typed calculi, it's impossible to define a fixed point combinator. Those typed calculi are useful with respect to their logical interpretation, but not as a basis for a Turing-complete programming language. In some typed calculi, it's possible to define a fixed point combinator. Those typed calculi are useful as a basis for a Turing-complete programming language, but not with respect to their logical interpretation.
In conclusion:
- The lambda calculus is not “inconsistent”, that concept does not apply.
- A typed lambda calculus that assigns a type to every lambda term is inconsistent. Some typed lambda calculi are like that, others make some terms untypable and are consistent.
- Typed lambda calculi are not the sole raison d'être for the lambda calculus, and even inconsistent typed lambda calculi are very useful tools — just not to prove things.
Context
StackExchange Computer Science Q#83178, answer score: 53
Revisions (0)
No revisions yet.