Lambda Calculus in Snap!

I have ideas for lambda calculus blocks.
These blocks are:
λ(v,term)
variable
alpha(v,v name)
beta(v,term)
apply(term,term)
It's just an idea, so I never coded these blocks.

I have 2 blocks for you:

rings and call.

what are they

now i understand

error with apply block:
image
definition:

heres a cool little website about lambda calculus

Huh? No link shows.

https://people.bath.ac.uk/wbh22/LogicGames/games/LambdaCalculus2/index.html

That's blocked for me.

Here's my attempt. Does that help?

Two things about your λ. First, in the lambda calculus, the function created by λ has to take exactly one input. So you really want it to look like
Lambda Calc script pic
but at present there's no way to specify the arity of a Procedure-type input. Luckily, your existing block can work if its input function has ≥1 empty input slots, e.g.,
Lambda Calc script pic (1)
but of course using a function made of lambdas; the + is just an example. But the definition of your λ has to turn its input into a function of one input by doing something like
Lambda Calc script pic (2)
(That's as much of a hint as I want to give you at this point; there's more to the definition than just that arity-one gray ring.)

Second, things get way more complicated if you want a procedure to be able to create and report a new procedure, as in
Lambda Calc script pic (3)
(This is actual Snap! code, not in your λ project.) The procedure created by that gray ring has to remember the value of n in this particular call to make-adder:
Lambda Calc script pic (4)
Lambda Calc script pic (5)
Lambda Calc script pic (6)
ADD-THREE remembers n=3; ADD-FIVE remembers n=5. In normal Snap! programming it's only in advanced projects that you use this feature (technical term: lexical scope), but if you're trying to build arithmetic in pure lambda calculus, you rely constantly on lexical scope. For example. MAKE-ADDER is
λn . λx . x+n except of course that instead of "x+n" you have a huge mess of lambdas.

I'm not sure what's going on here...
wdtemLambda Calc script pic

Getting closer...

image

This doesn't surprise me. If you don't put anything in that input slot, you are making a function with no body. I don't know what that particular error message means in this context, but see if it works with a real function! If so, don't worry about the empty body case.

Oh I see what you're doing. You shouldn't have to use metaprogramming to construct a new function body. Actually it may be that you don't need an INPUT NAMES: at all; if you provide an input value when you call the ringed function, CALL will fill empty input slots in the body. I was wrong about needing an explicit formal parameter when empty input slots will do. But, for example, the SUCCESSOR function is
λn . λf . λx (f ((n f) x)
and to represent that in Snap! you need a way to say which input goes where. You can do that with an upvar, so your constructor would be untitled script pic (2). Here's how I wrote it:
untitled script pic (3)
The script in the ring has an empty input slot in the SET block, so whatever input value is given in the CALL will be the value of X. That allows the body of FUNC to use the upvar X as if it were an input name.

This works because we're doing functional programming. If the user's function tried to SET X to something, I'm pretty sure it wouldn't work; the SET block's variable menu wouldn't include X. But for functional programming it works fine:


The inner CALL binds X to 5 and, in an environment including that binding, returns the function (λy.etc). Then the outer CALL binds Y to 7 and evaluates Y−X in an environment containing both bindings.

Have you used upvars before? The crucial thing about them is that the variable has two names. Inside the procedure λ, it's always called X, the name in the block prototype (inside the hat block). But when λ is called, the user can give it a different name, as I did in the inner λ, and then that's the name by which the caller refers to it.

Oh! That makes sense!

oops now i dont :hushed:

This topic was automatically closed 30 days after the last reply. New replies are no longer allowed.