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 mathend000#-Kombinator (λx.xx)(λx.xx) mathend000# hat keinen Typ

• jedes getypte Programm terminiert

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

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