A.A. 2002-03

Linguaggi di Programmazione I: Paradigmi

secondo “esonero”

data di assegnazione: 24 aprile 2003 data di consegna: 5 maggio 2003

Indichiamo con \overline{n} la codifica di Church di un numero naturale n. Ricordiamo che in ML \overline{n} ha tipo ('a -> 'a) -> ('a -> 'a). Abbiamo visto che, dati due numeri di Church \overline{n} ed \overline{m}, il termine \overline{n}(\overline{m}) denota il numero di Church \overline{m^{n}}. Una funzione ML che dato \overline{n} calcolasse \overline{n^{n}} avrebbe dunque la forma fn x ⇒ x x. Sappiamo tuttavia che tale termine non è tipabile in ML. Ciò è invece possibile in F 2! Sia strip la funzione definita induttivamente sui termini di F 2 che elimina le annotazioni sui tipi:

strip (k) = k
strip (x) = x
strip (λ x : A . M) = fn x ⇒ strip (M)
strip (M N) = strip (M) strip (N)
strip (Λ X . M) = strip (M)
strip (M A) = strip (M)

Trovare un termine M di F 2 tale che strip (M) = fn x ⇒ x x.

Per la lode. Dunque, usando un tale termine, si dovrebbe poter scrivere in F 2 un termine che, se strippato ed eseguito con la semantica del lambda calcolo, va in loop … o no?