Eigenschaften des Typsystems

Wir haben hier den einfach getypten Lambda-Kalkül nachgebaut:

• jedes Programm hat höchstens einen Typ
• nicht jedes Programm hat einen Typ.

  Der Y-Kombinator (λx.xx)(λx.xx) hat keinen Typ

• jedes getypte Programm terminiert

  (Begründung: bei jeder Applikation FA ist der Typ von FA kleiner als der Typ von F)

Übung: typisiere t t t t succ 0 mit succ = \ x -> x + 1 und t = \ f x -> f (f x)