Francesco Mazzoli f...@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
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
___
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
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
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
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
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
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
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
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
IIRC, Barendregt'84 monography (The Lambda Calculus: Its Syntax and
Semantics) has a significant part of it devoted to this question.
* Ian Price ianpric...@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
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
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
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
14 matches
Mail list logo
