Pages: 1 2 [3] 4   Go Down
Print
Author Topic: Aiuto esercizio Lambda-calcolo  (Read 10120 times)
0 Members e 1 Utente non registrato stanno visualizzando questa discussione.
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 3.079



WWW
« Reply #30 on: 31-03-2013, 19:51:37 »

http://www.itu.dk/people/sestoft/lamreduce/lamframes.html controllate i risultati qua.

P.S.
le espressioni si scrivono così:  (\x.x x) a

Carino.

Peccato che non permetta all'utente, in modalita' single-step, di scegliersi lui il redex da ridurre di volta in
volta. Il codice sicuramente sara' disponibile.
Magari qualcuno di voi potrebbe estenderlo.

Salutissimi
FB
Logged
Joe
Apprendista Forumista
**
Offline Offline

Posts: 492


« Reply #31 on: 02-04-2013, 08:12:01 »

Mi pare di si.

Salutissimi
FB

La ringrazio.
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 3.079



WWW
« Reply #32 on: 02-04-2013, 10:50:29 »

Salve a tutti, ho bisogno di un aiuto riguardo la riduzione in forma normale di una lambda espressione. Innanzitutto vi chiedo se sono corrette le seguenti riduzioni:

1) (\lambda x.yy)(\lambda z.z) x))
       
  • (\lambda x.yy)x
  • yy

2) (\lambda x.((\lambda y.z)x))(\lambda x.xx)(\lambda x.xx))
   
  • (\lambda a.((\lambda y.z)a))\Omega
  • (\lambda a.z)\Omega
  • z

L'aiuto che vi chiedo è, ad esempio, su questa (spiegandomi i passaggi):  testate testate testate

(\lambda xxxx.xx)(\lambda x.xx)(\lambda x.x)y((\lambda x.x)x)

1 OK
2 OK

Se non sbaglio  è l'esercizio che abbiamo fatto in aula ieri..  Ricopio dai miei appunti...

(\lambda xxxx.xx)(\lambda x.xx)(\lambda x.x)y((\lambda x.x)x)

Riscriviamo il lambda termine nel seguente modo

 \left{[(\lambda a.\begin{matrix} \underbrace{( \lambda b.\lambda c.\lambda x. xx)}_{M} \end{matrix}\begin{matrix}\underbrace{(\lambda x.xx)}_{N}\end{matrix}]y \right} x

Quindi..

\left{[(\lambda b.\begin{matrix} \underbrace{(\lambda c.\lambda x.xx)}_{M} \end{matrix}\begin{matrix}\underbrace{(\lambda x.x)}_{N}\end{matrix}]y\right}x


Riduciamo ancora..

\left[(\lambda c.\lambda x.xx)y\right]x

E ancora...

(\lambda x.xx)x

Infine otteniamo  xx

Grazie mille, l'ho appena rifatto e mi risulta  (qui il prof. aveva spiegato i passaggi). Mi facevano confondere tutte quelle parentesi, ma ho capito che alcune di quelle le aggiungeva il prof. per delimitare le redex).
Ora provo a fare la seconda espressione che avevo chiesto e posto eventualmente la soluzione.

Si, pero' nella sequenza di riduzione hai saltato dei passi iniziali.
Ti sei scordato il termine (\x.x) nel primo passaggio (poi fortunatamente riapparso per magia
nel secondo passaggio).
E non hai detto che hai ridotto il termine piu' a destra per ottenere x.

Salutoni
FB
Logged
Joe
Apprendista Forumista
**
Offline Offline

Posts: 492


« Reply #33 on: 02-04-2013, 11:05:13 »

Salve prof., vorrei chiederle se domani a lezione , prima di andare avanti, potremmo svolgere gli esercizi 3, 12 e 14 (qui presenti) riguardanti il lambda-calcolo tipato, in quanto non ho ben chiaro come procedere. La ringrazio infinite.
Logged
Joe
Apprendista Forumista
**
Offline Offline

Posts: 492


« Reply #34 on: 02-04-2013, 15:06:20 »

Salve prof., vorrei chiederle se domani a lezione , prima di andare avanti, potremmo svolgere gli esercizi 3, 12 e 14 (qui presenti) riguardanti il lambda-calcolo tipato, in quanto non ho ben chiaro come procedere. La ringrazio infinite.

 

Rimetto in vista il post.
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 3.079



WWW
« Reply #35 on: 02-04-2013, 19:10:09 »

Salve prof., vorrei chiederle se domani a lezione , prima di andare avanti, potremmo svolgere gli esercizi 3, 12 e 14 (qui presenti) riguardanti il lambda-calcolo tipato, in quanto non ho ben chiaro come procedere. La ringrazio infinite.

OK
Logged
Acicatena86
Apprendista Forumista
**
Offline Offline

Gender: Male
Posts: 404


See full me now who neon


« Reply #36 on: 10-04-2013, 09:17:21 »

Salve professore, il seguente esercizio è corretto?

Fornire una derivazione nel sistema di tipi a' la Curry per il termine \lambda x.\lambda y.x

\overline{ B |- x:a}  \overline{B |-y:b}

\overline{ B |- \lambda y.x:b->a}

\overline{B|- \lambda x.\lambda y.x:a->b->a}

Dove  B=\left{x:a,y:b\right}
« Last Edit: 10-04-2013, 09:20:18 by Acicatena86 » Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 3.079



WWW
« Reply #37 on: 10-04-2013, 13:46:44 »

Salve professore, il seguente esercizio è corretto?

Fornire una derivazione nel sistema di tipi a' la Curry per il termine \lambda x.\lambda y.x

\overline{ B |- x:a}  \overline{B |-y:b}

\overline{ B |- \lambda y.x:b->a}

\overline{B|- \lambda x.\lambda y.x:a->b->a}

Dove  B=\left{x:a,y:b\right}

Corretto.

FB
Logged
Joe
Apprendista Forumista
**
Offline Offline

Posts: 492


« Reply #38 on: 11-04-2013, 07:50:24 »

Salve prof., sto cercando di svolgere l'esercizio 14 sul lambda-calcolo tipato:

"Fornire la coppia principale (Principal Pair) nel sistema di tipi a' la Curry per il lambda termine y(\x.x) . Motivare la risposta."

Ho fatto così:

pp(y) = <{y : a}, a>

Adesso devo trovare la coppia principale di (\lambda x.M), nel nostro caso (\lambda x.x). Mi trovo la coppia principale di x:

pp(x) = <{x:b}, b>

x è una variabile libera in M cioè in x, quindi: pp(\lambda x.x) = <\phi, b -> b>

E' corretto quanto finora fatto? Se si, come dovrei procedere per trovare pp(y(\lambda x.x))?
La ringrazio per il suo chiarimento.
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 3.079



WWW
« Reply #39 on: 11-04-2013, 09:21:13 »

Salve prof., sto cercando di svolgere l'esercizio 14 sul lambda-calcolo tipato:

"Fornire la coppia principale (Principal Pair) nel sistema di tipi a' la Curry per il lambda termine y(\x.x) . Motivare la risposta."

Ho fatto così:

pp(y) = <{y : a}, a>

Adesso devo trovare la coppia principale di (\lambda x.M), nel nostro caso (\lambda x.x). Mi trovo la coppia principale di x:

pp(x) = <{x:b}, b>

x è una variabile libera in M cioè in x, quindi: pp(\lambda x.x) = <\phi, b -> b>

E' corretto quanto finora fatto? Se si, come dovrei procedere per trovare pp(y(\lambda x.x))?
La ringrazio per il suo chiarimento.

No, non hai applicato correttamente il passo dell'algoritmo che produce, se esiste,
il pp di un'applicazione dati i pp dei termini applicati. Controlla con attenzione e fammi sapere.

Salutoni
FB
Logged
Joe
Apprendista Forumista
**
Offline Offline

Posts: 492


« Reply #40 on: 11-04-2013, 18:27:41 »

Salve prof., sto cercando di svolgere l'esercizio 14 sul lambda-calcolo tipato:

"Fornire la coppia principale (Principal Pair) nel sistema di tipi a' la Curry per il lambda termine y(\x.x) . Motivare la risposta."

Ho fatto così:

pp(y) = <{y : a}, a>

Adesso devo trovare la coppia principale di (\lambda x.M), nel nostro caso (\lambda x.x). Mi trovo la coppia principale di x:

pp(x) = <{x:b}, b>

x è una variabile libera in M cioè in x, quindi: pp(\lambda x.x) = <\phi, b -> b>

E' corretto quanto finora fatto? Se si, come dovrei procedere per trovare pp(y(\lambda x.x))?
La ringrazio per il suo chiarimento.

No, non hai applicato correttamente il passo dell'algoritmo che produce, se esiste,
il pp di un'applicazione dati i pp dei termini applicati. Controlla con attenzione e fammi sapere.

Salutoni
FB

Purtroppo prof. non sono riuscito a concluderlo l'esercizio. Magari potremmo svolgerlo domani a lezione,  così ho tutto più chiaro? E' l'esercizio 14. La ringrazio infinite.
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 3.079



WWW
« Reply #41 on: 11-04-2013, 18:34:32 »

OK

FB
Logged
golvellius
Apprendista Forumista
**
Offline Offline

Posts: 124


« Reply #42 on: 15-04-2013, 12:59:03 »

Buongiorno, anche io ho difficoltà con l'esercizio n°14 sul lambda-calcolo tipato e essendo uno studente lavoratore non ho proprio modo di seguire le lezioni.

Volevo chiedere gentilmente se qualcuno può postare un po' quello che è stato fatto a lezione circa questo esercizio, perché sto avendo qualche difficoltà.

Vi ringrazio
Buona giornata.
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 3.079



WWW
« Reply #43 on: 15-04-2013, 14:49:05 »

Buongiorno, anche io ho difficoltà con l'esercizio n°14 sul lambda-calcolo tipato e essendo uno studente lavoratore non ho proprio modo di seguire le lezioni.

Volevo chiedere gentilmente se qualcuno può postare un po' quello che è stato fatto a lezione circa questo esercizio, perché sto avendo qualche difficoltà.

Forza!!!
L'abbiamo fatto praticamente due volte a lezione.
Qualcuno dia una mano al collega.

FB
Logged
Acicatena86
Apprendista Forumista
**
Offline Offline

Gender: Male
Posts: 404


See full me now who neon


« Reply #44 on: 15-04-2013, 22:20:13 »

Buongiorno, anche io ho difficoltà con l'esercizio n°14 sul lambda-calcolo tipato e essendo uno studente lavoratore non ho proprio modo di seguire le lezioni.

Volevo chiedere gentilmente se qualcuno può postare un po' quello che è stato fatto a lezione circa questo esercizio, perché sto avendo qualche difficoltà.

Vi ringrazio
Buona giornata.

Allora, abbiamo  y(\lambda x.x)

per prima cosa, l'algoritmo trova il tipo più semplice possibile per y, poichè y è una variabile, il tipo più semplice è  <y:\psi,\psi>

Adesso l'algoritmo trova il tipo più semplice possibile per \lambda x.x, per farlo, trova il tipo di x.
Il tipo più semplice di x è <x:\phi,\phi>

Tornando al nostro \lambda x.x, essendo un'applicazione, dove le variabili di M sono libere, il tipo più semplice possibile è <\emptyset , \phi \to \phi>

Adesso, dobbiamo fare una sostituzione, in maniera tale da poter applicare correttamente il secondo termine ad y.

La sostituzione più semplice possibile è quella di dare a y un tipo freccia, che ha come dominio il tipo di \lambda x.x.
Quindi <y:(\phi \to \phi)\to \tau,\tau>


Adesso dobbiamo unire le due basi, essendo una vuota, l'unione delle basi è data dalla base di y. Quindi in definitiva il principal pair è

<y:(\phi \to \phi)\to \tau,\tau>

Spero sia stato esaustivo e chiaro!
Logged
Pages: 1 2 [3] 4   Go Up
Print
Jump to: