Derivation trees for lambda-calculus
For the untyped lambda calculus, such a tree has the following properties:
Starting from any lambda term T, we have:
- if t=\x.M, we build a node with label \x with just one son, which is the subtree obtained applying the definition on M
- if T=(MN), we build a node with label @ with two sons. These are the subtrees obtained applying the definition on M and N.
This is not difficult, but I can't find examples of these trees on internet.
For the typed lambda calculus I can't really understand the method to check if a term is well typed or to assign a type to a term. I mean, using the tree system.
Do you know any good source where I can learn how these trees work?
Active forum topics
New forum topics