Pages: [1]   Go Down
Print
Author Topic: principal pairs ... spolveratina  (Read 749 times)
0 Members e 1 Utente non registrato stanno visualizzando questa discussione.
TuTToWeB
Apprendista Forumista
**
Offline Offline

Posts: 102


« on: 06-06-2012, 17:28:26 »

salve a tutti,
ho dato una spolverata all'algoritmo per trovare le coppie principali in un lambda termine.
Ho creato io un piccolo lambda termine, tipabile, e vorrei condividere con voi la soluzione anche per vedere se ho commesso degli errori e di avere magari l'occasione di parlarne domani in aula se ci sono dei problemi

(\x.ax)c

per pp((\x.ax)c) ci serve pp(\x.ax) e pp(c) e poi unificare

procediamo ricorsivamente
pp(c) = <c:sigma, sigma>

per pp(\x.ax) ci serve pp(ax), procediamo ancora una volta ricorsivamente

per pp(ax) dobbiamo avere pp(a) e pp(x) e poi unificare

pp(x) = <x:phi, phi>

pp(a) = <a:tau -> omega, tau->omega>

unify tau->omega phi = S1[tau |-> phi]

unifyBasis S1{a:tau->omega} S1{x:phi} = unifyBasis {a:phi->omega} {x:phi} = unifyBasis empty <x:phi> = S2[phi->phi]

questa è una sostituzione identica, ma non la consideriamo per semplicità

pp(ax) = <{a:phi->omega,x:phi}, omega}

pp(\x.ax) = (poiché x non è in FV(ax)) <{a:phi->omega,x:phi}, phi->psi >



per pp( (\x.ax)c ) bisogna unificare i tipi e i tipi presenti nelle due basi

unify phi->psi sigma = S3[phi |-> sigma]

unifyBasis S3{a:phi->omega,x:phi} S3{c:sigma} =
= unifyBasis {a:sigma->omega, x:sigma} {c:sigma} =
=unifyBasis {x:sigma} {c:sigma} = unifyBasis empty {sigma} = S4[sigma |-> sigma] (anche questa  è una sostituzione identica e non la consideriamo per semplicità)

pp( (\x.ax)c) = <{a:sigma->omega,x:sigma,c:sigma}, omega>

spero di esser stato quanto più chiaro possibile (ne dubito Smiley ) e spero di non aver saltato dei passaggi a trascrivere dai foglietti Smiley

a presto
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 3.072



WWW
« Reply #1 on: 06-06-2012, 20:13:22 »

Non ho visto dov'e' l'errore (controlliamo domani a lezione con calma),
ma sicuramente c'e': infatti la x e' legata e non puo' comparire nella base principale.

Salutoni
FB
Logged
Brennan
Matricola
*
Offline Offline

Posts: 46



« Reply #2 on: 06-06-2012, 23:53:57 »


pp(\x.ax) = (poiché x non è in FV(ax)) <{a:phi->omega,x:phi}, phi->psi >


non mi vorrei sbagliare ma ci sono due errori qui: x è in FV(ax) e quindi va fuori dalla base, e poi il tipo più generale dovrebbe essere phi->omega. Quindi pp(\x.ax) = <{a:phi->omega}, phi->omega >

inoltre :


pp(a) = <a:tau -> omega, tau->omega>


perché hai scelto di assegnare un tipo freccia in questo caso?

« Last Edit: 07-06-2012, 12:00:32 by Brennan » Logged
Pages: [1]   Go Up
Print
Jump to: