[Prev][Next][Index][Thread]
Re: Hilbert systems vs. Gentzen systems
[------- The Types Forum ------ http://www.cs.indiana.edu/types -------]
> From Healfdene Goguen:
> * Meta-properties, such as the deduction theorem, are commonly
> brought into the object language. This is more serious since Curry's
> abstraction doesn't satisfy the xi rule which allows equality
> underneath abstraction.
> From Thorsten Altenkirch:
>
> One important difference between combinatory logic (i.e. Hilbert
> systems) and lambda calculus (here Gentzen systems) is that the first
> is "algebraic", whereas the second is not. In particular the models of
> combinatory logic are closed under submodels which is not the case for
> lambda calculus. E.g. the closed terms of combinatory logic (the
> "interior") form a combinatory algebra which is not the case for
> lambda calculus (the closed terms are just a combinatory algebra).
>
> This is discussed in Hindley's & Seldin's "Introduction to Combinators
> and lambda calculus", pp. 107 for the untyped case but it is easy to
> see that it applies to typed calculi as well.
There is a point to be considered here that is often overlooked. In a
certain, strong, sense, the lambda calculus actually *is* algebraic.
The failure of the above properties (Curry's abstraction does not
satisfy the xi-rule; lambda calculus models are not closed under
submodels) comes from the notion of model considered, and not from the
lambda calculus itself. It is my impression that this has been known to
a few people for a long time, but since this point is missing from some
standard texts (including Hindley and Seldin's book and also
Barendregt's book), it is still relatively obscure.
What I mean is the following: Let A be a lambda algebra (i.e. a
combinatorial algebra satisfying the additional 4 or 5 Curry axioms).
There are two different styles of defining what it means for M=N to hold
in A, where M,N are open (lambda or combinatory) terms: M=N holds
'locally' iff it holds for all substitutions of elements of A for the
free variables, and it holds 'absolutely' iff it holds in A[x_1...x_n],
i.e. in the lambda algebra obtained from A by freely adjoining
indeterminates x_1...x_n (assuming the free variables of M and N are
contained in this set).
It should not be surprising that these interpretations are strictly
different. All the rules of the lambda calculus, including the xi rule,
are sound for the 'absolute' interpretation. (But not for the 'local'
interpretation: here the non-equational class of "lambda models" is
needed). As a consequence, the class of lambda algebras is not only
sound and complete *for arbitrary lambda theories*, but the theories of
lambda algebras and the lambda calculus become the same, in the sense
that the categories of their respective theories are equivalent.
This interpretation (for the beta-eta case) can be found in Lambek's
paper "From lambda calculus to cartesian closed categories". In the
typ
References: