Linguaggio predicativo con solo funzioni \( 1 \)-arie
Un linguaggio predicativo di solito è definito come il dato di 1) parentesi (\( ( \) e \( ) \)), 2) connettivi vari (\( {\land} \), \( \rightarrow \), ecc.), 3) quantificatori (\( {\forall} \), \( {\exists} \)) e 4) un'infinità numerabile di "variabili" (\( x_1,x_2,\dots \)). A questi quattro punti talvolta sono aggiunti 5) dei segni di funzione \( n \)-aria per (\( f_1^n,f_2^n,\dots \)) per \( n = 1,2,\dots \) e 6) dei segni di relazione \( n \)-ara.
I termini di un linguaggio predicativo sono dunque definiti per induzione chiedendo che 1) ogni variabile e ogni segno di funzione \( 0 \)-aria sia un termine; 2) se \( t_1,\dots,t_n \) sono termini, allora \( f(t_1,\dots,t_n) \) è un termine per ogni segno di funzione \( n \)-aria \( f \).
Ho due domande.
1) Perché si chiede che tra i termini ci siano scritture del tipo \( f(x_1,\dots,x_n) \), dove \( x_1,\dots,x_n \) sono variabili? Non basterebbe prendere i simboli di funzione \( f_j^n \)?
2) Posso ridefinire l'insieme dei termini in maniera da evitare di scrivere cose tipo \( f(t_1{\color{red},\dots,}t_n) \)? In altre parole vorrei lavorare solo con funzioni unarie (avete presente Haskell? Ecco, vorrei che tutti i "termini funzionali" prendessero un solo argomento). Ho idea di come fare per definire questi nuovi termini, ma non ho mai visto nessuno fare così. C'è qualche motivo per cui non si fa?
I termini di un linguaggio predicativo sono dunque definiti per induzione chiedendo che 1) ogni variabile e ogni segno di funzione \( 0 \)-aria sia un termine; 2) se \( t_1,\dots,t_n \) sono termini, allora \( f(t_1,\dots,t_n) \) è un termine per ogni segno di funzione \( n \)-aria \( f \).
Ho due domande.
1) Perché si chiede che tra i termini ci siano scritture del tipo \( f(x_1,\dots,x_n) \), dove \( x_1,\dots,x_n \) sono variabili? Non basterebbe prendere i simboli di funzione \( f_j^n \)?
2) Posso ridefinire l'insieme dei termini in maniera da evitare di scrivere cose tipo \( f(t_1{\color{red},\dots,}t_n) \)? In altre parole vorrei lavorare solo con funzioni unarie (avete presente Haskell? Ecco, vorrei che tutti i "termini funzionali" prendessero un solo argomento). Ho idea di come fare per definire questi nuovi termini, ma non ho mai visto nessuno fare così. C'è qualche motivo per cui non si fa?
Risposte
La mia impressione è che la potenza espressiva di questo linguaggio che vai costruendo debba essere quella del $\lambda$-calcolo, sicché non vuoi solo le funzioni (\(\lambda v . M\)), ma vuoi poterle applicare a termini (cioè se M,N sono nella tua term algebra, ci sta anche \(M\; N\) -l'applicazione di M ad N).
Questo risponde anche a 2: nel $\lambda$-calcolo di Giulietto Church tutti i \(\lambda\)-terms sono unari: la funzione somma ad esempio la somma di numerali è il termine \(λm n f x. m f (n f x)\) che è solo un modo forbito e zuccherosintatticoso di dire \(λm.(λn.(λf.(λx.m f (n f x))))\).
Il fatto è (anche) che a questo livello di primitività te ne puoi sbattere della necessità di avere espressioni human-readable e scrivere semplicemente \(λ λ λ 3 1 (2 1)\) per il combinatore S bindando alla de Brujin... le variabili sono per menti deboli.
Questo risponde anche a 2: nel $\lambda$-calcolo di Giulietto Church tutti i \(\lambda\)-terms sono unari: la funzione somma ad esempio la somma di numerali è il termine \(λm n f x. m f (n f x)\) che è solo un modo forbito e zuccherosintatticoso di dire \(λm.(λn.(λf.(λx.m f (n f x))))\).
Il fatto è (anche) che a questo livello di primitività te ne puoi sbattere della necessità di avere espressioni human-readable e scrivere semplicemente \(λ λ λ 3 1 (2 1)\) per il combinatore S bindando alla de Brujin... le variabili sono per menti deboli.
Che cosa intendi con "potenza espressiva"?
Più formalmente, io distinguerei tra termini \( 0 \)-ari e termini \( n \)-ari per \( n\geqq 1 \). Dunque le variabili e i simboli di funzione \( 0 \)-aria allora sono termini \( 0 \)-ari; se \( n\geqq 1 \), \( f \) è un segno di funzione \( n + 1 \)-aria e \( t_0 \) è un termine \( 0 \)-ario, allora \( f(t) \) è un termine \( n \)-ario; se \( n\geqq 1 \), \( t \) è un termine \( n + 1 \)-ario e \( t_0 \) è un termine \( 0 \)-ario, allora \( t(t_0) \) è un termine \( n \)-ario. Non so se questa definizione "va bene", sia perché non se se definisce ciò che sto cercando di definire, sia perché non so quanto sia implementabile pari pari su una macchina (tipo le definizione induttiva di "etichetta"; quella lo è).
il \( \lambda \)-calcolo mi sembra molto più basic di questo linguaggio: prendi variabili \( x_1,x_2,\dots \) e definisci i termini del \( \lambda \)-calcolo (anche) chiedendo che per ogni termine \( t \) e per ogni termine \( u \), \( tu \) sia un termine. No, non voglio questo nel mio linguaggio! Tra l'altro, secondo te questo linguaggio è una sorta di \( \lambda \)-calcolo mentre il linguaggio predicativo classico no? Perché io invece spero siano equivalenti (anzi credo -altro che spero- che siano proprio uguali, nel senso che la definizione di linguaggio predicativo "classica" è solo la specifica di una definizione di linguaggio mentre la definizione che si discute qui è la realizzazione di quella specifica).
Più formalmente, io distinguerei tra termini \( 0 \)-ari e termini \( n \)-ari per \( n\geqq 1 \). Dunque le variabili e i simboli di funzione \( 0 \)-aria allora sono termini \( 0 \)-ari; se \( n\geqq 1 \), \( f \) è un segno di funzione \( n + 1 \)-aria e \( t_0 \) è un termine \( 0 \)-ario, allora \( f(t) \) è un termine \( n \)-ario; se \( n\geqq 1 \), \( t \) è un termine \( n + 1 \)-ario e \( t_0 \) è un termine \( 0 \)-ario, allora \( t(t_0) \) è un termine \( n \)-ario. Non so se questa definizione "va bene", sia perché non se se definisce ciò che sto cercando di definire, sia perché non so quanto sia implementabile pari pari su una macchina (tipo le definizione induttiva di "etichetta"; quella lo è).
il \( \lambda \)-calcolo mi sembra molto più basic di questo linguaggio: prendi variabili \( x_1,x_2,\dots \) e definisci i termini del \( \lambda \)-calcolo (anche) chiedendo che per ogni termine \( t \) e per ogni termine \( u \), \( tu \) sia un termine. No, non voglio questo nel mio linguaggio! Tra l'altro, secondo te questo linguaggio è una sorta di \( \lambda \)-calcolo mentre il linguaggio predicativo classico no? Perché io invece spero siano equivalenti (anzi credo -altro che spero- che siano proprio uguali, nel senso che la definizione di linguaggio predicativo "classica" è solo la specifica di una definizione di linguaggio mentre la definizione che si discute qui è la realizzazione di quella specifica).
Non so se questa definizione "va bene", sia perché non se se definisce ciò che sto cercando di definire, sia perché non so quanto sia implementabile pari pari su una macchina (tipo le definizione induttiva di "etichetta"; quella lo è).Comunque la questione principale è veramente questa. Devo specificare nel modo più chiaro possibile che significa che
"marco2132k":sennò il robot mi stupra il gatto.
2) se \( t_1,\dots,t_n \) sono termini, allora \( {\color{red}f(t_1,\dots,t_n)} \) è un termine per ogni segno di funzione \( n \)-aria \( f \).
No, non voglio questo nel mio linguaggio!Ma appunto, se non ce lo vuoi non c'è speranza di esprimere l'applicazione di funzioni a termini: se non ammetti la giustapposizione di termini, da intepretare come "applicazione" di un termine a un altro, à la lambda calcolo, che significato ha \(f(\vec t)\)? Se guardi come sono implementati i linguaggi (tutti), vuoi almeno fare quello che fa il lambda calcolo, che è il minimo indispensabile per scrivere le funzioni computabili. Più in astratto quello che stai facendo è costruire la term algebra sul tuo linguaggio. O qualcosa di molto simile, insomma.
Il problema è che nel lambda calcolo "nudo" tutti i termini si applicano a tutti i termini. Io voglio essenzialmente una distinzione tra costanti e funzioni. Voglio scrivere cose come
\[
f^0,\quad f^1(f^0),\quad f^2(f^0),\quad f^2(f_0)(f_0), \quad f^2(f^1(f^0))
\] e mai cose come
\[
f^0(f_0),\quad f^1(f^7)
\] dove \( f^n \) è un segno di funzione \( n \)-aria.
Adesso che mi ci fai pensare potrei definire "le tuple \( \vec t \)" per induzione e questo mi darebbe lo stesso una buona definizione di termine. Poi magari dimostro che i due tipi di termini sono equivalenti e ho vinto (?)
\[
f^0,\quad f^1(f^0),\quad f^2(f^0),\quad f^2(f_0)(f_0), \quad f^2(f^1(f^0))
\] e mai cose come
\[
f^0(f_0),\quad f^1(f^7)
\] dove \( f^n \) è un segno di funzione \( n \)-aria.
Adesso che mi ci fai pensare potrei definire "le tuple \( \vec t \)" per induzione e questo mi darebbe lo stesso una buona definizione di termine. Poi magari dimostro che i due tipi di termini sono equivalenti e ho vinto (?)
Lasciare perdere questo messaggio.
[ot]Domanda ingenua: perché hai la necessità di modificare la definizione di termine?
(Sono molto arrugginito con queste cose, per cui quello che dirò può essere privo di senso.)
Se vogliamo distinguere le costanti dalle variabili, possiamo pensare bene di modificare l'alfabeto con cui stiamo lavorando. Definisci $C={c_1,c_2,...}$ come l'insieme dei simboli dedicati alle costanti, $V={x_1,x_2,...}$ l'insieme dei simboli dedicati alle variabili e imponi che tali insiemi siano disgiunti. Aggiungendo all'alfabeto con cui lavori i simboli $c, x, 0,1$ che servono per codificare i simboli per le costanti e per le variabili: è possibile costruire delle regole sintattiche per distinguere le costanti e le variabili e le stringhe prive di senso.
[Edit] L'ho visto fare al mio professore di linguaggi, per questo ho proposto questa idea, non so se può essere utile.[/ot]
[ot]Domanda ingenua: perché hai la necessità di modificare la definizione di termine?
(Sono molto arrugginito con queste cose, per cui quello che dirò può essere privo di senso.)
Se vogliamo distinguere le costanti dalle variabili, possiamo pensare bene di modificare l'alfabeto con cui stiamo lavorando. Definisci $C={c_1,c_2,...}$ come l'insieme dei simboli dedicati alle costanti, $V={x_1,x_2,...}$ l'insieme dei simboli dedicati alle variabili e imponi che tali insiemi siano disgiunti. Aggiungendo all'alfabeto con cui lavori i simboli $c, x, 0,1$ che servono per codificare i simboli per le costanti e per le variabili: è possibile costruire delle regole sintattiche per distinguere le costanti e le variabili e le stringhe prive di senso.
[Edit] L'ho visto fare al mio professore di linguaggi, per questo ho proposto questa idea, non so se può essere utile.[/ot]
"marco2132k":Questo (=vietare stringhe di simboli patologiche) si fa imponendo una qualche sorta di typing discipline, e non ha niente a che vedere col vietare l'applicazione di funzioni tout court. Semplicemente chiedi che certi termini non siano legali.
Il problema è che nel lambda calcolo "nudo" tutti i termini si applicano a tutti i termini. Io voglio essenzialmente una distinzione tra costanti e funzioni. Voglio scrivere cose come
\[
f^0,\quad f^1(f^0),\quad f^2(f^0),\quad f^2(f_0)(f_0), \quad f^2(f^1(f^0))
\] e mai cose come
\[
f^0(f_0),\quad f^1(f^7)
\] dove \( f^n \) è un segno di funzione \( n \)-aria.
Adesso che mi ci fai pensare potrei definire "le tuple \( \vec t \)" per induzione e questo mi darebbe lo stesso una buona definizione di termine. Poi magari dimostro che i due tipi di termini sono equivalenti e ho vinto (?)
Per quanto riguarda la costruzione della term algebra, vuoi una roba del genere o qualcosa di molto simile
(src: https://www.cambridge.org/core/books/de ... 7FCD34BC1D)
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo