Re: [Haskell-cafe] Lambda Calculus question on equivalence

2013-05-04 Thread Francesco Mazzoli
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-

Re: [Haskell-cafe] Lambda Calculus question on equivalence

2013-05-04 Thread Jon Fairbairn
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 obser

Re: [Haskell-cafe] Lambda Calculus question on equivalence

2013-05-03 Thread Francesco Mazzoli
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 oth

Re: [Haskell-cafe] Lambda Calculus question on equivalence

2013-05-03 Thread Andreas Abel
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 ca

Re: [Haskell-cafe] Lambda Calculus question on equivalence

2013-05-02 Thread Francesco Mazzoli
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

Re: [Haskell-cafe] Lambda Calculus question on equivalence

2013-05-02 Thread Timon Gehr
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 t

Re: [Haskell-cafe] Lambda Calculus question on equivalence

2013-05-02 Thread Timon Gehr
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 th

Re: [Haskell-cafe] Lambda Calculus question on equivalence

2013-05-02 Thread Roman Cheplyaka
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 toda

Re: [Haskell-cafe] Lambda Calculus question on equivalence

2013-05-02 Thread Edward Z. Yang
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 assum

Re: [Haskell-cafe] Lambda Calculus question on equivalence

2013-05-02 Thread Francesco Mazzoli
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 norma

Re: [Haskell-cafe] Lambda Calculus question on equivalence

2013-05-02 Thread Timon Gehr
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 term

Re: [Haskell-cafe] Lambda Calculus question on equivalence

2013-05-02 Thread Francesco Mazzoli
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

Re: [Haskell-cafe] Lambda Calculus question on equivalence

2013-05-02 Thread Edward Z. Yang
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

[Haskell-cafe] Lambda Calculus question on equivalence

2013-05-02 Thread Ian Price
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 possibl