Lambda Calculus question on equivalence

older
A three page web application in a...

Ian Price

2 May 2013 2 May '13

7:47 p.m.

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 the opportunity to do it again" - from "The Wizardy Compiled"

Show replies by date

Edward Z. Yang

2 May 2 May

8:11 p.m.

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?

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

Francesco Mazzoli

8:42 p.m.

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)...) holds: the same function will always produce the same output given definitionally equal arguments. You stumbled upon a subject that generated a great deal of research in the field of type theory [2]. There are various developments focusing on having a ‘better’ equality that identifies more things are equal. Your intuition of ‘observationally’ equal will probably be close to the notion of isomorphism between two sets, and in fact one of the more exciting developments right now concerns a type theory where equality is based on isomorphism [3]—however the computational ‘details’ haven’t been worked out yet :). There are other attempts [4] that fix the instance above (function extensionality) but don’t quite go all the way (not without reasons, since the isomorphism business has far reaching consequences that could be seen as impractical). Francesco [1]: https://en.wikipedia.org/wiki/Extensionality [2]: https://en.wikipedia.org/wiki/Intuitionistic_type_theory#Extensional_versus_... [3]: https://en.wikipedia.org/wiki/Homotopy_type_theory [4]: http://www.cs.nott.ac.uk/~txa/publ/obseqnow.pdf

Timon Gehr

9:16 p.m.

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, they have the same unique normal form, namely λλλ 3 2 (3 2 1).

...

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

Francesco Mazzoli

9:33 p.m.

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. Besides that, the typed calculi I cited are interesting because they internalise some notion of equality, but the observation about function extensionality holds with or without types. Francesco

Timon Gehr

10:44 p.m.

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

'terminating' does not occur in the original post.

...

otherwise you can’t normalise and compare. ...

The terms in question are already normalised.

Francesco Mazzoli

11:08 p.m.

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

That’s a good point, but I was talking about typed terms. I guess the discussion does change if you go into the untyped lambda calculus but then you are opening a big can of worms regarding to termination (see below).

...

...
I don’t think so, since Ian talked about ‘terminating’ λ-calculus, while the untyped λ-calculus isn’t...

'terminating' does not occur in the original post.

‘normal form’ does, which is what I was referring to.

...

...
otherwise you can’t normalise and compare. ...

The terms in question are already normalised.

‘(L A)’ and ‘(L B)’ are clearly not normalised (if L is a function). If the calculus is not terminating you need to explain what’s your strategy when comparing things that are not in a normal form already. Francesco

Edward Z. Yang

9:37 p.m.

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

Timon Gehr

11 p.m.

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

Roman Cheplyaka

10:33 p.m.

IIRC, Barendregt'84 monography ("The Lambda Calculus: Its Syntax and Semantics") has a significant part of it devoted to this question. * Ian Price [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 -- Ian Price -- shift-reset.com

"Programming is like pinball. The reward for doing it well is the opportunity to do it again" - from "The Wizardy Compiled"

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

Andreas Abel

3 May 3 May

2:34 p.m.

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 [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 -- Ian Price -- shift-reset.com

"Programming is like pinball. The reward for doing it well is the opportunity to do it again" - from "The Wizardy Compiled"

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

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

-- Andreas Abel <>< Du bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.abel@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/

Francesco Mazzoli

3:38 p.m.

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

Jon Fairbairn

4 May 4 May

8:34 a.m.

Francesco Mazzoli 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@cl.cam.ac.uk

Francesco Mazzoli

8:44 a.m.

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

4448

Age (days ago)

4450

Last active (days ago)

List overview

Download

13 comments

7 participants

participants (7)

Andreas Abel
Edward Z. Yang
Francesco Mazzoli
Ian Price
Jon Fairbairn
Roman Cheplyaka
Timon Gehr