Ian Price | 2 May 21:47 2013

Lambda Calculus question on equivalence

Hi,

I know this isn't perhaps the best forum for this, but maybe you can
give me some pointers.

Earlier today I was thinking about De Bruijn Indices, and they have the
property that two lambda terms that are alpha-equivalent, are expressed
in the same way, and I got to wondering if it was possible to find a
useful notion of function equality, such that it would be equivalent to
structural equality (aside from just defining it this way), though
obviously we cannot do this in general.

So the question I came up with was:

Can two normalised (i.e. no subterm can be beta or eta reduced) lambda
terms be "observationally equivalent", but not alpha equivalent?

By observationally equivalent, I mean A and B are observationally
equivalent if for all lambda terms L: (L A) is equivalent to (L B) and
(A L) is equivalent to (B L). The definition is admittedly circular, but
I hope it conveys enough to understand what I'm after.

My intuition is no, but I am not sure how to prove it, and it seems to
me this sort of question has likely been answered before.

Cheers
--

-- 
Ian Price -- shift-reset.com

"Programming is like pinball. The reward for doing it well is
(Continue reading)

Edward Z. Yang | 2 May 22:11 2013
Picon

Re: Lambda Calculus question on equivalence

The notion of equivalence you are talking about (normally L is referred
to as a "context") is 'extensional equality'; that is, functions f
and g are equal if forall x, f x = g x.  It's pretty easy to give
a pair of functions which are not alpha equivalent but are observationally
equivalent:

    if collatz_conjecture then true else bottom
    true / bottom (Depending on whether or not you think the collatz conjecture is true...)

Cheers,
Edward

Excerpts from Ian Price's message of Thu May 02 12:47:07 -0700 2013:
> Hi,
> 
> I know this isn't perhaps the best forum for this, but maybe you can
> give me some pointers.
> 
> Earlier today I was thinking about De Bruijn Indices, and they have the
> property that two lambda terms that are alpha-equivalent, are expressed
> in the same way, and I got to wondering if it was possible to find a
> useful notion of function equality, such that it would be equivalent to
> structural equality (aside from just defining it this way), though
> obviously we cannot do this in general.
> 
> So the question I came up with was:
> 
> Can two normalised (i.e. no subterm can be beta or eta reduced) lambda
> terms be "observationally equivalent", but not alpha equivalent?
> 
(Continue reading)

Francesco Mazzoli | 2 May 22:42 2013
Picon

Re: Lambda Calculus question on equivalence

At Thu, 02 May 2013 20:47:07 +0100,
Ian Price wrote:
> I know this isn't perhaps the best forum for this, but maybe you can
> give me some pointers.
> 
> Earlier today I was thinking about De Bruijn Indices, and they have the
> property that two lambda terms that are alpha-equivalent, are expressed
> in the same way, and I got to wondering if it was possible to find a
> useful notion of function equality, such that it would be equivalent to
> structural equality (aside from just defining it this way), though
> obviously we cannot do this in general.
> 
> So the question I came up with was:
> 
> Can two normalised (i.e. no subterm can be beta or eta reduced) lambda
> terms be "observationally equivalent", but not alpha equivalent?
> 
> By observationally equivalent, I mean A and B are observationally
> equivalent if for all lambda terms L: (L A) is equivalent to (L B) and
> (A L) is equivalent to (B L). The definition is admittedly circular, but
> I hope it conveys enough to understand what I'm after.
> 
> My intuition is no, but I am not sure how to prove it, and it seems to
> me this sort of question has likely been answered before.

Yes, they can.  Take ‘f = λ x : ℕ → x + x’ and ‘g = λ x : ℕ → 2 * x’.  These
terms are not ‘definitionally’ equal (which could be the α-equivalence you cite
but can be extended to fancier checks on the term structure).  However, for all
(well typed) inputs the result of those two functions are the same: they are
‘extensionally’ equal [1].  The first part (...(L A) is equivalent to (L B)...)
(Continue reading)

Timon Gehr | 2 May 23:16 2013
Picon
Picon

Re: Lambda Calculus question on equivalence

On 05/02/2013 10:42 PM, Francesco Mazzoli wrote:
> At Thu, 02 May 2013 20:47:07 +0100,
> Ian Price wrote:
>> I know this isn't perhaps the best forum for this, but maybe you can
>> give me some pointers.
>>
>> Earlier today I was thinking about De Bruijn Indices, and they have the
>> property that two lambda terms that are alpha-equivalent, are expressed
>> in the same way, and I got to wondering if it was possible to find a
>> useful notion of function equality, such that it would be equivalent to
>> structural equality (aside from just defining it this way), though
>> obviously we cannot do this in general.
>>
>> So the question I came up with was:
>>
>> Can two normalised (i.e. no subterm can be beta or eta reduced) lambda
>> terms be "observationally equivalent", but not alpha equivalent?
>>
>> By observationally equivalent, I mean A and B are observationally
>> equivalent if for all lambda terms L: (L A) is equivalent to (L B) and
>> (A L) is equivalent to (B L). The definition is admittedly circular, but
>> I hope it conveys enough to understand what I'm after.
>>
>> My intuition is no, but I am not sure how to prove it, and it seems to
>> me this sort of question has likely been answered before.
>
> Yes, they can.  Take ‘f = λ x : ℕ → x + x’ and ‘g = λ x : ℕ → 2 * x’.

Those are not lambda terms.
Furthermore, if those terms are rewritten to operate on church numerals, 
(Continue reading)

Francesco Mazzoli | 2 May 23:33 2013
Picon

Re: Lambda Calculus question on equivalence

At Thu, 02 May 2013 23:16:45 +0200,
Timon Gehr wrote:
> > Yes, they can.  Take ‘f = λ x : ℕ → x + x’ and ‘g = λ x : ℕ → 2 * x’.
> Those are not lambda terms.

How are they not lambda terms?

> Furthermore, if those terms are rewritten to operate on church numerals,
> they have the same unique normal form, namely λλλ 3 2 (3 2 1).

You are assume things about the implementation of natural numbers, of *, and +
(admittedly they were underspecified on my side :).  They could be implemented
in different way, or I could simply change the second definition to ‘λ x → x *
2’, in which case execution would be stuck on the abstract variable.

In any case, definitionally different functions can be extensionally equal,
there is little doubt on that.

> > These terms are not ‘definitionally’ equal (which could be the α-equivalence you cite
> > but can be extended to fancier checks on the term structure).  However, for all
> > (well typed)  inputs the result of those two functions are the same: they are
> > ‘extensionally’ equal [1].  The first part (...(L A) is equivalent to (L B)...)
> > holds: the same function will always produce the same output given
> > definitionally equal arguments.
> > ...
> 
> (I guess the question is about untyped lambda calculus.)

I don’t think so, since Ian talked about ‘terminating’ λ-calculus, while
the untyped λ-calculus isn’t... otherwise you can’t normalise and compare.
(Continue reading)

Timon Gehr | 3 May 00:44 2013
Picon
Picon

Re: Lambda Calculus question on equivalence

On 05/02/2013 11:33 PM, Francesco Mazzoli wrote:
> At Thu, 02 May 2013 23:16:45 +0200,
> Timon Gehr wrote:
>>> Yes, they can.  Take ‘f = λ x : ℕ → x + x’ and ‘g = λ x : ℕ → 2 * x’.
>> Those are not lambda terms.
>
> How are they not lambda terms?
>

I guess if + and * are interpreted as syntax sugar then they are lambda 
terms with free variables. In this case, they are not equivalent.

>> Furthermore, if those terms are rewritten to operate on church numerals,
>> they have the same unique normal form, namely λλλ 3 2 (3 2 1).
>
> You are assume things about the implementation of natural numbers, of *, and +
> (admittedly they were underspecified on my side :).  They could be implemented
> in different way, or I could simply change the second definition to ‘λ x → x *
> 2’, in which case execution would be stuck on the abstract variable.
>

AFAICS this does not show anything either, as the terms λλλ 3 2 (3 2 1) 
and λλ 2 (λ 2 (2 1)) are not extensionally equivalent. (since their 
domain is not restricted to terms corresponding to church numerals. Eg. 
feed them λλ 2.)

> In any case, definitionally different functions can be extensionally equal,
> there is little doubt on that.
>
>>> These terms are not ‘definitionally’ equal (which could be the α-equivalence you cite
(Continue reading)

Francesco Mazzoli | 3 May 01:08 2013
Picon

Re: Lambda Calculus question on equivalence

At Fri, 03 May 2013 00:44:09 +0200,
Timon Gehr wrote:
> 
> On 05/02/2013 11:33 PM, Francesco Mazzoli wrote:
> > At Thu, 02 May 2013 23:16:45 +0200,
> > Timon Gehr wrote:
> >>> Yes, they can.  Take ‘f = λ x : ℕ → x + x’ and ‘g = λ x : ℕ → 2 * x’.
> >> Those are not lambda terms.
> >
> > How are they not lambda terms?
> >
> 
> I guess if + and * are interpreted as syntax sugar then they are lambda 
> terms with free variables. In this case, they are not equivalent.

+ and * should be interpreted as term definitions, that can be replaced with the
actual body, whatever that might be.  I’m not sure about the ‘sugar’ you are
talking about... but again these details don’t really matter.

> > You are assume things about the implementation of natural numbers, of *, and +
> > (admittedly they were underspecified on my side :).  They could be implemented
> > in different way, or I could simply change the second definition to ‘λ x → x *
> > 2’, in which case execution would be stuck on the abstract variable.
> >
> 
> AFAICS this does not show anything either, as the terms λλλ 3 2 (3 2 1) 
> and λλ 2 (λ 2 (2 1)) are not extensionally equivalent. (since their 
> domain is not restricted to terms corresponding to church numerals. Eg. 
> feed them λλ 2.)

(Continue reading)

Edward Z. Yang | 2 May 23:37 2013
Picon

Re: Lambda Calculus question on equivalence

Excerpts from Timon Gehr's message of Thu May 02 14:16:45 -0700 2013:
> Those are not lambda terms.
> Furthermore, if those terms are rewritten to operate on church numerals, 
> they have the same unique normal form, namely λλλ 3 2 (3 2 1).

The trick is to define the second one as x * 2 (and assume the fixpoint
operates on the first argument). Now they are not equal.

Edward

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Timon Gehr | 3 May 01:00 2013
Picon
Picon

Re: Lambda Calculus question on equivalence

On 05/02/2013 11:37 PM, Edward Z. Yang wrote:
> Excerpts from Timon Gehr's message of Thu May 02 14:16:45 -0700 2013:
>> Those are not lambda terms.
>> Furthermore, if those terms are rewritten to operate on church numerals,
>> they have the same unique normal form, namely λλλ 3 2 (3 2 1).
>
> The trick is to define the second one as x * 2 (and assume the fixpoint
> operates on the first argument). Now they are not equal.
>
> Edward
>

Neither equal nor extensionally equivalent.

mult = λm.λn.λf. n (m f)

mult 2 = λn.λf. n (2 f)

mult 2 = λn.λf. n (λx. f (f x))

flip mult 2 = λm.λf. 2 (m f)

flip mult 2 = λm.λf.λx. m f (m f x)

(λn.λf. n (λx. f (f x)) const = λf. const (λx. f (f x))
                               = λf.λa.λx. f (f x)

This is clearly not the same as:

(λm.λf.λx. m f (m f x)) const = λf.λx. f
(Continue reading)

Roman Cheplyaka | 3 May 00:33 2013

Re: Lambda Calculus question on equivalence

IIRC, Barendregt'84 monography ("The Lambda Calculus: Its Syntax and
Semantics") has a significant part of it devoted to this question.

* Ian Price <ianprice90 <at> googlemail.com> [2013-05-02 20:47:07+0100]
> Hi,
> 
> I know this isn't perhaps the best forum for this, but maybe you can
> give me some pointers.
> 
> Earlier today I was thinking about De Bruijn Indices, and they have the
> property that two lambda terms that are alpha-equivalent, are expressed
> in the same way, and I got to wondering if it was possible to find a
> useful notion of function equality, such that it would be equivalent to
> structural equality (aside from just defining it this way), though
> obviously we cannot do this in general.
> 
> So the question I came up with was:
> 
> Can two normalised (i.e. no subterm can be beta or eta reduced) lambda
> terms be "observationally equivalent", but not alpha equivalent?
> 
> By observationally equivalent, I mean A and B are observationally
> equivalent if for all lambda terms L: (L A) is equivalent to (L B) and
> (A L) is equivalent to (B L). The definition is admittedly circular, but
> I hope it conveys enough to understand what I'm after.
> 
> My intuition is no, but I am not sure how to prove it, and it seems to
> me this sort of question has likely been answered before.
> 
> Cheers
(Continue reading)

Andreas Abel | 3 May 16:34 2013
Picon

Re: Lambda Calculus question on equivalence

The answer to your question is given in Boehm's theorem, and the answer 
is "no", as you suspect.

For the untyped lambda-calculus, alpha-equivalence of beta-eta normal 
forms is the same as observational equivalence.  Or put the other way 
round, two normal forms which are not alpha-equivalent can be separated 
by an observation L.

Cheers,
Andreas

On 03.05.2013 00:33, Roman Cheplyaka wrote:
> IIRC, Barendregt'84 monography ("The Lambda Calculus: Its Syntax and
> Semantics") has a significant part of it devoted to this question.
>
> * Ian Price <ianprice90 <at> googlemail.com> [2013-05-02 20:47:07+0100]
>> Hi,
>>
>> I know this isn't perhaps the best forum for this, but maybe you can
>> give me some pointers.
>>
>> Earlier today I was thinking about De Bruijn Indices, and they have the
>> property that two lambda terms that are alpha-equivalent, are expressed
>> in the same way, and I got to wondering if it was possible to find a
>> useful notion of function equality, such that it would be equivalent to
>> structural equality (aside from just defining it this way), though
>> obviously we cannot do this in general.
>>
>> So the question I came up with was:
>>
(Continue reading)

Francesco Mazzoli | 3 May 17:38 2013
Picon

Re: Lambda Calculus question on equivalence

At Fri, 03 May 2013 16:34:28 +0200,
Andreas Abel wrote:
> The answer to your question is given in Boehm's theorem, and the answer 
> is "no", as you suspect.
> 
> For the untyped lambda-calculus, alpha-equivalence of beta-eta normal 
> forms is the same as observational equivalence.  Or put the other way 
> round, two normal forms which are not alpha-equivalent can be separated 
> by an observation L.

Thanks for the reference, and sorry to Ian for the confusion given by the fact
that I was thinking in types...

However, what is the notion of ‘telling apart’ here exactly?  Is it simply that
the resulting terms will have different denotations in some semantics?  My
initial (wrong) assumption about termination was due to the fact that I thought
that the ultimate test of equivalence was to be done with α-equivalence itself,
on the normal forms.

Francesco

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Jon Fairbairn | 4 May 10:34 2013
X-Face
Picon
Picon

Re: Lambda Calculus question on equivalence

Francesco Mazzoli <f <at> mazzo.li> writes:

> At Fri, 03 May 2013 16:34:28 +0200,
> Andreas Abel wrote:
>> The answer to your question is given in Boehm's theorem, and the answer 
>> is "no", as you suspect.
>> 
>> For the untyped lambda-calculus, alpha-equivalence of beta-eta normal 
>> forms is the same as observational equivalence.  Or put the other way 
>> round, two normal forms which are not alpha-equivalent can be separated 
>> by an observation L.
>
> Thanks for the reference, and sorry to Ian for the confusion given by the fact
> that I was thinking in types...
>
> However, what is the notion of ‘telling apart’ here exactly?  Is it simply that
> the resulting terms will have different denotations in some semantics?  My
> initial (wrong) assumption about termination was due to the fact that I thought
> that the ultimate test of equivalence was to be done with α-equivalence itself,
> on the normal forms.

α-equivalence on the Böhm trees — normal forms extended to
infinity. I suppose that counts as “some semantics” but its very
direct.

--

-- 
Jón Fairbairn                                 Jon.Fairbairn <at> cl.cam.ac.uk

_______________________________________________
Haskell-Cafe mailing list
(Continue reading)

Francesco Mazzoli | 4 May 10:44 2013
Picon

Re: Lambda Calculus question on equivalence

At Sat, 04 May 2013 09:34:01 +0100,
Jon Fairbairn wrote:
> α-equivalence on the Böhm trees — normal forms extended to
> infinity. I suppose that counts as “some semantics” but its very
> direct.

Ah yes, that makes sense.  Thanks!

Francesco

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane