Pages: [1]   Go Down
Print
Author Topic: Esercizi non banali sul lambda-calcolo  (Read 715 times)
0 Members e 1 Utente non registrato stanno visualizzando questa discussione.
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.928



WWW
« on: 23-12-2017, 13:17:02 »

Definire una grammatica che generi tutti e soli i lambda-termini in forma normale.
« Last Edit: 02-01-2018, 13:34:12 by Franco Barbanera » Logged
ɹǝǝuıƃuǝsɹǝʌǝɹ
Administrator
God of the Forum
*****
Offline Offline

Gender: Male
Posts: 4.467


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


WWW
« Reply #1 on: 28-12-2017, 00:18:09 »

Definire una grammatica che generi tutti e soli i lambda-termini in forma normale.

L'alfabeto è fissato a priori ?
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
teo998
Matricola
*
Offline Offline

Posts: 42



WWW
« Reply #2 on: 28-12-2017, 13:00:47 »

Un termine è in forma normale quando non gli si può applicare alcuna beta induzione.
Un termine è beta inducibile se e solo se al suo interno è presente un sottotermine del tipo (<astrazione><termine>); di conseguenza nei termini in forma normale tutte le applicazioni non hanno come primo termine un'astrazione.

Le variabili e le astrazioni sono definite in maniera equivalente al classico linguaggio del lambda calcolo.


<normale> ::= <variabile> | <astrazione> | <applicazione normale>
<applicazione normale> ::= ( <variabile> <normale> ) | ( <applicazione normale> <normale>)
<astrazione> ::= (\ <variabile> . <normale>)

Logged

Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.928



WWW
« Reply #3 on: 28-12-2017, 18:17:26 »

Un termine è in forma normale quando non gli si può applicare alcuna beta induzione.
Un termine è beta inducibile se e solo se al suo interno è presente un sottotermine del tipo (<astrazione><termine>); di conseguenza nei termini in forma normale tutte le applicazioni non hanno come primo termine un'astrazione.

Le variabili e le astrazioni sono definite in maniera equivalente al classico linguaggio del lambda calcolo.


<normale> ::= <variabile> | <astrazione> | <applicazione normale>
<applicazione normale> ::= ( <variabile> <normale> ) | ( <applicazione normale> <normale>)
<astrazione> ::= (\ <variabile> . <normale>)



Ho solo letto la prima riga:
Un termine è in forma normale quando non gli si può applicare alcuna beta induzione.

Mi e' bastato...

Correggi e poi leggo il resto.

Un caro saluto
FB
« Last Edit: 29-12-2017, 00:48:06 by Franco Barbanera » Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.928



WWW
« Reply #4 on: 29-12-2017, 00:52:13 »

Definire una grammatica che generi tutti e soli i lambda-termini in forma normale.

L'alfabeto è fissato a priori ?

L'alfabeto fa parte della definizione stessa di grammatica (che e' una quadrupla cosi' e cosa', tale che cosi' e cosa')
Logged
teo998
Matricola
*
Offline Offline

Posts: 42



WWW
« Reply #5 on: 30-12-2017, 14:57:46 »

Mi correggo; sviluppo meglio il ragionamento che avevo semplificato un po' troppo.

Un termine è in forma normale quando non gli si può applicare alcuna beta induzione riduzione.
  • Un termine è beta inducibile riducibile se è del tipo (<astrazione><termine>); di conseguenza le applicazioni in forma normale non hanno come primo termine un'astrazione.
  • Un applicazione è beta riducibile (tramite le regole cong) se al suo interno è presente un termine riducibile; di conseguenza le applicazioni in forma normale hanno come termini solo termini in forma normale.
  • Un'astrazione è riducibile (regola xi) se il suo corpo è riducibile; di conseguenza le applicazioni in forma normale hanno come corpo solo termini in forma normale.

Le variabili sono definite in maniera equivalente al classico linguaggio del lambda calcolo.


<normale> ::= <variabile> | <astrazione> | <applicazione normale>
<applicazione normale> ::= ( <variabile> <normale> ) | ( <applicazione normale> <normale>)
<astrazione> ::= (\ <variabile> . <normale>)

Logged

Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.928



WWW
« Reply #6 on: 02-01-2018, 13:10:53 »

Le variabili sono definite in maniera equivalente al classico linguaggio del lambda calcolo.


Se le definissimo come per il linguaggio del lambda calcolo, dovremmo avere un alfabeto infinito...
Per essere piu' precisi potremmo dire che le variabili sono definite come fatto per il linguaggio WHILE
(l'alfabeto e' finito, ma il numero di variabili che si possono generare e' infinito)

Il resto sembra corretto.


Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.928



WWW
« Reply #7 on: 02-01-2018, 13:34:00 »

Altro esercizio non banale

Definire una sintassi alternativa per il lambda-calcolo in cui non occorra introdurre la relazione
di alpha-riduzione. Una sintassi equivalente quindi a quella con le "freccette" accennata a lezione,
ma senza le freccette (un lambda-termine rimarrebbe esprimibile come stringa alfanumerica.
Definire quindi su questi nuovi termini la relazione di beta-riduzione.
Logged
ɹǝǝuıƃuǝsɹǝʌǝɹ
Administrator
God of the Forum
*****
Offline Offline

Gender: Male
Posts: 4.467


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


WWW
« Reply #8 on: 03-01-2018, 01:47:21 »

Definire una grammatica che generi tutti e soli i lambda-termini in forma normale.

L'alfabeto è fissato a priori ?

L'alfabeto fa parte della definizione stessa di grammatica (che e' una quadrupla cosi' e cosa', tale che cosi' e cosa')
Mmm... ho ancora un dubbio... Siccome i lambda-termini possono essere di tipo "variabile", e la variabile è presa da un insieme numerabile di oggetti, bisognerebbe che l'insieme Σ e l'insieme delle regole abbia potenza almeno uguale a quella del numerabile...

Abbiamo noi mai definito grammatiche di questo tipo?

O si vuole usare un altro sistema per rappresentare la quantità numerabile di λ-variabili?
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
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.928



WWW
« Reply #9 on: 03-01-2018, 17:59:31 »

Come ho scritto tre post sopra, si puo' utilizzare il metodo utilizzato per la grammatica del linguaggio WHILE,
che e' poi quello di tutti i linguaggi di programmazione:
le variabili sono nomi, cioe' stringhe (magari con una certa struttura) su un alfabeto finito.
Logged
teo998
Matricola
*
Offline Offline

Posts: 42



WWW
« Reply #10 on: 15-01-2018, 12:27:21 »

Altro esercizio non banale

Definire una sintassi alternativa per il lambda-calcolo in cui non occorra introdurre la relazione
di alpha-riduzione. Una sintassi equivalente quindi a quella con le "freccette" accennata a lezione,
ma senza le freccette (un lambda-termine rimarrebbe esprimibile come stringa alfanumerica.
Definire quindi su questi nuovi termini la relazione di beta-riduzione.

dopo averci pensato un po' sono arrivato a questa conclusione; prof mi dica se c'è qualcosa che porta a affermazioni false o se c'è qualcosa espressa male:

introduciamo la variabile speciale #n, dove n è un numero naturale;
#1 è la varibile che si riferisce alla variabile legata dell'astrazione più vicina, #2 è la variabile che si riferisce alla variabile legata della seconda astrazione più vicina, ecc.

Esempio:
\.#1      \x.x
\.\.#1 #2   \fx.fx
\.\.#2      \xy.y


definiamo un termine di grado n come:
<termine, n> ::= #k (per ogni k tale che k>1, k<=n) | <variabile> | (<termine, n> <termine, n>) | \.<termine, n+1>
un termine di grado n è anche un termine di grado n', con n'>n
(il grado di un termine può essere definito informalmente come: se il grado è 0, è una lambda termine; se il grado è k, significa che il termine è il corpo di una funzione che è un termine di grado k-1)

definiamo l'insieme dei lambda termini come l'insieme di tutti e soli i termini di grado 0

definiamo l'operazione di sostituzione nel seguente modo
N è un termine, #k è una variabile speciale

#k[N/#k]   N
 y[N/#k]    y, con y≠#k
(AB)[N/#k]   (A[N/#k] B[N/#k])
(\.M)[N/#k]   \.M[N/#k+1], dove M è un termine di grado k+1

la sostituzione del tipo M[N/x] dove x non è una variabile speciale non viene definita in quanto inutile per la beta-riduzione, che utilizza la sostituzione solo su variabili legate (e le variabili legate sono solo le variabili speciali)

Definiamo la beta-riduzione con le seguenti regole:
beta: (\.M)N -> M[N/#1]
cong1, cong2, xi equivalenti alle regole della classica beta-riduzione
« Last Edit: 15-01-2018, 12:51:06 by teo998 » Logged

Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.928



WWW
« Reply #11 on: 15-01-2018, 12:45:09 »

La tua idea e' corretta.
Hai definito quelli che si chiamano DeBrujin indexes.

Puoi controllare la correttezza delle tue definizioni di sostituzione e di beta-riduzione
confrontandole con quanto descritto in
https://en.wikipedia.org/wiki/De_Bruijn_index
oppure, meglio ancora, con quanto scritto in modo piu' formale
nella Sezione 2.3 del seguente articolo
http://www.mi.sanu.ac.rs/~uros.m/logcom/hdb/Volume_11/Issue_03/pdf/110363.pdf

Complimenti.

FB
Logged
teo998
Matricola
*
Offline Offline

Posts: 42



WWW
« Reply #12 on: 15-01-2018, 12:55:18 »

grazie per il materiale di approfondimento
: D
Logged

Pages: [1]   Go Up
Print
Jump to: