OK, so I'm guessing there might be one or two (!) people around here who
know something about the Lambda calculus.
I've written a simple interpretter that takes any valid Lambda
expression and performs as many beta reductions as possible. When the
input is first received, all the variables
forgot to cc the cafe :-)
On Sun, Jun 21, 2009 at 1:08 PM, Keith Sheppardkeiths...@gmail.com wrote:
hmm, it's been a while but...
i think this infinite loop with a free variable would cause collision
(\a . a a) (\b . b b d)
On Sun, Jun 21, 2009 at 12:53 PM, Andrew
An answer would probably depend on the reductions order you've chosen.
Would that do?
(\e - e (\u - e (\v - u))) (\f - \x - f x) -- all variables have
different names, see?
= (\f - \x - f x) (\u - (\f - \x - f x) (\v - u))
= \x - (\u - (\f - \x - f x) (\v - u)) x
= \x - (\f - \x - f x)
On Sun, Jun 21, 2009 at 8:53 PM, Andrew
Coppinandrewcop...@btinternet.com wrote:
OK, so I'm guessing there might be one or two (!) people around here who
know something about the Lambda calculus.
I've written a simple interpretter that takes any valid Lambda expression
and performs as many
2009/6/21 Andrew Coppin andrewcop...@btinternet.com:
OK, so I'm guessing there might be one or two (!) people around here who
know something about the Lambda calculus.
I've written a simple interpretter that takes any valid Lambda expression
and performs as many beta reductions as possible.
Correction: I think that one can find an expression that causes name
clashes anyway, I'm just not certain that there is one that would
clash independent of whichever order you choose.
On 21 Jun 2009, at 21:12, Miguel Mitrofanov wrote:
An answer would probably depend on the reductions order
scratch that... it's completely wrong
On Sun, Jun 21, 2009 at 1:09 PM, Keith Sheppardkeiths...@gmail.com wrote:
forgot to cc the cafe :-)
On Sun, Jun 21, 2009 at 1:08 PM, Keith Sheppardkeiths...@gmail.com wrote:
hmm, it's been a while but...
i think this infinite loop with a free variable
On Sun, Jun 21, 2009 at 05:53:04PM +0100, Andrew Coppin wrote:
I've written a simple interpretter that takes any valid Lambda
expression and performs as many beta reductions as possible. When the
input is first received, all the variables are renamed to be unique.
Question: Does this
On Sun, Jun 21, 2009 at 05:53:04PM +0100, Andrew Coppin wrote:
OK, so I'm guessing there might be one or two (!) people around here who
know something about the Lambda calculus.
I've written a simple interpretter that takes any valid Lambda expression
and performs as many beta reductions as
Miguel Mitrofanov wrote:
Correction: I think that one can find an expression that causes name
clashes anyway, I'm just not certain that there is one that would clash
independent of whichever order you choose.
Yes there is.
Consider
(\f g - f (f (f (f (f (f g)) (\l a b - l (b a)) (\x -
Lauri Alanko wrote:
With name collisions I'm assuming you mean inadvertent variable
capture. The answer depends on your evaluation strategy. If you never
reduce inside a lambda (e.g. call-by-name or call-by-value), then you
will always be substituting a closed term in place of a variable, and
Wow. Now you've showed it to me, it seems pretty obvious. That's what
I like about math.
On 21 Jun 2009, at 21:56, Bertram Felgenhauer wrote:
Miguel Mitrofanov wrote:
Correction: I think that one can find an expression that causes name
clashes anyway, I'm just not certain that there is one
Probably the easiest way to fix this was already proposed by Deniz
Dogan: de Bruijn indices.
On 21 Jun 2009, at 21:57, Andrew Coppin wrote:
Lauri Alanko wrote:
With name collisions I'm assuming you mean inadvertent variable
capture. The answer depends on your evaluation strategy. If you
Andrew Coppin wrote:
Ladies and gentlemen, we have a counter-example!
(\x1 - x1 x1) (\y2 - \z3 - y2 z3)
(\y2 - \z3 - y2 z3) (\y2 - \z3 - y2 z3)
\z3 - (\y2 - \z3 - y2 z3) z3
\z3 - \z3 - z3 z3
Now the operative question becomes... how in the name of God to I fix
this?
(The obvious
Andrew Coppin wrote:
Well anyway, the obvious thing to do is after each reduction, strip
off all the variable indicies and rerun the labeller to assign new
indicies. But does this solution work properly in general?
No.
Supposing some Lambda expression eventually reduces to, say,
\x1 - \x2
Hello,
Have you read the lambda calculus chapter in:
The Implementation of Functional Programming Languages by Simon Peyton
Jones, published by Prentice Hall, 1987:
http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/
- jeremy
As others have pointed out, it is not enough to rename before reduction.
It should be pretty obvious since when you do substitution and copy a
lambda expression into more than once place you will introduce
variables with the same name. You can keep unique variables by
cloning during substitution,
Actually, keeping all names distinct is not de Bruijn numbering, it's
called the Barendregt convention.
On Sun, Jun 21, 2009 at 7:05 PM, Deniz Dogandeniz.a.m.do...@gmail.com wrote:
2009/6/21 Andrew Coppin andrewcop...@btinternet.com:
OK, so I'm guessing there might be one or two (!) people
On Sun, Jun 21, 2009 at 07:48:30PM +0100, Andrew Coppin wrote:
Andrew Coppin wrote:
Well anyway, the obvious thing to do is after each reduction, strip off
all the variable indicies and rerun the labeller to assign new indicies.
But does this solution work properly in general?
No.
All,
Just as ancillary information: ∃ a calculator on Hackage called
LambdaCalculator. Its rather short (loc wise) and fun to play with.
Thomas
On Sun, Jun 21, 2009 at 10:57 AM, Andrew
Coppinandrewcop...@btinternet.com wrote:
Lauri Alanko wrote:
With name collisions I'm assuming you mean
20 matches
Mail list logo
