Computing alpha-equality in pure lambda calculus
Klaus Ostermann
pure lambda calculus has no equality operator in order to compare
values. I know that for special cases like church integers it is possible
to "compute" whether two functions represent the same integer.
I wonder whether this is also possible in general. Can alpha-equality
(i.e., up to renaming) of two values be computed in pure lambda
calculus? If not, would it make sense to add an equality operator that
tests for equality and returns true or false (that is, the usual encodings
of true and false) ?
Any ideas or references?
Klaus
Darius
"Klaus Ostermann" <klaus...@SPAMgmx.net> wrote:
> Hi all,
>
> pure lambda calculus has no equality operator in order to compare
> values. I know that for special cases like church integers it is
> possible to "compute" whether two functions represent the same
> integer.
>
> I wonder whether this is also possible in general. Can alpha-equality
> (i.e., up to renaming) of two values be computed in pure lambda
> calculus?
No. This is one of the most direct consequences of results on the
(apparent) limits of computing, e.g. the Halting Problem.
> If not, would it make sense to add an equality operator that
> tests for equality and returns true or false (that is, the usual
> encodings of true and false) ?
Not if you are using lambda calculus as a model of computing. If you
are using the lambda calculus as a mathematical formalism, then it's
perfectly fine, but you are taking equality as given, not "computing"
it.
> Any ideas or references?
Well you could look up any of a variety of things about
Turing-completeness, Turing machines, the lambda calculus, the Halting
Problem, and decidability. But to sum it up, given
omega =def (\x.x x) (\x.x x) -- the computation that loops forever
does omega = omega or does omega = omega', where omega' is some
variation of omega? How would you decide this -within- the lambda
calculus?
Klaus Ostermann
I am very well aware of the fact about Halting problem, decidability etc.
What I was asking for is *alpha-equality*, that is, the equality relation
that
is closed under alpha-renaming (renaming of bound variables) only.
This relation is clearly decidable, I think. I just don't see how it could
be expressed in the lambda calculus itself.
I read some stuff about self-reflecting lambda calculi, within which
one can reason about the structure of a term inside the lambda-calculus,
somewhat similar to "quote" and "eval" in Lisp. However, this is much too
heavyweigth
for what I want.
Klaus
"Darius" <dda...@hotpop.com> schrieb im Newsbeitrag
news:20040113164210....@hotpop.com...
Neelakantan Krishnaswami
> On Tue, 13 Jan 2004 22:02:22 +0100
> "Klaus Ostermann" <klaus...@SPAMgmx.net> wrote:
>
>> Hi all,
>>
>> pure lambda calculus has no equality operator in order to compare
>> values. I know that for special cases like church integers it is
>> possible to "compute" whether two functions represent the same
>> integer.
>>
>> I wonder whether this is also possible in general. Can alpha-equality
>> (i.e., up to renaming) of two values be computed in pure lambda
>> calculus?
>
> No. This is one of the most direct consequences of results on the
> (apparent) limits of computing, e.g. the Halting Problem.
I don't see the relevance of the halting problem. Obviously, the
halting problem means you can't test for general equality in the
lambda calculus, but alpha-equivalence is a much weaker notion. A
recursion over the structure of the terms lets you test for alpha
equivalence, which is obviously decidable.
It seems to me that the real reason you can't compute the alpha
equivalence of lambda terms is because there's no way to get ahold of
the syntax of a term. For example, the terms
\x. x
and
\x. (\y. x) (\z. z)
are computationally equivalent, but are not alpha-equivalent. Since
there are no programs you can write that will distinguish these two
terms, there can be no way to compute the alpha equivalence of them
within the lambda calculus.
If you added some kind of quotation and anti-quotation mechanism to
the lambda calculus, a la interpreted Lisp, then you could calculate
the alpha-equivalence of values, because you could then destructure
terms.
--
Neel Krishnaswami
ne...@cs.cmu.edu
galathaea
:
: I am very well aware of the fact about Halting problem, decidability etc.
:
: What I was asking for is *alpha-equality*, that is, the equality relation
: that
: is closed under alpha-renaming (renaming of bound variables) only.
: This relation is clearly decidable, I think. I just don't see how it could
: be expressed in the lambda calculus itself.
:
: I read some stuff about self-reflecting lambda calculi, within which
: one can reason about the structure of a term inside the lambda-calculus,
: somewhat similar to "quote" and "eval" in Lisp. However, this is much too
: heavyweigth
: for what I want.
Would you not be confronted, then, with the undecidability of the word
problem? The alpha equality you refer to seems very similar to the general
word problem over presentations in group theory, known to be undecidable,
and key to the problem of identity in general proof theory and the lambda
calculus.
--
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
galathaea: prankster, fablist, magician, liar
Darius
"Klaus Ostermann" <klaus...@SPAMgmx.net> wrote:
> Dear Darius,
>
> I am very well aware of the fact about Halting problem, decidability
> etc.
>
> What I was asking for is *alpha-equality*, that is, the equality
> relation that
> is closed under alpha-renaming (renaming of bound variables) only.
Yes, I wondered about that, but considering in the standard pure lambda
calculus it's pretty immediate that it isn't. All you can do to (\x.x)
(\x.x) and (\x.x) is apply them and "look" at the result, they are not
alpha-equivalent but there is no way to compute that from within the
calculus. Hence me assuming you meant 'up to alpha-equivalence' or
something to that effect.
> This relation is clearly decidable, I think.
Convert to de Bruijn indices and compute structural equality. That
should work.
> I read some stuff about self-reflecting lambda calculi, within which
> one can reason about the structure of a term inside the
> lambda-calculus, somewhat similar to "quote" and "eval" in Lisp.
> However, this is much too heavyweigth for what I want.
How would you make it more lightweight?
Torben Ægidius Mogensen
> Can alpha-equality (i.e., up to renaming) of two values be computed
> in pure lambda calculus?
As other have said, this isn't generally possible. However, you can
(outside the lambda calculus) map lambda terms to encodings (also
represented as lambda terms) such that alpha-equivalence of the
encodings is computable. This is similar to the way you encode
numbers as lambda terms to operate on them.
Torben
Dennis E. Hamilton
can determine alpha-equality.
Eliminate lambda everywhere by converting to combinators, using some
unambiguous literals for the combinatory functions S and K. (This is a
recursive descent process that eliminates the innermost lambda's first.)
Two lambda-expressions that are identical except for naming of bound
variables will be identical (alpha-equal) after that elimination. Free
variables that were not bound anywhere in the originals will remain free, as
will constant elements.
The rules for the rewriting are given in
[Rosenbloom1950]
Rosenbloom, Paul. The Elements of Mathematical Logic. Dover (New York:
1950). pbk.
- Dennis
<http://orcmid.com/>
"Klaus Ostermann" <klaus...@SPAMgmx.net> wrote in message
news:bu1rbg$eqb$1...@news.tu-darmstadt.de...
> Dear Darius,
>
> I am very well aware of the fact about Halting problem, decidability etc.
>
> What I was asking for is *alpha-equality*, that is, the equality relation
> that
> is closed under alpha-renaming (renaming of bound variables) only.
> This relation is clearly decidable, I think. I just don't see how it could
> be expressed in the lambda calculus itself.
>
[ ... ]
Matthias Blume
> If you have the lambda expressions in some formal representation, then you
> can determine alpha-equality.
>
> Eliminate lambda everywhere by converting to combinators, using some
> unambiguous literals for the combinatory functions S and K. (This is a
> recursive descent process that eliminates the innermost lambda's first.)
>
> Two lambda-expressions that are identical except for naming of bound
> variables will be identical (alpha-equal) after that elimination. Free
> variables that were not bound anywhere in the originals will remain free, as
> will constant elements.
That's not what he is asking, and if you already have a representation
of the (abstract) syntax of the two terms, then testing for
alpha-equality is trivial. No need to convert to combinators.
What he is asking for is a lambda term, call it A, such that for all values
(by the way, what are values here? NFs? HNFs?) X and Y the expression
A X Y
reduces to \x\y.x (aka "true") if and only if X and Y are
alpha-equivalent and reduces to \x\y.y (aka "false") in all other
cases.
Matthias
Aki Helin
> "Klaus Ostermann" <klaus...@SPAMgmx.net> writes:
>> Can alpha-equality (i.e., up to renaming) of two values be computed
>> in pure lambda calculus?
>
> As other have said, this isn't generally possible. However, you can
> (outside the lambda calculus) map lambda terms to encodings (also
> represented as lambda terms) such that alpha-equivalence of the
> encodings is computable.
As a related note, lambda calculus extended with this kind of mapping
as a primitive is a way to fix a fairly wide class of problems. Some
examples that can be derived from it are the parallel or*, try**,
alpha-equivalence, internal compilation to combinators and a
(possibly nonterminating) search for the smallest expression with the
normal form or property X.
On the other hand by keeping the mapping separate (as the previous
poster did in http://citeseer.nj.nec.com/mogensen94efficient.html)
none of the nicer properties of lambda calculus are lost.
* And "or" that gives a normal form even if one of it's parameters
has none. This was referred to somewhere in in Barendregt:
"The Lambda Calculus, Its Syntax and Semantics"
** An "eval" with bounds. You can compute Chaitlin's omega with
this, but don't hold your breath.
--
aki helin
ol...@pobox.com
> What he is asking for is a lambda term, call it A, such that for all values
> (by the way, what are values here? NFs? HNFs?) X and Y the expression
>
> A X Y
>
> reduces to \x\y.x (aka "true") if and only if X and Y are
> alpha-equivalent and reduces to \x\y.y (aka "false") in all other
> cases.
That is a very good way of putting this question. It becomes clear
that the answer is NO. Not because of undecidability. Simply,
lambda-calculus does not provide introspection. Indeed, if X is a
term \x\y.x y and Y is the term \x.x then there cannot be such a term A
so that A X X and A Y Y reduce to \x\y.x (aka "true") but A X Y reduce
to \x\y.y (aka "false"). It is easy to see why: the only way a term A
may "examine" another term X is by applying it to something. However,
(X something something-else) and (Y something something-else) reduce
to a common term. So, the results of the applications are
indistinguishable.
It seems that some quandary in this thread comes from the fact that
the original post is somewhat contradictory:
> pure lambda calculus has no equality operator in order to compare
> values. I know that for special cases like church integers it is possible
> to "compute" whether two functions represent the same integer.
> I wonder whether this is also possible in general. Can alpha-equality
> (i.e., up to renaming) of two values be computed in pure lambda
> calculus?
The first paragraph talks about extensional equality: if CEQ is a term
comparing two Church numerals, then "CEQ X Y" (with X and Y as above)
will return \x\y.x (aka "true") because both X and Y represent Church
numeral 1. X and Y are not alpha-equivalent however. The second
paragraph talks about intensional equality: whether X and Y have the
same form (rather the same "effect"). But lambda-calculus offers no
reflection.
It goes without saying that one may use lambda-calculus to encode a
a lambda-calculator (choosing a particular representation of
lambda-terms as, well, lambda-terms). After all, lambda-calculus is
Turing-complete. One can then easily write such a term A so that
> such that for all values X and Y *representing object lambda-terms*
> expression
> A X Y
> reduces to \x\y.x (aka "true") if and only if X and Y
> *represent*
> alpha-equivalent terms and reduces to \x\y.y (aka "false") in all other
> cases.
Matthias Blume
> Matthias Blume <fi...@my.address.elsewhere> wrote in message news:<m13cahu...@tti5.uchicago.edu>...
> > What he is asking for is a lambda term, call it A, such that for all values
> > (by the way, what are values here? NFs? HNFs?) X and Y the expression
> >
> > A X Y
> >
> > reduces to \x\y.x (aka "true") if and only if X and Y are
> > alpha-equivalent and reduces to \x\y.y (aka "false") in all other
> > cases.
>
>
> That is a very good way of putting this question. It becomes clear
> that the answer is NO. Not because of undecidability. Simply,
> lambda-calculus does not provide introspection. Indeed, if X is a
> term \x\y.x y and Y is the term \x.x then there cannot be such a term A
> so that A X X and A Y Y reduce to \x\y.x (aka "true") but A X Y reduce
> to \x\y.y (aka "false"). It is easy to see why: the only way a term A
> may "examine" another term X is by applying it to something. However,
> (X something something-else) and (Y something something-else) reduce
> to a common term. So, the results of the applications are
> indistinguishable.
It might still be that the answer to the question depends on what we
consider "values". For example, while both your terms are \beta-NFs,
the second is not a \beta\eta-NF. There is a theorem that states that
distinct \beta\eta-NFs X and Y can be "separated", i.e., that for any
two terms G and H there is a term C such that C X reduces to G and C Y
reduces to H (if I recall correctly).
Probably overlooking the obvious, it is not immediately clear to me
whether or not this is related to the OP's question. (My guess is
that it is not, and that the above term A does not exist even if we
focus on \beta\eta-NFs. There is probably a simple proof for this,
but I can't think of it right now.)
Matthias
Tim Sweeney
Structural equality of unevaluated lambda terms is solveable in the
pure lambda calculus. One easy way to implement this is to store
terms using de Bruijn indices (Google for it) and to compare their
representations for structural equality. If comparing for equivalance
is a big goal of a system you're building, check out Luca Cardelli's
"Explicit Substitutiuons" paper for a nice term evaluation and
representation scheme that does not rely on names.
Torben Ægidius Mogensen
> It might still be that the answer to the question depends on what we
> consider "values". For example, while both your terms are \beta-NFs,
> the second is not a \beta\eta-NF. There is a theorem that states that
> distinct \beta\eta-NFs X and Y can be "separated", i.e., that for any
> two terms G and H there is a term C such that C X reduces to G and C Y
> reduces to H (if I recall correctly).
This obviously works only for closed terms, as there is no way we can
make C (\x.a) --> T while C (\x.b) --> F.
Torben
Klaus Ostermann
I know that it is possible to compute alpha-equality. However,
it seems (and most others here seem to agree with that) that it
is not possible to do that *inside* the lambda calculus itself.
Klaus
Klaus Ostermann
Most of us seem to agree that determining alpha equality of two
values (i.e., of the form x or \x.t ) is not possible inside the lambda
calculus.
Isn't this strange? Comparison of two values is nothing special
in every "real" programming language like C or Java - just compare
the bytes.
In the lambda calculus, it seems as if we need to go to some kind
of meta layer to do the same.
It seems to me that "values" in the lambda calculus have a different
nature than values in C or Java. Values in
lambda calculus correspond more to "0" and "1" in real programming
languages, which we use to construct values. If we would have
different representations of 0 or 1 in C or Java, we also wouldn't
have means to differentiate them.
Is this analogy correct? What do you think?
Klaus
Tomasz Zielonka
>
> Isn't this strange? Comparison of two values is nothing special
> in every "real" programming language like C or Java - just compare
> the bytes.
Is 2 + 2 different than 4 in C or Java?
Best regards,
Tom
--
.signature: Too many levels of symbolic links
Klaus Ostermann
2+2 is not a value.
Klaus
Andreas Rossberg
>
> Most of us seem to agree that determining alpha equality of two
> values (i.e., of the form x or \x.t ) is not possible inside the lambda
> calculus.
>
> Isn't this strange? Comparison of two values is nothing special
> in every "real" programming language like C or Java - just compare
> the bytes.
For that, you need built-in primitives for accessing the representation
level of values. You cannot express those "within" the language itself
either.
- Andreas
--
Andreas Rossberg, ross...@ps.uni-sb.de
"Computer games don't affect kids; I mean if Pac Man affected us
as kids, we would all be running around in darkened rooms, munching
magic pills, and listening to repetitive electronic music."
- Kristian Wilson, Nintendo Inc.
Matthias Blume
Right. I was quoting from (very faint) memory. I might even
completely misremember.
Matthias
Tomasz Zielonka
>> Is 2 + 2 different than 4 in C or Java?
>
> 2+2 is not a value.
But you want
(\f.\x.(f (f (f (f x)))))
to be different than
(\n.\m. n (\s.\g.\y.(g (s g y))) m) (\f.\x.(f (f x))) (\f.\x.(f (f x)))
right? ;)
> Klaus
Peter G. Hancock
>>>>> Klaus Ostermann wrote (on Fri, 16 Jan 2004 at 14:25):
> Isn't this strange? Comparison of two values is nothing special
> in every "real" programming language like C or Java - just compare
> the bytes.
It depends what you mean by a value. Often, equality between "things"
of some kind is coarser than bit-level equality. Think of different
representations of the same table by balanced trees, etc. And often, bit
level equality doesn't imply equality of value. Think of
self-relative pointers (in different locations), etc.
> In the lambda calculus, it seems as if we need to go to some kind
> of meta layer to do the same.
I think there's something in that. There's definitional equality
(equality in virtue of definitions), that lives on "some kind of meta
layer"), and identity (the smallest reflexive relation between
values). People have struggled with what exactly "equality" might
mean (in a mathematical or computational setting) for well over 20
centuries.
What the values are "in" the lambda calculus I don't know. It's by no
means clear its got anything to do with irreducible terms. It seems to
me that's a notion that comes up when you give a _model_ of the lambda
calculus, and there are zillions of those.
I'm just saying (rather lamely) that we're in deep water here.
Peter Hancock