Basic notation in lambda calculus - Computer Science Stack Exchange most recent 30 from cs.stackexchange.com 2019-09-17T00:26:38Z https://cs.stackexchange.com/feeds/question/70477 https://creativecommons.org/licenses/by-sa/4.0/rdf https://cs.stackexchange.com/q/70477 2 Basic notation in lambda calculus Agnivesh Singh https://cs.stackexchange.com/users/66496 2017-02-18T17:13:38Z 2017-02-19T14:57:48Z <p>I have started learning lambda calculus from the book by Hindley and Seldin.</p> <p>It brought up the concept with the function $x-y$, first as a function of $x$ and then as a function of $y$. In a way, it emphasized the difference between treating the expression as a function of $x$ and function of $y$, giving separate names to the functions.</p> <p>$$f(x,y) = x-y \qquad\text{and}\qquad g(y,x) = x -y$$ and, in $\lambda$ notion, $$h = \lambda xy.x-y \qquad\text{and}\qquad g = \lambda yx. x-y\,.$$</p> <p>If I am not wrong then it can be inferred that $f =\lambda x .(x-y)$ means that while computing the value of the expression the expression will vary only with $x$ and similarly when $\lambda$ is placed with $x$ the other variable $y$ will be kept as a constant.</p> <p>But then it said that this can be denoted as, with $h$ being the common name of the function $$h = \lambda xy.(x-y)\qquad\text{and}\qquad h = \lambda yx.(x-y)\,.$$<br> Is it so that in the above expression the variable which is adjacent to $\lambda$ receives the value and the other one is constant? The above function is called a two-place function; what does that mean?</p> <p>Then he introduces the following function in $\lambda$ notation calling it a one-point function: $$h^\star = \lambda x .(\lambda y . x−y)$$ and says that, for each number $a$, we have $h^\star(a)=\lambda y . a−y$. Here $a$ is being provided as an argument but $\lambda$ is placed near $y$. Why is this?</p> <p>And then it deduces that $(h^\star(a))(b)=(\lambda y . a−y)(b) = a−b = h(a,b)$ and says $h^\star$ can be viewed as "representing" $h$. Is "representing" a technical term? How was $(\lambda y . a−y)(b) = a−b$ concluded?</p> https://cs.stackexchange.com/questions/70477/-/70481#70481 2 Answer by Aristu for Basic notation in lambda calculus Aristu https://cs.stackexchange.com/users/34010 2017-02-18T18:50:27Z 2017-02-19T14:25:41Z <blockquote> <p>If I am not wrong then it can be inferred that :</p> <p>$f=\lambda x.(x−y)$ means that while computing the value of the expression the expression will vary only with "x" and similarly when "lambda " is placed with x the other variable y" will be kept as a constant .</p> </blockquote> <p>Yes, intuitively that's how it works. </p> <hr> <p>What you're looking is called <a href="https://en.wikipedia.org/wiki/Currying" rel="nofollow noreferrer">Currying</a> and it's explained fairly early in this book (in fact, I think it's the next section but I don't have a copy now to check). So when we want to work with functions with many arguments we often do it like this:</p> <p>$$f(x,y,z) = x\times y + z$$</p> <p>But you can break this into simpler functions, $(x \times y)$ and $(+z)$. The multiplication can be broken into even simpler terms, first I provide $x$, then just multiply by $y$, that is, $f^{\star}(y) = x\times y$. </p> <p>Defining some 1-argument functions:</p> <p>\begin{align*} plus_z &amp;:= f^\prime(s) = s + z\\ times_y &amp;:= f^\star(s) = s\times y \end{align*}</p> <p>Combining these we can rewrite $f$ as:</p> <p>$$f(x,y,z) = f^\prime(f^\star(x)) = plus_z (times_y ~ x)$$ </p> <p>Writing this in using $\lambda$ we have:</p> <p>$$\lambda x y z. (x\times y + z) \equiv \lambda x.\bigg(\lambda y. \Big(\lambda z. (x\times y + z ) \Big) \bigg)$$</p> <p>What the author has shown is that you can take a function with many arguments and transform it into many simpler functions with just one argument, the bigger function is just a composition of the simpler ones. </p> <p>So just how the proof works? In your book the following functions are defined:</p> <p>\begin{align*} h^\star &amp;= \lambda x . (\lambda y . x − y)\\ h(x,y) &amp;= x-y \end{align*}</p> <p>You want to show that $h^\star = h$. To do that just take any two arguments $a$ and $b$. First evaluate $h^\star$ in $a$.</p> <p>$$h^\star(a) = (\lambda x. (\lambda y. x - y))(a) = \lambda y. a - y$$</p> <p>This gives you a simpler one argument function $h^\prime = h^\star(a)$.</p> <blockquote> <p>How was $(λy.a−y)(b)=a−b$ concluded</p> </blockquote> <p>The same way $(\lambda x. (\lambda y. x - y))(a) = \lambda y. a - y$ was concluded. Just evaluate the function in $b$. </p> <p>$$h^\prime(b) = (h^\star(a))(b) = (\lambda y. a - y)(b) = a - b$$</p> <p>Which is the same result computed by $h(a,b) = a - b$. </p>