0

I'm stuck on how to do this reduction, I have read this post and this pdf but I can't seem to find a solution: (λx.yx)((λy.λt.yt)zx)=> (λx.yx)(λt.zxt) => y(λt.zxt)

but the solution should be yx according to online solvers.

could someone explain what passages I am doing wrong? What are the passages that you should follow to do it right?

Praisethefab
  • 11
  • 3

2 Answers2

0

applicative order

β y := z

(λx.yx)((λy.λt.yt)zx) 
          =    =  =

(λx.yx)((λt.zt)x)

β t := x

(λx.yx)((λt.zt)x)
          =  = =

(λx.yx)(zx)

β x := zx

(λx.yx)(zx)
  =  = ====

y(zx)
Mulan
  • 129,518
  • 31
  • 228
  • 259
-1

A friend of mine had this solution that apperently corresponds to the real answer:

(λx.yx)((λy.λt.yt)zx) => y(((λy.λt.yt)z)x) => y((λt.zt)x) => y(zx) => yzx

my error would have been that I resolved the lambda as if (λx.yx)((λy.λt.yt)(zx)), I considered zx as a singol block not knowing that by default they aren't and that you need parenteses to specify it. Only question that remains is why the professor answer yzx is different from the online answer yx.

Praisethefab
  • 11
  • 3
  • 2
    “y(zx) => yzx” is incorrect. [Lambda calculus is left-associative](https://en.wikipedia.org/wiki/Lambda_calculus#Notation), so yzx = (yz)x, which is not the same as y(zx). – rob mayoff Jul 07 '22 at 15:01