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

Browse archivesActive forum topics 
Recent comments
1 day 3 hours ago
1 day 5 hours ago
1 day 6 hours ago
1 day 13 hours ago
1 day 17 hours ago
1 day 21 hours ago
1 day 21 hours ago
1 day 21 hours ago
1 day 23 hours ago
1 day 23 hours ago