Tagged Questions
10
votes
1answer
468 views
If $f(x)=g(x)$ for all $x:A$, why is it not true that $\lambda x{.}f(x)=\lambda x{.}g(x)$?
There's something about lambda calculus that keeps me puzzled. Suppose we have $x:A\vdash f(x):P(x)$ and $x:A\vdash g(x):P(x)$ for some dependent type $P$ over a type $A$. Then it is not necessarily ...
23
votes
6answers
2k views
Learning Lambda Calculus
What are some good online/free resources (tutorials, guides, exercises, and the like) for learning Lambda Calculus?
Specifically, I am interested in the following areas:
Untyped lambda calculus
...
