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

Browse archives
Active forum topics 
Recent comments
6 hours 21 min ago
8 hours 56 min ago
10 hours 27 min ago
11 hours 9 min ago
23 hours 43 min ago
1 day 2 hours ago
1 day 6 hours ago
1 day 8 hours ago
1 day 12 hours ago
1 day 22 hours ago