Home » forums » LtU Forum

Derivation trees for lambda-calculus

Hi,
I am studying lambda-calculus (untyped and typed). My teacher often uses the derivation trees.

For the untyped lambda calculus, such a tree has the following properties:

Starting from any lambda term T, we have:
(I use \ for lambda)
- if T=x, we build a terminal leaf node with label x

- 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,
Carlo

By ilSignorCarlo at 2007-11-26 22:01 | LtU Forum | previous forum topic | next forum topic | other blogs | 13726 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Abstract syntax tree

That's just the abstract syntax tree resulting from parsing the lambda expression. It's just another way of writing the same thing, and doesn't convey any new information.

Wikipedia has a page on inferring types from simple lambda terms: http://en.wikipedia.org/wiki/Type_inference

By Tim Sweeney at Tue, 2007-11-27 20:35 | login or register to post comments

Trees, types, and predictions

There are some examples of this kind of tree in chapter 2 of the Peyton Jones/Lester book Implementing functional languages: a tutorial[*]. But as Tim says, those trees alone won't tell you much about type inference.

For type inference, the Schwartzbach paper linked from the Getting Started thread might be helpful as an intro; the TAPL book (also in that thread) is a much more in-depth treatment.

[*] First featured on LtU in 2000, when Chris Rathman wondered if "MS is actually ever gonna do an FP language implementation?" 7 years later, they're productizing F#, and adding the functional Linq sublanguage into other .NET languages.

By Anton van Straaten at Wed, 2007-11-28 03:28 | login or register to post comments

Tim

As successful as Tim seems, I prefer being me, and I'm willing to bet he prefers being him, but Tim did say what I would've.

By Derek Elkins at Wed, 2007-11-28 03:44 | login or register to post comments

Equivalent up to alpha conversion

Oops, I was thinking of another thread & didn't check who said what. I've performed an alpha rename of Derek for Tim in that comment.

By Anton van Straaten at Wed, 2007-11-28 04:17 | login or register to post comments

AST with types

The trees alone don't tell me much about type inference, but my teacher used to use them with associated types. My problem is that I have the finished tree with all the types in the right place, but I can't understand the process.
I mean: where is the starting point?

Actually I have the same problem with the derivation in the natural deduction style. Does the inference starts from the top towards bottom or vice-versa? Or is it the same?

By ilSignorCarlo at Wed, 2007-11-28 22:03 | login or register to post comments