Teoria dei Tipi
Piccolo sondaggio:
ne ho sentito parlare di recente, chi di voi usa la teoria dei tipi abitualmente(anche in maniera amichevole) al posto dell'insiemistica/logica o quantomeno la conosce?
spero non nessuno
ne ho sentito parlare di recente, chi di voi usa la teoria dei tipi abitualmente(anche in maniera amichevole) al posto dell'insiemistica/logica o quantomeno la conosce?
spero non nessuno
Risposte
meraviglioso fields, meraviglioso!!
@onlyReferee:
[ot]
posso chiederti su che argomento in generale la stai facendo?[/ot]
@onlyReferee:
[ot]
"onlyReferee":
Fatto sta che nella tesi che sto portando avanti adesso, pur avendo a che fare principalmente con l'argomento dei linguaggi formali, potrebbero tornarmi buone anche alcune nozioni relative alla teoria dei tipi...
posso chiederti su che argomento in generale la stai facendo?[/ot]
Ciao hyoukarou!
La teoria dei tipi ho avuto modo di scoprirla l'anno scorso al quarto anno di magistrale seguendo il corso di logica matematica (studio informatica ed amo molto anche la matematica). In quanto informatico questa corrispondenza tra i programmi e le dimostrazioni (che poi coinvolgono appunto i tipi all'interno delle formule con i lambda-termini) mi ha profondamente affascinato. Fatto sta che nella tesi che sto portando avanti adesso, pur avendo a che fare principalmente con l'argomento dei linguaggi formali, potrebbero tornarmi buone anche alcune nozioni relative alla teoria dei tipi...
Lo ritengo uno dei più grandi collegamenti tra informatica e matematica.
La teoria dei tipi ho avuto modo di scoprirla l'anno scorso al quarto anno di magistrale seguendo il corso di logica matematica (studio informatica ed amo molto anche la matematica). In quanto informatico questa corrispondenza tra i programmi e le dimostrazioni (che poi coinvolgono appunto i tipi all'interno delle formule con i lambda-termini) mi ha profondamente affascinato. Fatto sta che nella tesi che sto portando avanti adesso, pur avendo a che fare principalmente con l'argomento dei linguaggi formali, potrebbero tornarmi buone anche alcune nozioni relative alla teoria dei tipi...
Lo ritengo uno dei più grandi collegamenti tra informatica e matematica.
"hyoukarou":
A dire il vero non so molto nemmeno io, l'ho "scoperta" da qualche giorno per questo volevo chiedere quanto potrebbe fruttare studiarla(per uno che ha abbastanza tempo da perdere).
Per uno che ha tempo da perdere, vale la pena studiare tutto (dal punto di vista logico: ex falso quodlibet
). Diciamo che la teoria dei tipi non si studia in un giorno, perché è molto sofisticata, e ci vuole molto tempo per assimilarla. Se ti interessano la logica e i proof assistant è un must, altrimenti puoi vivere senza, visto che si tratta di qualcosa alle frontiere della ricerca.
Per quanto ne ho capito le varie teorie dei tipi sono molto connesse alla topologia, alla teoria delle categorie, alla logica e vedendo un paio di costruzioni come quella dei numeri naturali immaginavo potesse essere usata come sostituto a ZFC.
Questo un giorno non lontano avverrà con la teoria omotopica dei tipi, ma la teoria degli insiemi va bene per ora. La stessa teoria degli insiemi ammette un'interpretazione in teoria dei tipi, attraverso l'isomorfismo di Curry-Howard. Quindi di fatto si può continuare a restare in ZF e fare teoria dei tipi.
Ho la fortuna e il privilegio di lavorare in teoria dei tipi da diversi anni. Nonostante noi logici studiamo e amiamo la teoria moderna dei tipi da più di 60 anni, essa è stata molto recentemente apprezzata da una più ampia comunità matematica grazie al lavoro della medaglia Fields Voevodsky. Voevodsky poco tempo fa ha iniziato a interessarsi ai proof assistant per la formalizzazione della matematica, e ha notato delle analogie tra Coq (un proof assisant basato sulla teoria dei tipi) e la teoria omotopica in matematica. Con l'aiuto della comunità logica è stata sviluppata la teoria omotopica dei tipi, di cui ultimamente c'è un gran parlare.
Comunque, per rispondere a Luca, no, la teoria moderna dei tipi non c'entra nulla con la dottrina di Russell. E' vero che Russell ha inventato il concetto di tipo e ispirato direttamente Church e Curry (i pionieri della teoria moderna dei tipi), tuttavia la dottrina di Russell è obsoleta e sostanzialmente morta con il lavoro di Russell stesso e Whitehead.
Per rispondere a Sergio, sì, la teoria dei tipi è essenzialmente informatica, ma, no, la teoria dei tipi è innanzitutto logica pura, più precisamente deduzione naturale. Il fatto è che la più grande scoperta in logica dopo i teoremi di Godel è il cosiddetto isomorfismo di Curry-Howard, i.e. il menage à trois della teoria della dimostrazione. Si tratta della corrispondenza tra dimostrazioni logiche, programmi informatici tipati e funzioni matematiche. Tanti anni fa è stato notato da Church, Curry e Howard che l'operatore $\rightarrow$ che dati due insiemi/oggetti $A$ e $B$ crea lo spazio di funzioni $A\rightarrow B$ ha delle proprietà logiche interessanti. Quali?
Be', data una funzione $f: A\rightarrow B$ e un elemento $a: A$, attraverso la nozione di applicazione possiamo ottenere un oggetto $f(a): B$. Ma questo, dal punto di vista logico, non è altro che il familiare modus ponens! In altri termini, se $A$ implica $B$ e $A$ sono veri, allora $B$ è vero. Inoltre, quando definiamo una funzione $x\mapsto f(x): A\rightarrow B$ che prende un oggetto $x: A$ e restituisce un oggetto $f(x)$ di tipo $B$, stiamo nello stesso tempo deducendo dalla premessa $A$ la proposizione $B$, e quindi otteniamo che $A\rightarrow B$.
Similmente, l'uso del prodotto cartesiano $A\times B$ corrisponde alla proposizione logica $A\wedge B$, mentre l'unione disgiunta $A+B$ corrisponde alla proposizione $A\vee B$. Il quantificatore $\forall x\in A. B(x)$ corrisponde al prodotto cartesiano di una collezione di insiemi $B(x)$ indicizzata dagli elementi di $A$ e così via.
Così facendo tutte le dimostrazioni logiche rappresentano al tempo stesso un programma informatico tipato e una funzione matematica. Le operazioni di esecuzione di un programma corrispondono dal punto di vista logico all'eliminazione dei lemmi, definizioni e ridondanze in una prova in modo da ottenere una prova più diretta, importantissimo processo chiamato normalizzazione.
Ad esempio supponiamo di avere dimostrato/definito
$x: A$
.
.
.
$f(x): B$
-----------
$ x\mapsto f(x): A\rightarrow B$ $\qquad\qquad \qquad\qquad a: A$
------------------------------------------------------
$(x\mapsto f(x))(a): B$
Ora, il passo di calcolo $(x\mapsto f(x))(a)= f(a)$ corrisponde alla semplificazione della prova sopra in
$a: A$
.
.
.
$f(a): B$
In altri termini, se prima dimostriamo che da $A$ segue $B$, ottenendo $A\rightarrow B$, e poi dimostriamo $A$ e usiamo il modus ponens per ottenere $B$, be', possiamo eliminare questo giro dimostrando direttamente $B$ da $A$ visto che $A$ è dimostrabile e non è necessario assumerla.
Comunque, per rispondere a Luca, no, la teoria moderna dei tipi non c'entra nulla con la dottrina di Russell. E' vero che Russell ha inventato il concetto di tipo e ispirato direttamente Church e Curry (i pionieri della teoria moderna dei tipi), tuttavia la dottrina di Russell è obsoleta e sostanzialmente morta con il lavoro di Russell stesso e Whitehead.
Per rispondere a Sergio, sì, la teoria dei tipi è essenzialmente informatica, ma, no, la teoria dei tipi è innanzitutto logica pura, più precisamente deduzione naturale. Il fatto è che la più grande scoperta in logica dopo i teoremi di Godel è il cosiddetto isomorfismo di Curry-Howard, i.e. il menage à trois della teoria della dimostrazione. Si tratta della corrispondenza tra dimostrazioni logiche, programmi informatici tipati e funzioni matematiche. Tanti anni fa è stato notato da Church, Curry e Howard che l'operatore $\rightarrow$ che dati due insiemi/oggetti $A$ e $B$ crea lo spazio di funzioni $A\rightarrow B$ ha delle proprietà logiche interessanti. Quali?
Be', data una funzione $f: A\rightarrow B$ e un elemento $a: A$, attraverso la nozione di applicazione possiamo ottenere un oggetto $f(a): B$. Ma questo, dal punto di vista logico, non è altro che il familiare modus ponens! In altri termini, se $A$ implica $B$ e $A$ sono veri, allora $B$ è vero. Inoltre, quando definiamo una funzione $x\mapsto f(x): A\rightarrow B$ che prende un oggetto $x: A$ e restituisce un oggetto $f(x)$ di tipo $B$, stiamo nello stesso tempo deducendo dalla premessa $A$ la proposizione $B$, e quindi otteniamo che $A\rightarrow B$.
Similmente, l'uso del prodotto cartesiano $A\times B$ corrisponde alla proposizione logica $A\wedge B$, mentre l'unione disgiunta $A+B$ corrisponde alla proposizione $A\vee B$. Il quantificatore $\forall x\in A. B(x)$ corrisponde al prodotto cartesiano di una collezione di insiemi $B(x)$ indicizzata dagli elementi di $A$ e così via.
Così facendo tutte le dimostrazioni logiche rappresentano al tempo stesso un programma informatico tipato e una funzione matematica. Le operazioni di esecuzione di un programma corrispondono dal punto di vista logico all'eliminazione dei lemmi, definizioni e ridondanze in una prova in modo da ottenere una prova più diretta, importantissimo processo chiamato normalizzazione.
Ad esempio supponiamo di avere dimostrato/definito
$x: A$
.
.
.
$f(x): B$
-----------
$ x\mapsto f(x): A\rightarrow B$ $\qquad\qquad \qquad\qquad a: A$
------------------------------------------------------
$(x\mapsto f(x))(a): B$
Ora, il passo di calcolo $(x\mapsto f(x))(a)= f(a)$ corrisponde alla semplificazione della prova sopra in
$a: A$
.
.
.
$f(a): B$
In altri termini, se prima dimostriamo che da $A$ segue $B$, ottenendo $A\rightarrow B$, e poi dimostriamo $A$ e usiamo il modus ponens per ottenere $B$, be', possiamo eliminare questo giro dimostrando direttamente $B$ da $A$ visto che $A$ è dimostrabile e non è necessario assumerla.
A dire il vero non so molto nemmeno io, l'ho "scoperta" da qualche giorno per questo volevo chiedere quanto potrebbe fruttare studiarla(per uno che ha abbastanza tempo da perdere).
Per quanto ne ho capito le varie teorie dei tipi sono molto connesse alla topologia, alla teoria delle categorie, alla logica e vedendo un paio di costruzioni come quella dei numeri naturali immaginavo potesse essere usata come sostituto a ZFC.
Un paio di pdf provocanti:
http://www.ams.org/journals/bull/1989-21-02/S0273-0979-1989-15849-7/S0273-0979-1989-15849-7.pdf
http://profs.sci.univr.it/~zorzim/categorie.pdf
Per quanto ne ho capito le varie teorie dei tipi sono molto connesse alla topologia, alla teoria delle categorie, alla logica e vedendo un paio di costruzioni come quella dei numeri naturali immaginavo potesse essere usata come sostituto a ZFC.
Un paio di pdf provocanti:
http://www.ams.org/journals/bull/1989-21-02/S0273-0979-1989-15849-7/S0273-0979-1989-15849-7.pdf
http://profs.sci.univr.it/~zorzim/categorie.pdf
Sto affrontando lo studio dei tipi nel corso di teoria dei modelli...ma non so se è la stessa cosa, anche perchè il docente non ce l'ha presentato come teoria che "sostituisse" l'insiemistica.
Dammi/cci qualche altro dettaglio.
Dammi/cci qualche altro dettaglio.
Io ho solo letto di essa avendo letto i Principia di Russel, ma di più di quanto è spiegato dallo stesso Russel non so. Aspettiamo che un logico risponda, non so nemmeno se come teoria si è sviluppata.
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo