User loginNavigation 
Derivation trees for lambdacalculusHi, 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? Thanks, By ilSignorCarlo at 20071126 22:01  LtU Forum  previous forum topic  next forum topic  other blogs  11984 reads

Browse archives
Active forum topics 
Recent comments
2 weeks 6 days ago
3 weeks 6 days ago
6 weeks 1 day ago
6 weeks 6 days ago
7 weeks 1 hour ago
7 weeks 2 days ago
7 weeks 2 days ago
7 weeks 3 days ago
7 weeks 3 days ago
7 weeks 4 days ago