Pages: [1]   Go Down
Print
Author Topic: variabili libere e legate  (Read 2351 times)
0 Members e 1 Utente non registrato stanno visualizzando questa discussione.
rox
Forumista
***
Offline Offline

Posts: 633


« on: 11-05-2014, 13:25:57 »

Salve a tutti, non ho ben chiaro il concetto di variabile libera e variabile legata. Per esempio se scrivo questa astrazione :
Code:

 λx.x(λy.yx)

l'insieme delle variabili dovrebbero essere x,y
la variabile libera dovrebbe essere y perché è l'input della funzione superiore
la variabile legata dovrebbe essere x perché è la variabile "nascosta" che viene richiamata all'interno della funzione superiore

ho capito bene oppure mi è sfuggita qualcosa?
Logged

Una macchina è in grado di lavorare come cinquanta uomini comuni, ma nessuna macchina può svolgere il lavoro di un uomo straordinario.
ɹǝǝuıƃuǝsɹǝʌǝɹ
Administrator
God of the Forum
*****
Offline Offline

Gender: Male
Posts: 4.475


Più grande è la lotta, e più è glorioso il trionfo


WWW
« Reply #1 on: 11-05-2014, 19:48:52 »

Applichiamo la definizione che trovi sul sito del professore .

Variabili legate:
BV (λx.x(λy.yx)) = {x} ∪ BV (x(λy.yx)) = {x} ∪ BV (x) ∪ BV (λy.yx) = {x} ∪ ∅ ∪ {y} ∪ BV (yx}
= {x} ∪ ∅ ∪ {y} ∪ BV (x) ∪ BV (y) = {x} ∪ ∅ ∪ {y} ∪ ∅ ∪ ∅ = {x, y}

Variabili libere:
FV (λx.x(λy.yx)) = FV (x(λy.yx)) ∖ {x} = (FV (x) ∪ FV (λy.yx)) ∖ {x} = ({x} ∪ (FV (yx) ∖ {y})) ∖ {x}
= ({x} ∪ ((FV (y) ∪ FV (x)) ∖ {y})) ∖ {x} = ({x} ∪ (({y} ∪ {x}) ∖ {y})) ∖ {x} = ({x} ∪ ({y, x} ∖ {y})) ∖ {x}
= ({x} ∪ {x}) ∖ {x} = {x} ∖ {x} = ∅

Ricapitolando:
BV (λx.x(λy.yx)) = {x, y}
FV (λx.x(λy.yx)) = ∅

Se, invece delle definizioni formali, vuoi andare a "intùito", puoi capire perché è così dal seguente ragionamento:
sono libere quelle variabili che non puoi assolutamente rinominare, per alcun motivo, perché sono esse stesse una informazione (con la loro dignità speciale); ti sei accorto della x (come legata), perché, giustamente, se la rinomini (sempre allo stesso modo) ottieni un termine equivalente (almeno nel senso della computazione), cioè quella x viene usata solo come segnaposto per l'argomento effettivo della astrazione funzionale, che, quando usata in una "applicazione" di due termini, quello a sinistra dei quali è proprio il nostro termine, produce un nuovo termine che è dato da quel termine passato come argomento applicato al termine che è una astrazione funzionale che prenderà altre variabili e ci farà qualcos'altro. Quindi la x, evidentemente anche nel corpo della nostra astrazione, certamente non è libera, ma è legata.

Veniamo al caso della y: ecco, se noi provassimo a sostituire la y nella astrazione che verrebbe prodotta eseguendo la computazione, scopriremmo che è solo un segnaposto per una ulteriore sostituzione, in particolare ci ricorda che essa (y) è parte di un termine astrazione di cui è argomento, e che quindi, ai fini della computazione, sarebbe utile solo come segnaposto per una ulteriore computazione (da fare in un ulteriore passo di computazione, qualora ci fosse la possibilità di farlo). Quindi, vediamo che se sostituissimo tutte le occorrenze di y con una qualsiasi altra variabile, non avremmo alcun problema, nel senso della computazione; dunque y è legata.

Siccome le uniche variabili che ci sono sono x e y, e sono entrambe legate, evidentemente non ci sono variabili libere, ed infatti è così .
Logged

La grande marcia della distruzione mentale proseguirà. Tutto verrà negato. Tutto diventerà un credo. È un atteggiamento ragionevole negare l'esistenza delle pietre sulla strada; sarà un dogma religioso affermarla. È una tesi razionale pensare di vivere tutti in un sogno; sarà un esempio di saggezza mistica affermare che siamo tutti svegli. Accenderemo fuochi per testimoniare che due più due fa quattro. Sguaineremo spade per dimostrare che le foglie sono verdi in estate. Non ci resterà quindi che difendere non solo le incredibili virtù e saggezze della vita umana, ma qualcosa di ancora più incredibile: questo immenso, impossibile universo che ci guarda dritto negli occhi. Combatteremo per i prodigi visibili come se fossero invisibili. Guarderemo l'erba e i cieli impossibili con uno strano coraggio. Saremo tra coloro che hanno visto eppure hanno creduto.

In tutto, amare e servire.

  
                            ن                           
I can deal with ads,
I can deal with buffer,
but when ads buffer
I suffer...

...nutrimi, o Signore, "con il pane delle lacrime; dammi, nelle lacrime, copiosa bevanda...

   YouTube 9GAG    anobii  S  Steam T.B.o.I. Wiki [univ] Lezioni private  ʼ  Albo d'Ateneo Unicode 3.0.1
Usa "Search" prima di aprire un post - Scrivi sempre nella sezione giusta - Non spammare - Rispetta gli altri utenti - E ricorda di seguire il Regolamento
rox
Forumista
***
Offline Offline

Posts: 633


« Reply #2 on: 12-05-2014, 18:54:07 »

mmm allora ho capito in questo esempio come si fa a vedere formalmente quali sono le variabili libere e quelle legate(un po' meno ho capito come vederlo ad occhio  testate ) . Applicando la definizione formale in questo caso avrò:
Code:


FV(λz.λx(xy))=FV(λx(xy))\{z}=FV(xy)\{z}\{x}=(({x}U{y})\{z})\{x}={y}\{z}={y}


è corretto quello che ho fatto? 
Logged

Una macchina è in grado di lavorare come cinquanta uomini comuni, ma nessuna macchina può svolgere il lavoro di un uomo straordinario.
ɹǝǝuıƃuǝsɹǝʌǝɹ
Administrator
God of the Forum
*****
Offline Offline

Gender: Male
Posts: 4.475


Più grande è la lotta, e più è glorioso il trionfo


WWW
« Reply #3 on: 12-05-2014, 20:07:04 »

Sì.

Hai omesso un passaggio, e cioè
Quote
FV(λz.λx(xy))=FV(λx(xy))\{z}=FV(xy)\{z}\{x}=(FV(x) U FV(y))\{z}\{x}=(({x}U{y})\{z})\{x}={y}\{z}={y}

che hai implicitato, ma è ok ok.
Logged

La grande marcia della distruzione mentale proseguirà. Tutto verrà negato. Tutto diventerà un credo. È un atteggiamento ragionevole negare l'esistenza delle pietre sulla strada; sarà un dogma religioso affermarla. È una tesi razionale pensare di vivere tutti in un sogno; sarà un esempio di saggezza mistica affermare che siamo tutti svegli. Accenderemo fuochi per testimoniare che due più due fa quattro. Sguaineremo spade per dimostrare che le foglie sono verdi in estate. Non ci resterà quindi che difendere non solo le incredibili virtù e saggezze della vita umana, ma qualcosa di ancora più incredibile: questo immenso, impossibile universo che ci guarda dritto negli occhi. Combatteremo per i prodigi visibili come se fossero invisibili. Guarderemo l'erba e i cieli impossibili con uno strano coraggio. Saremo tra coloro che hanno visto eppure hanno creduto.

In tutto, amare e servire.

  
                            ن                           
I can deal with ads,
I can deal with buffer,
but when ads buffer
I suffer...

...nutrimi, o Signore, "con il pane delle lacrime; dammi, nelle lacrime, copiosa bevanda...

   YouTube 9GAG    anobii  S  Steam T.B.o.I. Wiki [univ] Lezioni private  ʼ  Albo d'Ateneo Unicode 3.0.1
Usa "Search" prima di aprire un post - Scrivi sempre nella sezione giusta - Non spammare - Rispetta gli altri utenti - E ricorda di seguire il Regolamento
rox
Forumista
***
Offline Offline

Posts: 633


« Reply #4 on: 13-05-2014, 09:31:22 »

apposto! ti ringrazio

ma ad occhio come faccio a capire cosa posso sostituire? devo fare tutto il procedimento di cui abbiamo discusso? io negli esercizi vedo che devono essere fatte moltissime sostituzioni… per farle se ho ben capito serve sapere se ci sono variabili libere e se diventano legate dopo la loro sostituzione...
« Last Edit: 13-05-2014, 15:31:29 by rox » Logged

Una macchina è in grado di lavorare come cinquanta uomini comuni, ma nessuna macchina può svolgere il lavoro di un uomo straordinario.
Pages: [1]   Go Up
Print
Jump to: