Lambda Calculus let explanation needed

Question

In this treatment of let a lambda calculus version of let is given

(\f.z)(\x.y)

with the words

f is defined by f x = y in the expression z, and then as

let f x = y in z

I know from a beginner's perspective how Haskell's let works, i.e., the definitions follows the let and expressions (do something with those definitions) follows the in.

let <definitions> in <expression>

But this most general lambda calculus description is baffling. For example, I assume there could be a Haskell lambda function version of let f x = y in z. Could someone write this out -- and maybe give an example or two -- in Haskell? Just guessing, it seems a first lambda function takes a second lambda function -- somehow?

(\x -> y)(\f -> z)

But this is just a guess.

user253751 user253751 · Accepted Answer · 2021-01-30T00:57:41

The Haskell version is exactly the same as the lambda calculus version but with Haskell syntax:

(\f -> z) (\x -> y)

Why?

let f x = y in z
    ^^^^^^^ "local" function called "f"

let f = (\x -> y) in z
    ^^^^^^^^^^^^^ same thing without the function syntax

We are just introducing a new variable f which holds the value (\x -> y).

How do we introduce a variable in lambda calculus? We define a function and then call it, like this:

(\x.zzzzzzzzzzzzzzzzzzz) 1
    ^^^^^^^^^^^^^^^^^^^ inside this part, x is 1

(lambda calculus doesn't have numbers, but you get the idea)

So we're just introducing a variable called f whose value is (\x.y)

Lambda Calculus let explanation needed

1 Answers