Combinatore logica di assiomi

Question

Sto portando alcuni esperimenti nel teorema dimostrato, con il combinatore logica, che è alla ricerca molto promettente, ma c'è un ostacolo:è stato sottolineato che in combinator di logica è vero che, ad esempio,I = SKK ma questo non è un teorema, deve essere aggiunto come un assioma.Qualcuno conosce un elenco completo di assiomi e di regole che devono essere aggiunti?

Edit:Ovviamente si può dimostrare, con la mano che mi = SKK, ma a meno che mi manca qualcosa, non è un teorema, all'interno del sistema di combinator logica con uguaglianza.Ciò detto, si può solo macro espandere I SKK...ma mi manca ancora qualcosa di importante.Prendendo il set di clausole di p(X) e ~p(X), che può risolvere una contraddizione in ordinarie del primo ordine logica, e di convertirli in SK, eseguendo la sostituzione e la valutazione di tutte le chiamate di S e K, il mio programma genera il seguente (dove sto utilizzando ' per Unlambda il backtick):

"eq "s "s "s 'k s "s "s 'k s "s 'k k 'k eq "s "s 'k s k 'k 'k k "s 'k k 'k falso k vero k 'vero

Sembra forse quello di cui ho bisogno è di un adeguato insieme di regole per la gestione parziale chiamate 'k e "s, sto solo non vedere ciò che queste regole dovrebbero essere, e tutta la letteratura che è possibile trovare in questa zona è stato scritto per un pubblico di destinazione dei matematici non programmatori.Ho il sospetto che probabilmente la risposta è abbastanza semplice, una volta che hai capito.

Answer 1

Alcuni libri di testo di definire Io come semplici alias per ((S, K) K).In questo caso sono identici (termini) per definitionem.Per dimostrare la loro uguaglianza (come funzioni), abbiamo bisogno solo di dimostrare che l'uguaglianza è riflessivo, che può essere raggiunto da una riflessività assioma schema:

• Proposizione `E = E"è deducibile (Riflessività assioma schema, creare un'istanza per ogni possibile termini indicati qui da metavariable E)

Quindi, suppongo che in tutte le successive, che le Vostre domande indaga un altro approccio:quando combinator Io non è definito come un semplice alias per termine composto ((S, K) K), ma ha introdotto come un autonomo di base combinator costante sulla propria, la cui semantica operazionale è dichiarato esplicitamente dall'assioma schema di

• ``(Io E) = E"è deducibile (I-assioma schema)

Suppongo che la Tua domanda chiede

se siamo in grado di dedurre formalmente (restando all'interno del sistema), che ad un autonomo definito Io si comporta esattamente come ((S, K) K), quando utilizzato come funzioni riduzioni?

Penso che possiamo, ma dobbiamo ricorrere a strumenti più efficaci.Ho congettura che i soliti schemi di assioma non è sufficiente, dobbiamo dichiarare anche il extensionality proprietà (uguaglianza di funzioni), che è il punto principale.Se vogliamo formalizzare extensionality come un assioma, dobbiamo aumentare il nostro oggetto di lingua con variabili libere.

Penso, dobbiamo adottare un simile approccio per la costruzione di combinatoria logica, che abbiamo per consentire anche l'utilizzo di variabili in oggetto di lingua.Uffa corso, voglio dire "basta" gratis oggetti di valore.Utilizzo di variabili associate sarebbe un imbroglio, dobbiamo rimanere all'interno del regno della logica combinatoria.Utilizzando la connessione varaibles non è barare, è un onesto strumento.Così, possiamo fare la prova formale È richiesto.

Oltre la semplice uguaglianza di assiomi e regole di inferenza (transitività, la riflessività, la simmetria, Leibniz regole), dobbiamo aggiungere un extensionality regola di inferenza per l'uguaglianza.Qui è il punto in cui le variabili libere materia.

In Csörnyei 2007:157-158, ho trovato il seguente approccio.Penso che in questo modo la prova può essere fatto.

Alcune osservazioni:

La maggior parte degli assiomi sono infatti schemi di assioma, costituito da un numero infinito assioma istanze.Le istanze devono essere istanziati per ogni possibile E, F, G i termini.Qui, io uso il corsivo per metavariables.

Superficiale natura infinita di schemi di assioma non aumentare la computabilità dei problemi, perché possono essere affrontati in un tempo finito:il nostro assioma di sistema ricorsiva.Significa che un intelligente parser può decidere in un tempo finito (inoltre, in modo molto efficace), se una data proposizione è un'istanza di un assioma schema, o non.Pertanto, l'utilizzo di schemi di assioma di non aumentare né teorico né pratico problemi.

Ora ci sembra il nostro framework:

Lingua

ALFABETO

Costanti:I tre sono chiamati costanti: K, S, Io.

Ho aggiunto il costante Io solo perché la Tua domanda presuppone che non abbiamo definito il combinator Io come un semplice alias/macro per termine composto S K K, ma si tratta di un autonomo costante sul proprio.

Mi indica costanti grassetto capitelli romani.

Segno di applicazione:Un segno @ di `applicazione" è sufficiente (notazione prefissa con sioni e 2).Come " zucchero sintattico, io uso qui parantheses invece l'applicazione esplicita segno:Io uso l'esplicita apertura ( e chiusura ) segni.

Variabili:Anche se combinator logica non fa uso di variabili associate, scope ecc, ma siamo in grado di introdurre variabili.Ho il sospetto, che non sono solo " zucchero sintattico, possono rafforzare la detrazione del sistema, troppo.Ho congettura, che la Tua domanda si richiedono il loro utilizzo.Qualsiasi enumerabile insieme infinito (disgiunti delle costanti e parentesi di segni) servirà come alfabeto di variabili, si indicano qui con formattato romane minuscole lettere x, y, z...

TERMINI

I termini sono definiti induttivamente:

• Una costante è un termine
• Ogni variabile è un termine
• Se E è un termine, e F è un termine troppo, quindi ancheE F è un termine

Io a volte uso pratico delle convenzioni come "zucchero sintattico", ad es.scrivere

E F G H

invece di

(((E F) G) H).

Detrazione

Conversione di schemi di assioma:

• ``K E F = E"è deducibile (K-assioma schema)
• ``S F G H = F H (G H)" è deducibile (S-assioma schema)
• ``Io E = E"è deducibile (I-assioma schema)

Ho aggiunto il terzo assioma di conversione (Io regola) solo perché la Tua domanda presuppone che non abbiamo definito il combinator Io come alias/macro per S K K.

Uguaglianza assioma schemi e regole di inferenza

• ``E = E"è deducibile (Riflessività assioma)
• Se "E = F"è intuibile, quindi "F = E"è anche deducibile (Simmetria regola di inferenza)
• Se "E = F"è intuibile, e "F = G"è deducibile troppo, poi anche "E = G"è riducibile (Transitività la regola)
• Se "E = F"è intuibile, quindi "E G = F G"è anche deducibile (Leibniz regola)
• Se "E = F"è intuibile, quindi "G E = G F"è anche deducibile (Leibniz regola II)

Domanda

Passiamo ora ad analizzare la Tua domanda.Ho congettura che la detrazione sistema definito finora non è abbastanza forte per dimostrare la Tua domanda.

È la proposizione "Io = S K K"deducibile?

Il problema è che abbiamo per dimostrare l'equivalenza di funzioni.Consideriamo due funzioni equivalenti se si comportano allo stesso modo.Funzioni di agire in modo che siano applicate per argomenti.Dobbiamo dimostrare che entrambe le funzioni agiscono allo stesso modo, se applicato a ogni possibile argomento.Di nuovo, il problema con l'infinito!Ho il sospetto, schemi di assiomi non può aiutare qui.Qualcosa di simile

Se E F = G F è intuibile, quindi anche E = G è intuibile

non sarebbe riuscita a fare il lavoro:possiamo vedere che questo non e ' il prodotto che vogliamo.Con esso, possiamo dimostrare che

``Io E = S K K E"è deducibile

per ogni E termine istanza, ma questi risultati sono solo separate istanze, e non può essere utilizzato come un tutto per ulteriore detrazione.Abbiamo solo risultati concreti (infiniti), non essendo in grado di riassumere:

• essa detiene per E := K
• vale per E := S
• essa detiene per E := K K
• .
• .
• .

...

possiamo riassumere questi frammentato risultato istanze in un unico grande risultato, affermando extensionality!Noi non possiamo versare questi a basso valore frammento nell'imbuto di una regola di inferenza che sciogliere un poco di più prezioso risultato.

Dobbiamo aumentare la potenza della nostra deduzione di sistema.Dobbiamo trovare un programma formale che coglie il problema.Le vostre domande porta a extensionality, e penso che, dichiarando extensionality esigenze che si possono porre proposizioni che valgono per le *****qualsiasi***** le istanze.Ecco perché penso che ci deve consentire il libero variabili all'interno del nostro oggetto di lingua.Ho congettura che i seguenti ulteriori regola di inferenza farà il lavoro:

• Se la variabile x non è parte di termini né E né F, e la dichiarazioneE x) = (F x) è derivabile, allora E = F è anche deducibile (Extensionality regola di inferenza)

La cosa difficile in questo assioma, facilmente causando confusione:x è un oggetto variabili, completamente emancipata e rispettato parti del nostro oggetto di una lingua, mentre E e G sono metavariabili, non parti dell'oggetto di una lingua, ma utilizzato solo per un breve notazione di schemi di assioma.

(Osservazione:Più precisamente, il extensionality regola di inferenza deve essere formalizzato in un più attenta, l'introduzione di un metavariabile x su tutti i possibili oggetto le variabili x, y, z,..., e anche un altro tipo di metavariabile E su tutti i possibili termine istanze.Ma questa distinzione tra i due tipi di metavariables plus le variabili oggetto non è così didattiche, qui, non interessa la Tua domanda di troppo.)

Prova

Proviamo ora la proposizione che `Io = S K K''.

Procedura per la sinistra:

• proposizione `Io x = x" è un'istanza di I-assioma schema con instatiation [E := x],

Procedura per la destra:

• Proposizione "S K K x = K x (K x)" è un'istanza di S-assioma schema con le istanze [E := K, F := K, G := x], così è deducibile
• Proposizione "K x (K x) = x" è un'istanza di K-assioma schema con le istanze [E := x, F := K x], così è deducibile

La transitività dell'uguaglianza:

• Istruzione "S K K x = K x (K x)" corrisponde la prima premessa di transitività regola di inferenza, e istruzione "K x (K x) = x" corrisponde la seconda premessa di questa regola di inferenza.Le istanze sono [E := S K K x, F := K x (K x), G = x].Quindi la conclusione non tiene troppo: E = G.Riscrivere la conclusione con la stessa istanze, si ottiene istruzione "S K K x = x", dunque, è intuibile.

La simmetria di parità:

• Utilizzando "S K K x = x", possiamo dedurre "x = S K K x"

La transitività dell'uguaglianza:

• Utilizzando "Io x = x" e "x = S K K x", possiamo dedurre "Io x = S K K x"

Ora abbiamo spianato la strada per il punto cruciale:

• Proposizione "Io x = S K K x" corrisponde con la prima premessa di Estensione regola di inferenza:(E x) = (F x), con le istanze [E := Io, F := S K K].Quindi, la conclusione deve anche tenere, che è, "E = F"con la stessa istanze ([E := Io, F := S K K]), ottenendo la proposizione "Io = S K K", quod erat demonstrandum.

---

Csörnyei, Zoltán (2007): Lambda-kalkulus.Un funkcionális programozás alapjai. Budapest:Typotex.ISBN-978-963-9664-46-3.

Answer 2

Non è necessario definire I come un assioma. Inizia con il seguente:

I.x = x
K.x y = x
S.x y z = x z (y z)

Da SKanything = anything, allora SKanything è una funzione identità, proprio come I.

Quindi, I = SKK e I = SKS. Non c'è bisogno di definire I come un assioma, è possibile definire come lo zucchero sintassi che alias SKK.

Le definizioni di S e K Sei solo assiomi.

Answer 3

Gli assiomi usuali sono completi per l'uguaglianza beta, ma non danno l'uguaglianza eta. Curry ha trovato una serie di circa trenta assiomi a quelli abituali per ottenere completezza per l'uguaglianza di beta-eta. Sono elencati in Hindley & Seldin di Introduzione ai combinatori e lambda-calcolo .

Roger Hindley, di Curry ultimo problema , elenca alcuni desiderata supplementari abbiamo potrebbe desiderare da mapping tra il lambda calcolo e le note che non abbiamo mappature che soddisfano tutti loro. È probabile che non si cura molto di tutti i criteri.