44
$\begingroup$

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"?

$\endgroup$
52
$\begingroup$

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.

  • 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.
$\endgroup$
  • 2
    $\begingroup$ Wow, there is a lot for me to unpack here. Thanks for the detailed explanation. It's going to take me some time to try to grok it all. $\endgroup$ – Ben I. Oct 29 '17 at 22:38
  • 4
    $\begingroup$ Technically, viewing untyped as unityped, you can make a CH correspondence between the untyped lambda calculus and a logic. It's just a very, very boring (and certainly inconsistent) logic. Proof assistants like NuPRL muddy the waters a bit. The object language of NuPRL contains the untyped lambda calculus, and you can readily define the Y combinator. NuPRL splits things a bit differently so it has a type refinement system rather than a type system, and the exercise isn't to produce well-typed terms but to produce the typing derivations. $\endgroup$ – Derek Elkins Oct 30 '17 at 1:58
  • $\begingroup$ Is it just me, or is it weird to impose the "propositions as types" paradigm on untyped lambda calculus? I've always seen people talk about logic in untyped lambda calculus by introducing specific objects to be the boolean values true and false, and propositions were things that had boolean valued output. (and were only considered propositions on the domain of things where it does output a boolean value). $\endgroup$ – user5386 Oct 30 '17 at 4:38
  • $\begingroup$ Trivial(proves every statement) and contains contradictions are two different properties. While they are equivalent in classical logic, for paraconsistent logics a system can be inconsistent and non-trivial. $\endgroup$ – Taemyr Oct 30 '17 at 9:31
  • 1
    $\begingroup$ "Inconsistent", for a λ-calculus-based logic, means "assigns every type to some term", not "assigns a type to every term" (although the former follows from the latter); there are plenty of λ-calculus-based languages which correspond to inconsistent logics but where not every λ-calculus term is typeable. $\endgroup$ – Jonathan Cast Oct 30 '17 at 14:51
6
$\begingroup$

I'd like to add one to what @Giles said.

The Curry-Howard correspondence makes a parallel between $\lambda$-terms (more specifically, the types of $\lambda$-terms) and proof systems.

For example, $\lambda x.\lambda y.x$ has type $a \to (b \to a)$ (where $a \to b$ means "function from $a$ to $b$"), which corresponds to the logical statement $a \implies (b \implies a)$. The function $\lambda x.\lambda y.xy$ has type $(a \to b) \to (a \to b)$, corresponding to $(a \implies b) \implies (a \implies b)$. We can convert any lambda-calculus type to a logical tautology by, in a sense, "pattern matching" on functions.

The problem arises when we consider the Y combinator, defined as $\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$. The issue arises because we expect the Y combinator, as a "fix-point" combinator, to have type $(a \to a) \to a$ (because it takes a function from a type to that same type, and finds a fixed-point for that function, which has that type). Converting this to a logical statement yields $(a \implies a) \implies a$. This is a contradiction:

$$(a \implies a) \implies a \\ \top \implies a \\ a \\(\neg a \implies \neg a) \implies (\neg a) \\ \top \implies \neg a \\ \neg a$$

Accepting $(a \to a) \to a$ in a type system leads to the type system being inconsistent. This means we can either

  • Disallow types like $(a \to a) \to a$ in a type system (this gives you the Simply typed $\lambda$-calculus), or
  • Live with the type system being inconsistent as a system of logical deduction.
$\endgroup$
  • 1
    $\begingroup$ CH relates types to propositions, programs to proofs, and even reductions to proof transformations. It is not just about types. Next, only inhabited types correspond to tautologies. $\forall a, b.a\to b$ is a (polymorphic) lambda calculus type even if no terms inhabit it. Assuming you mean types like $\forall a.(a\to a) \to a$, then accepting such types is perfectly fine, the issue is whether that type has an inhabitant or not. Conversely, we can add primitive terms to the STLC that will make the corresponding logic inconsistent without extending the type system. $\endgroup$ – Derek Elkins Nov 22 '17 at 22:13
  • $\begingroup$ @DerekElkins, what kind of primitive terms? Also, if I understand correctly, this is just to assume (a -> a) -> a is always inhabited which produce the inconsistency? So there is no more inconsistency with a programming language which requires a termination proof? Or is there any other source of inconsistency in untyped or Hindley‑Milner typed lambda calculus? $\endgroup$ – Hibou57 Mar 27 at 15:53
  • 1
    $\begingroup$ @Hibou57 Primitive terms, i.e. constants, like fix. You can just assert that there is a constant $\mathsf{fix}_A$ for each type $A$. That will already give you an inconsistent system as far as CH is concerned, as it would imply every type is inhabited by $\mathsf{fix}(\lambda x.x)$. You could additionally add $\delta$-rules to make $\mathsf{fix}$ compute, and that would turn, say, the STLC with naturals into a Turing-complete system, but you don't have to add these computational rules, and the system would still be inconsistent. $\endgroup$ – Derek Elkins Mar 28 at 5:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.