Tutorial 1 – 18.10.2006

Lambda Calculus

  • Lambda terms

    • inductive definition
    • recursive functions: size, free variables, closed terms
    • structural induction: proving a simple property |fv(t)| <= size(t)
    • concrete syntax: strings of characters
    • abstract syntax: abstract syntax trees
  • Reduction relation (call-by-value)

    • inductive definition
    • values = abstractions
    • deterministic – without proof
      (i.e induction on the structure of the derivation)
  • Evaluation Relation

    • reflexive transitive closure of the reduction relation
    • success evaluation -> value
    • stuckness – only for open terms here
    • divergence – omega

back to the tutorial page


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s

%d bloggers like this: