Citiți cu atenție capitolul despre programare funcțională din notele de curs.
Exerciții propuse:
Definiți un interpretor pentru λ-calcul în Coq și testați
implementarea pe câteva exemple interesante.
(1 punct) Definiți sintaxa pentru λ-calcul.
(1 punct) Definiți cele două tipuri de substituții (cea care nu
evită capturarea și cea care evită capturarea).
(1 punct) Definiți regula de β-reducere.
(1 punct) Implementați strategia CBN și testați această strategie
pe 2 exemple netriviale.
(1 punct) Implementați strategia CBV și testați această strategie
pe 2 exemple netriviale.
(3 puncte) Formulați și demonstrați o teoremă de
confluență pentru lambda calcul (adică, demonstrați că dacă o
λ-expresie e se reduce atât la e1 cât și la
e2, atunci există e' astfel încât
e1 și e2 se reduc la e').
