Hi so im really struggling right now with the lambda calculus. It doesnt make sense to me.

So i know that ($\lambda x \to x)(y)$ means i have a function which takes a number to itself. The confusing part hits in when i see something like

$(\lambda x \to gx)x$

Does this mean i have a function which takes an x and outputs g and i should apply it to x?

or does it mean i have an a function which takes an x and outputs gx ? My book says that {$g,x$} are free variables. What would that mean concretely. Im looking for intuition, nothing is making sense. :C

• Can you tell us what book you are using, please. Does it really use $\to$ in its notation for $\lambda$-terms? – Rob Arthan Mar 6 '17 at 21:26
• yes im using a script my university offers.its not really a book i can link if you want to see it. – asddf Mar 6 '17 at 21:28
• Don't worry about the link, but does it really use the notation $\lambda x \to gy$? (When the rest of the world writes $\lambda x.gy$ or $\lambda x \cdot g y$ or, when they're not thinking about $\lambda$-calculus, $x \mapsto gy$.) – Rob Arthan Mar 6 '17 at 21:32
• yes it does use the notation with an arrow. Do you know any other sources you could recommend for the lambda calculus ? – asddf Mar 6 '17 at 21:34
• Here's a list off the top of my head: the Wikipedia page isn't bad and will lead you too lots of other references. The book "The Lambda Calculus" by Barendregt is a very comprehensive reference (perhaps too comprehensive if you are new to the subject). Jesse Alama's article in the Stanford Encyclopaeida of Philosophy is good as is Mike Gordon's book "Programming theory and its applications". – Rob Arthan Mar 6 '17 at 21:52

No, $(\lambda x\to x)$ is a function that takes a number (or, indeed, anything whether or not it is a number) to itself. When you say $(\lambda x\to x)y$ you're applying that function to $y$ (whatever $y$ is), and the result of that is just $y$.

In $(\lambda x\to gx)$ you have a function that takes something and returns the value of $g$ applied to that something -- as you describe it, a function that takes $x$ and produces $gx$.

However, again, when you write $(\lambda x\to gx)x$ you have taken the function just described and applied it to $x$, which would produce $gx$.

The statement that $g$ and $x$ are free variables means that the expression "$(\lambda x\to gx)x$" doesn't really have a value before you decide what the value of the variables $g$ and $x$ are going to be. It's a recipe for doing something with a thing you call $g$ and a thing you call $x$, but you can't really do it before you have decided what those things are going to be.

Note, by the way, that in $(\lambda x\to gx)x$ you have two different $x$ around. If we write it $(\lambda x_1\to gx_1)x_2$, the two ones shown as $x_1$ is just a dummy variable that tells you what the function does with its argument, whereas the $x_2$ is the free variable whose value you're supposed to decide.

• Is the thing you did at the end an alpha conversion?, btw thank you a lot for helping me its a lot clearer now ! – asddf Mar 6 '17 at 19:24
• @asddf: Yes, exactly -- except that we're not supposed to $\alpha$-convert the free variable! But your $(\lambda x.gx)x$ is $\alpha$-equivalent to $(\lambda y.gy)x$. I was holding back on the fancy word in case you hadn't encountered it yet. – Henning Makholm Mar 6 '17 at 19:31
• Just one last question: $\lambda x y \to t$ means that my function requires two variables ? – asddf Mar 6 '17 at 19:45
• @asddf No. For example $(\lambda xy \to t)r$ reduces to $(\lambda y \to t)$. Another, $(\lambda xyz \to axbyczd)r$ reduces to $(\lambda yz \to arbyczd)$. $\lambda xy \to t$ is just an abbreviation for $\lambda x \to (\lambda y \to t)$. – DanielV Mar 6 '17 at 20:39
• @asddf: It is simply a convention that this is what is meant when there are two or more letters after the $\lambda$. Formally only a single letter after the $\lambda$ is allowed; writing $\lambda x\to\lambda y\to t$ as $\lambda xy\to t$ is nothing more than a convenient abbreviation for the former. – Henning Makholm Mar 6 '17 at 20:50