Benvenuto!
Accedi
o
registrati
.
09-12-2019, 14:45:19
Home
CDL Informatica
UniCT
CEA
Prof
Help
Search
Calendar
Login
Register
Forum Informatica Unict
»
LAUREA MAGISTRALE
»
Corsi disattivati - Vecchio curriculum
»
Linguaggi di Programmazione, 9 CFU
(Moderator:
Franco Barbanera
) »
Come "costruire" la base nel λ-calcolo tipato a' la Curry
Pages: [
1
]
Go Down
« precedente
successivo »
Print
Author
Topic: Come "costruire" la base nel λ-calcolo tipato a' la Curry (Read 1971 times)
0 Members e 1 Utente non registrato stanno visualizzando questa discussione.
andyusa83
Apprendista Forumista
Offline
Gender:
Posts: 232
Come "costruire" la base nel λ-calcolo tipato a' la Curry
«
on:
15-05-2014, 18:57:18 »
Salve a tutti,
sto cercando di svolgere esercizi del tipo:
Code:
Fornire una derivazione nel sistema di tipi a' la Curry per il termine
λbc.((λy.c)(bc))
C'è la soluzione per l'esercizio indicato (n° 11) ma non riesco a capire come vengono "costruite" le basi da cui partire per dare i giudizi sui vari sottotermini. Ad esempio la soluzione inizia così:
Code:
b:t1->t2,c:t1, y:t2 |- c:t1 b:t1->t2,c:t1 |- b:t1->t2 b: t1->t2, c: t1 |- c: t1
------------------------------ -------------------------------------------------------
b:t1->t2, c:t1 |- λy.c:t2->t1 b: t1->t2, c: t1 |- (bc): t2
e i passaggi sono banali ma come si determinano le basi? Ad occhio? (Non penso proprio.)
E poi, perché la b compare nella base a sinistra nonostante non sia necessaria all'inizio mentre la y non compare a destra? È solo una scelta arbitraria per averla più avanti quando si dovrà dare un giudizio sul termine più esterno?
Ringrazio anticipatamente chiunque risponda.
Saluti.
«
Last Edit: 15-05-2014, 19:01:45 by andyusa83
»
Logged
Franco Barbanera
Moderator
Forumista Eroico
Offline
Posts: 3.081
Re:Come "costruire" la base nel λ-calcolo tipato a' la Curry
«
Reply #1 on:
16-05-2014, 14:53:27 »
Quote
E poi, perché la b compare nella base a sinistra nonostante non sia necessaria all'inizio mentre la y non compare a destra? È solo una scelta arbitraria per averla più avanti quando si dovrà dare un giudizio sul termine più esterno?
Si.
FB
Logged
andyusa83
Apprendista Forumista
Offline
Gender:
Posts: 232
Re:Come "costruire" la base nel λ-calcolo tipato a' la Curry
«
Reply #2 on:
16-05-2014, 16:53:30 »
Quote from: Franco Barbanera on 16-05-2014, 14:53:27
Quote
E poi, perché la b compare nella base a sinistra nonostante non sia necessaria all'inizio mentre la y non compare a destra? È solo una scelta arbitraria per averla più avanti quando si dovrà dare un giudizio sul termine più esterno?
Si.
FB
Grazie, professore, ma tornano alla questione principale, come faccio a determinare le basi di partenza?
Logged
Franco Barbanera
Moderator
Forumista Eroico
Offline
Posts: 3.081
Re:Come "costruire" la base nel λ-calcolo tipato a' la Curry
«
Reply #3 on:
19-05-2014, 17:33:53 »
Nelle basi di partenza debbono esserci le variabili libere del termine finale
piu' quelle che verranno via via legate nei punti in cui si utilizzera' la regola
di (--> I).
FB
Logged
andyusa83
Apprendista Forumista
Offline
Gender:
Posts: 232
Re:Come "costruire" la base nel λ-calcolo tipato a' la Curry
«
Reply #4 on:
19-05-2014, 21:57:32 »
Quote from: Franco Barbanera on 19-05-2014, 17:33:53
Nelle basi di partenza debbono esserci le variabili libere del termine finale
piu' quelle che verranno via via legate nei punti in cui si utilizzera' la regola
di (--> I).
FB
Ma come si stabiliscono i tipi delle variabili (libere o legate che siano) da mettere nelle basi iniziali? È questo che non riesco a capire.
Logged
Franco Barbanera
Moderator
Forumista Eroico
Offline
Posts: 3.081
Re:Come "costruire" la base nel λ-calcolo tipato a' la Curry
«
Reply #5 on:
20-05-2014, 10:52:22 »
Se segui pedissequamente l'algoritmo pp, e' lui che le costruisce man mano.
Ma per termini semplici si puo' ovviamente fare ad occhio.
Per esempio, se il termine e' xyz e' ovvio che x deve avere come tipo una freccia
che ha come codominio una freccia.
Quindi occorre (cosa per cui si fanno gli esercizi) quel minimo di dimestichezza
con il sistema di assegnamento di tipi per riuscire a capire quali tipi utilizzare.
FB
Logged
andyusa83
Apprendista Forumista
Offline
Gender:
Posts: 232
Re:Come "costruire" la base nel λ-calcolo tipato a' la Curry
«
Reply #6 on:
21-05-2014, 17:48:37 »
Quote from: Franco Barbanera on 20-05-2014, 10:52:22
Se segui pedissequamente l'algoritmo pp, e' lui che le costruisce man mano.
Ma per termini semplici si puo' ovviamente fare ad occhio.
Per esempio, se il termine e' xyz e' ovvio che x deve avere come tipo una freccia
che ha come codominio una freccia.
Quindi occorre (cosa per cui si fanno gli esercizi) quel minimo di dimestichezza
con il sistema di assegnamento di tipi per riuscire a capire quali tipi utilizzare.
FB
Grazie Prof, ho applicato l'algoritmo pp (sul quale tra l'altro ho alcuni dubbi) ma continuo a non capire: non si dovrebbe iniziare con tipi semplici per tutte le variabili e via via eliminare dalla base quelle che si legano e assegnare i tipi alle varie applicazioni e lambda-astrazioni che si presentano? Lo chiedo perché nella soluzione dell'esempio citato si parte già con un tipo freccia per la variabile b: t1->t2.
Mi sembra strano infatti alla fine il risultato proposto è: (t1->t2)->t1->t1, quando ad occhio, considerando che il termine che il termine λbc.((λy.c)(bc)) è riducibile a λbc.c, dovrebbe venire t2->t1->t1, o una sua sostituzione.
Sicuramente la soluzione proposta è giusta e mi sta sfuggendo qualcosa ma al momento non capisco cosa.
Logged
Franco Barbanera
Moderator
Forumista Eroico
Offline
Posts: 3.081
Re:Come "costruire" la base nel λ-calcolo tipato a' la Curry
«
Reply #7 on:
22-05-2014, 15:12:43 »
L'esercizio chiede il tipo principale di
λbc.((λy.c)(bc))
NON di
λbc.c
Nel termine
λbc.((λy.c)(bc))
il tipo del dominio (il tipo di b) deve essere per forza una freccia,
poiche' all'interno del termine la variabile b viene applicata a c
e questo si puo' fare solo se b ha un tipo freccia.
FB
Logged
andyusa83
Apprendista Forumista
Offline
Gender:
Posts: 232
Re:Come "costruire" la base nel λ-calcolo tipato a' la Curry
«
Reply #8 on:
22-05-2014, 23:05:42 »
Quote from: Franco Barbanera on 22-05-2014, 15:12:43
L'esercizio chiede il tipo principale di
λbc.((λy.c)(bc))
NON di
λbc.c
Nel termine
λbc.((λy.c)(bc))
il tipo del dominio (il tipo di b) deve essere per forza una freccia,
poiche' all'interno del termine la variabile b viene applicata a c
e questo si puo' fare solo se b ha un tipo freccia.
FB
Grazie per il chiarimento, Prof. Adesso penso di aver capito.
Saluti.
Logged
Pages: [
1
]
Go Up
Print
« precedente
successivo »
Jump to:
Please select a destination:
-----------------------------
Area Ufficiale
-----------------------------
=> Annunci Ufficiali
=> Segreteria Didattica
=> Aiuto, proposte e commenti
=> Stages e progetti finali
=> C.O.F. Centro Orientamento e Formazione
=> Messaggi (d)agli amministratori del forum
-----------------------------
LAUREA TRIENNALE (D.M. 270/04)
-----------------------------
=> I anno
===> Architettura degli Elaboratori, 9 CFU
===> Elementi di Analisi Matematica, 12 CFU
===> Fondamenti di Informatica, 9 CFU
===> Matematica Discreta, 12 CFU
===> Programmazione 1, 9 CFU
===> Programmazione 2, 9 CFU
=> II anno
===> Algoritmi, 9 CFU
===> Basi di Dati, 9 CFU
===> Fisica, 9 CFU
===> Ingegneria del Software, 9 CFU
===> Inglese, 3 e 6 CFU
===> Interazione e Multimedia, 9 CFU
===> Sistemi Operativi, 9 CFU
=> III anno
===> Calcolo Numerico, 6 CFU
===> Formazione Numerica, 6 CFU
===> Introduzione all'Analisi dei Dati, 9 CFU
===> Metodi Matematici e Statistici, 6 CFU
===> Reti di Calcolatori, 9 CFU
===> Tecniche di Programmazione Concorrente e Distribuita, 9 CFU
===> Teoria dell'Informazione e Crittografia, 9 CFU
=> III anno - Materie a scelta (crediti liberi)
===> Computer Forensics, 6 CFU
===> Computer Graphics, 9 CFU
===> Digital Game Development, 6 CFU
===> GPGPU/CUDA, 6 CFU
===> Informatica Musicale, 6 CFU
===> LAP 1: programmazione C/C++ 6 CFU
===> LAP 2: Programmazione Android, 6 CFU
===> Sistemi Centrali, 6 CFU
===> Startup d'impresa e Modelli di Business, 6 CFU
===> Internet Security 9 CFU
===> Social Media Management, 6 CFU
=> Corsi disattivati - Vecchio curriculum
===> E-Commerce, 6 CFU
===> Legislazione Informatica, 6 CFU
===> Teoria della Computabilità, 9 CFU
-----------------------------
LAUREA MAGISTRALE
-----------------------------
=> I ANNO
===> Intelligenza Artificiale e Lab, 9 CFU
===> Algoritmi e Complessità, 9 CFU
===> Computer Vision, 9 CFU
===> Crittografia, 9 CFU
===> Fondamenti e Linguaggi per la Programmazione Distribuita
===> Inglese Scientifico, 3 CFU
===> Metodi analitici per l'informatica, 6 CFU
===> Metodi Matematici per l'Ottimizzazione (Corso Integrato), 12 CFU
===> Multimedia, 9 CFU
===> Sicurezza dei Sistemi Informatici 9 CFU
===> Computer Security, 9 CFU
=> II ANNO
===> Machine Learning 6 CFU
===> Teoria della Computabilità, 9 CFU
===> Analisi e Gestione dei Dati, 9 CFU
===> Compilatori, 9 CFU
===> Computazione Naturale e BioIspirata, 6 CFU
===> Introduzione alla Bioinformatica, 9 CFU
===> Linguaggi Formali e Applicazioni, 9 CFU
===> Logica Computazionale, 9 CFU
===> P2P & Wireless Networks, 9 CFU
===> Pattern Recognition, 9 CFU
===> Sistemi Distribuiti, 9 CFU
===> Sistemi dedicati e laboratorio, 9 CFU
===> Web Reasoning
=> Corsi disattivati - Vecchio curriculum
===> Fisica moderna per l'informatica, 6 CFU
===> Linguaggi di Programmazione, 9 CFU
===> Protocolli di Rete
===> Teoria dei Codici, 6 CFU
-----------------------------
Vecchi ordinamenti ad esaurimento
-----------------------------
=> Laurea Triennale (D.M. 509/00)
===> Algoritmi 1
===> Algoritmi 2
===> Basi Teoriche dell'Informatica
===> Economia Aziendale
===> Fisica 1, 6 CFU
===> Fisica 2, 6 CFU
===> Fisica 3
===> Formazione Analitica 1
===> Formazione Analitica 2
===> Formazione Discreta 1
===> Formazione Discreta 2
===> J2ME
===> Lab. Amministrazione di Sistemi
===> Laboratorio di Interazione
===> Modelli Matematici
===> Multimedia per Dispositivi Mobile
===> Progetto Software
===> Reti 1, 6 CFU
===> Sicurezza dei Sistemi Informatici 1
===> Sistemi Distribuiti 1
===> Teoria dei Grafi
===> Usabilità ed Estetica del Web
===> Web Programming
=> Laurea Specialistica (D.M. 509/00)
===> Algoritmi 3
===> Analisi Numerica
===> Complessità
===> Computabilità
===> Data analysis e management
===> Ingegneria del software 2
===> Linguaggi Formali
===> Metodi algoritmici per l'ottimizzazione combinatoria
===> Programmazione Funzionale
===> Reti di Calcolatori 2
===> Ricerca Operativa
===> Sistemi Distribuiti 2
-----------------------------
Dottorandi
-----------------------------
=> Wall
=> Events
-----------------------------
Area Studenti
-----------------------------
=> Agorà
=> L'angolo del tecnico
=> Il Mercatino degli studenti
=> Software
===> -vecchia catalogazione [sarà rimossa a breve]-
=====> Proprietario
=====> Free Software
=====> Open Source
===> Approfondimenti
===> News
===> Studio
===> Videogiochi
===> Networking e telecomunicazioni
===> Sviluppo
===> Ufficio e produttività
===> Sistemi Operativi
=====> Microsoft Windows
=====> GNU/Linux, Unix e BSD
=====> Mac OS X
=====> Windows Phone
=====> Android
=====> iOS
=====> Altri
===> Eventi, conferenze, concorsi
=> Microsoft Student Partner - Avvisi e informazioni
=> ERASMUS/borse di studio internazionali
Caricamento in corso...