logica combinatoria
logica combinatoria locuzione utilizzata in due diverse accezioni:
• per indicare un modello di calcolo logico introdotto nel 1920 dal matematico ucraino M.I. Schönfinkel (combinatory [...] esistono operatori (come l’astrazione λ) che leghino le variabili presenti nel termine. Nonostante tale differenza, il lambda-calcolo e la logica combinatoria hanno lo stesso potere espressivo, nel senso che rappresentano la stessa classe di funzioni ...
Leggi Tutto
logica lineare
logica lineare area di ricerca della logica matematica nata nel 1986 e diffusasi in seguito alla pubblicazione, nel 1987, dell’articolo Linear logic del logico francese Jean-Yves Girard [...] della logica intuizionista, tuttavia si pone come strumento utile alla ricerca in vari settori fra cui il → lambda-calcolo, la → programmazione logica e la teoria della → complessità computazionale.
La logica lineare elimina le due regole strutturali ...
Leggi Tutto
calcolabilita
calcolabilità in logica, termine che indica la possibilità di descrivere in modo sequenziale, deterministico e finito, una procedura di calcolo che consenta di pervenire a un dato risultato. [...] sono stati introdotti altri modelli di calcolabilità fra i quali le → funzioni ricorsive generali e il λ-calcolo (→ lambda-calcolo). Questi modelli di calcolabilità sono equivalenti fra loro in quanto individuano una stessa classe di funzioni; ciò ...
Leggi Tutto
LISP
LISP sigla (dall’inglese List Processing) con cui si indica un linguaggio di programmazione introdotto per consentire un’agevole elaborazione di liste di dati simbolici. È stato il primo linguaggio [...] dare un nome standard, ma semplicemente indicando i parametri formali della funzione e la sua operazione. Così, per esempio, poiché nel lambda-calcolo la funzione ƒ(x) può essere indicata come λxƒ e si possono considerare x e ƒ come due componenti il ...
Leggi Tutto
Post, sistema di
Post, sistema di in logica, uno dei modelli sviluppati per proporre una definizione matematica del concetto intuitivo di → funzione calcolabile; altri modelli, tutti tra loro equivalenti, [...] sono la macchina di → Turing, le → funzioni ricorsive e il → lambda-calcolo. Nel sistema di Post il calcolo di una funzione matematica è simulato dalla manipolazione di una stringa di simboli attraverso un insieme di regole stabilite in modo ...
Leggi Tutto
operatore logico
operatore logico in un’algebra di → Boole, sinonimo di operazione su variabili booleane. Gli operatori logici fondamentali sono gli operatori and, per il prodotto logico, or, per la [...] G («sarà sempre vero che»), F («ci sarà un momento in cui»), H («è stato sempre vero che»), P («c’è stato un momento in cui»). Un particolare operatore logico, detto operatore di astrazione λ, è utilizzato nel cosiddetto λ-calcolo (→ lambda-calcolo). ...
Leggi Tutto
termine libero
termine libero o termine aperto, in logica, termine di un linguaggio formale che contiene almeno una variabile libera. In particolare, nel linguaggio dei predicati, termine che contiene [...] , risulta libero in quanto, oltre a x, contiene la variabile libera y che non è vincolata dal quantificatore universale.
☐ Nel → lambda-calcolo un termine è libero se fra le sue variabili ne contiene almeno una che non è vincolata dal simbolo λ. Per ...
Leggi Tutto
tipo
tipo termine che assume significati diversi in informatica e in logica.
☐ In informatica, con il termine tipo o tipo di dato si indica la caratteristica comune dei valori che possono essere assunti [...] sono non tipati (o non tipizzati) poiché i loro termini non hanno tipo. Un esempio di linguaggio siffatto è il → lambda-calcolo puro, i cui termini non sono tipati e possono essere trattati tutti nello stesso modo: si può applicare una variabile x a ...
Leggi Tutto
combinatore
combinatore in logica, funzione che trasforma una data sequenza di simboli, che appartengono a un linguaggio formale, in un’altra sequenza. Per esempio, in un linguaggio formale contenente [...] di simboli operate dai combinatori è quello di rappresentare formalmente il procedimento di calcolo di una funzione (→ algoritmo). In particolare, nel λ-calcolo (→ lambda-calcolo), un combinatore è una formula in forma normale che non contiene ...
Leggi Tutto
occorrenza
occorrenza termine che, riferito a un simbolo s, ne indica la presenza all’interno di una formula F di un linguaggio formale. Vi sono 1, 2, 3, ..., n occorrenze del simbolo s nella formula [...] logici che contengono quantificatori, come per esempio il linguaggio dei predicati, o comunque operatori, quali il lambda-calcolo, è importante distinguere le occorrenze libere dalle occorrenze vincolate (o legate) di una stessa variabile. Una ...
Leggi Tutto