Pages: [1]   Go Down
Print
Author Topic: Esercizi su alpha-conversione  (Read 266 times)
0 Members e 1 Utente non registrato stanno visualizzando questa discussione.
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.927



WWW
« on: 28-12-2017, 18:30:51 »

Le seguenti coppie di lambda-termini sono alpha-convertibili? Perche'

\t.(tt)(\xy.x(tyy))        \r.(tt)(\xy.x(tyy))

\t.(tt)(\xy.x(tyy))         \r.(rr)(\xy.x(ryy))

\r.(rr)(\xy.x(ryy))          \r.(rr)(\vy.x(rvv))

\r.(rr)(\xy.x(ryy))          \r.(rr)(\wy.w(ryy))

\r.(rr)(\xy.x(ryy))          \r.(rr)(\ww.w(rww))

\r.(rr)(\ww.w(rww))      \r.(rr)(\ws.w(rss))

\r.(rr)(\ww.w(rww))       \r.(rr)(\ws.s(rss))

\r.(rr)(\ws.s(rss))            \r.(rr)(\xs.s(rss))
Logged
luca98
Matricola
*
Offline Offline

Posts: 78



« Reply #1 on: 29-12-2017, 20:18:43 »

numero le coppie da 1 a 8

1) la prima coppia non è alpha-convertibile perchè se cambio \t con \r allora dovranno essere cambiate anche tutte le altre t legate a \t. il secondo lambda termine della coppia dovrebbe essere \r.(rr)(\xy.x(ryy)).

2) la coppia è alpha convertibile poichè cambio \t e le t legate ad esso  con r

3) la coppia non è alpha convertibile poichè cambio si \x in \v, ma viene commesso l'errore di cambiare una variabile diversa da x(le due y alla fine) sempre con v e questo non si può fare. La cosa giusta da fare è cambiare la x legata con v e lasciare le y così come sono... \r.(rr)(\vy.v(ryy)). Le y sono legate al \y.

4)la coppia è alpha-convertibile poichè cambio \x e la x legata ad esso  con w.

5) la coppia non è alpha convertibile. Non posso cambiare sia x e y con la stessa variabile (in questo caso w)

6)la coppia non è alpha convertibile...
\r.(rr)(\ww.w(rww)) può essere scritta anche in questo modo: \r.(rr)(\w.(\w.w(rww)))
da ciò si può capire bene che le w dal "." in poi sono legate al secondo \w e quindi se noi cambiamo quest'ultima in s anche tutte le w che vengono dopo dovranno essere cambiate in s(nel termine presente nel testo la w dopo il punto non è stata cambiata)

7) la coppia è alpha convertibile(soluzione al 6)

Cool la coppia è alpha convertibile poichè viene cambiato \w in \x(non ci sono variabili legate quindi non ho bisogno di sostituire nient'altro)
-----------------------------------------------------------------------------------------------------------------------------------

professore mi corregga se c'è qualcosa che non va...
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.927



WWW
« Reply #2 on: 02-01-2018, 12:30:20 »

professore mi corregga se c'è qualcosa che non va...

Controllare la correttezza delle tue risposte dovrebbe esser compito anche dei tuoi colleghi...


Come ulteriore esercizio, prendi una delle coppie per le quali la risposta e' affermativa
e produci una dimostrazione formale del fatto che siano alpha-convertibili
(cioe' una derivazione nel sistema per l'alpha-conversione indicato nel testo)

Buon Anno!
FB
Logged
Pages: [1]   Go Up
Print
Jump to: