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  11030 reads

Browse archivesActive forum topics 
Recent comments
16 hours 27 min ago
1 day 1 hour ago
1 day 12 hours ago
1 day 13 hours ago
1 day 13 hours ago
1 day 14 hours ago
1 day 15 hours ago
1 day 17 hours ago
1 day 18 hours ago
1 day 20 hours ago