2 May 2013 21:47

## 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
```

2 May 2013 22:11

### 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?
>
```

2 May 2013 22:42

### 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)...)
```

2 May 2013 23:16

### 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,
```

2 May 2013 23:33

### 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.
```

3 May 2013 00:44

### 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
```

3 May 2013 01:08

### 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.)

```

2 May 2013 23:37

### 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

_______________________________________________
```
3 May 2013 01:00

### 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
```

3 May 2013 00:33

### 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
```

3 May 2013 16:34

### 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:
>>
```

3 May 2013 17:38

### Re: Lambda Calculus question on equivalence

```At Fri, 03 May 2013 16:34:28 +0200,
Andreas Abel wrote:
> 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

_______________________________________________
```
4 May 2013 10:34

### 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:
>> 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

_______________________________________________
```

4 May 2013 10:44

### 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

_______________________________________________