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-
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
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
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
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
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
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
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
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
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
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
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
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
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
14 matches
Mail list logo