Wir definieren eine Tupeldarstellung für -Terme. Seien M und M_i Lambda-Terme (i>=0), und T und F die -Terme für true und false. Wir definieren dann induktiv

1. [M] : M
2. [M₀,M₁] : z.zM₀M₁, wobei z nicht aus FV(M_i), i=0,1 ist
3. [M₀,M₁, ..., M_n] : [M₀,[M₁, ..., M_n]] für n>=2

Die dazugehörige Projektionsfunktion ist dann
Pⁿ_i : x.xF⁽ⁱ⁾T für 0<=i<n, und
Pⁿ_n : x.xF⁽ⁿ⁾, wobei
F⁽ⁱ⁾ i-mal F bedeuten soll.

Man gebe die Reduktionsketten und die Normalformen an für

1. P²₀[x,y,z]
2. P²₁[x,y,z]
3. P²₂[x,y,z]

Beweisen Sie für 0<=i<=n : Pⁿ_i[M₀,M₁, ..., M_n] = M_i

Gegeben sei das Programm

begin
  var a: real;
  proc p(x,y): 
    begin
      var b: real;
      b := x + y;
      if b<5 then p(b,x);
    end; 
  a := 1; 
  p(a,a); 
end. 
      

Zeigen Sie durch Anwenden der Kopierregel (call by name, static scoping), das bei der Ausführung des Programms zu einem Zeitpunkt gleichzeitig drei Inkarnationen der Prozedur p und damit alle Kopien der lokalen Variable b benötigt werden. Welche Werte haben die Inkarnationen dann?

Wir hatten gesehen, das für -Terme M,N gilt MN => M=N. Gilt auch die Umkehrung?

Entwickeln Sie (mit Hilfe des Y-Kombinators) -Terme für die induktiv definierten Funktionen

1.  für n <= 1 :   F(n) := 1
    für n > 1  :   F(n) := F(n-1) + F(n-2)
   	  

2.  für n = 0 :    F(n) := 1
    für n > 0 :    F(n) := n + F(n-1)