Axiomes de la logique combinatrice

Question

Je réalise quelques expériences de démonstration de théorèmes avec la logique combinatrice, ce qui semble prometteur, mais il y a une pierre d'achoppement :il a été souligné que dans la logique des combinateurs, il est vrai que par ex.I = SKK mais ce n'est pas un théorème, il faut l'ajouter comme un axiome.Quelqu'un connaît-il une liste complète des axiomes qui doivent être ajoutés ?

Modifier:Vous pouvez bien sûr prouver à la main que I = SKK, mais à moins que quelque chose ne me manque, ce n'est pas un théorème dans le système de logique combinatrice avec égalité.Cela étant dit, vous pouvez simplement développer la macro I en SKK...mais il me manque encore quelque chose d'important.En prenant l'ensemble des clauses p(X) et ~p(X), qui résolvent facilement une contradiction dans la logique ordinaire du premier ordre, et en les convertissant en SK, en effectuant une substitution et en évaluant tous les appels de S et K, mon programme génère le suivant (où j'utilise ' pour le backtick d'Unlambda) :

''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 faux 'k vrai, 'k vrai'

Il semble que j'ai peut-être besoin d'un ensemble de règles appropriées pour gérer les appels partiels 'k et ''s, je ne vois tout simplement pas quelles devraient être ces règles, et toute la littérature que je peux trouver dans ce domaine a été écrite pour un public cible de mathématiciens et non de programmeurs.Je suppose que la réponse est probablement assez simple une fois que vous la comprenez.

Answer 1

Certains manuels définissent je comme simple pseudonyme pour ((SK)K).Dans ce cas, ils sont identiques (en tant que termes) par définition.Pour prouver leur égalité (en tant que fonctions), il suffit de prouver que l'égalité est réflexive, ce qui peut être réalisé par un schéma d'axiome de réflexivité :

• Proposition ``E = E'' est déductible (Réflexivité schéma d'axiome, instancié pour chaque terme possible désigné ici par métavariable E)

Ainsi, je suppose dans ce qui suit, que vos questions explorent une autre approche :quand combinateur je n'est pas défini comme un simple pseudonyme pour terme composé ((SK)K), mais présenté comme un combinateur de base autonome constante seule, dont la sémantique opérationnelle est déclarée explicitement par axiome schème

• ``(je E) = E'' est déductible (I-axiome schème)

Je suppose que votre question demande

si nous pouvons déduire formellement (en restant à l'intérieur du système) qu'un tel système défini de manière autonome je se comporte exactement comme ((SK)K), lorsqu'il est utilisé comme fonctions dans des réductions ?

Je pense que nous le pouvons, mais nous devons recourir à des outils plus solides.Je suppose que les schémas d'axiomes habituels ne suffisent pas, nous devons également déclarer la propriété d'extensionnalité (égalité des fonctions), c'est le point principal.Si nous voulons formaliser l’extensionnalité comme un axiome, nous devons augmenter notre langage objet avec variables libres.

Je pense que nous devons adopter une telle approche pour construire une logique combinatoire que nous devons également autoriser l'utilisation de variables dans le langage objet.Bien sûr, je veux dire "juste" gratuit objets de valeur.Utiliser des variables liées serait de la triche, il faut rester dans le domaine de la logique combinatoire.Utiliser des variables gratuites n'est pas de la triche, c'est un outil honnête.Ainsi, nous pouvons faire la preuve formelle dont vous avez besoin.

Aux simples axiomes d’égalité et aux règles d’inférence (transitivité, réflexivité, symétrie, règles de Leibniz), nous devons ajouter un extensionnalité règle d’inférence pour l’égalité.C'est ici que les variables libres comptent.

Dans Csörnyei 2007 :157-158, j’ai trouvé l’approche suivante.Je pense que de cette façon, la preuve peut être faite.

Quelques remarques :

La plupart des axiomes sont en fait schémas d'axiomes, composé d'une infinité d'instances d'axiomes.Les instances doivent être instanciées pour chaque possible E, F, g termes.Ici, j'utilise l'italique pour les métavariables.

La nature infinie superficielle des schémas d'axiomes ne posera pas de problèmes de calculabilité, car ils peuvent être résolus en un temps fini :notre système d'axiomes est récursif.Cela signifie qu'un analyseur intelligent peut décider en un temps fini (et de plus, très efficacement) si une proposition donnée est ou non une instance d'un schéma d'axiomes.Ainsi, l’utilisation de schémas d’axiomes ne pose aucun problème théorique ou pratique.

Voyons maintenant notre cadre :

Langue

ALPHABET

Constantes:Les trois suivantes sont appelées constantes : K, S, je.

J'ai ajouté la constante je uniquement parce que votre question présuppose que nous n'avons pas défini le combinateur je comme un simple alias/macro pour terme composé S K K, mais c'est une constante autonome en soi.

Je désignerai les constantes par des majuscules romaines en gras.

Signe de candidature:Un signe @ de ``application'' suffit (notation de préfixe avec arité 2).Comme sucre syntaxique, j'utilise ici des parenthèses à la place du signe d'application explicite :J'utiliserai les signes explicites d'ouverture (et de fermeture).

Variables:Bien que la logique combinatrice n'utilise pas de variables liées, de portée, etc., nous pouvons introduire des variables libres.Je soupçonne qu’ils ne sont pas seulement du sucre syntaxique, ils peuvent aussi renforcer le système de déduction.Je suppose que votre question nécessitera leur utilisation.Tout ensemble infini énumérable (disjoint des constantes et des signes de parenthèses) servira d'alphabet des variables, je les désignerai ici par des lettres minuscules romaines non formatées x, y, z...

TERMES

Les termes sont définis de manière inductive :

• Toute constante est un terme
• Toute variable est un terme
• Si E est un terme, et F est un terme aussi, alors aussi (E F) est un terme

J'utilise parfois des conventions pratiques comme sucre syntaxique, par ex.écrire

E F g H

au lieu de

(((E F) g) H).

Déduction

Schémas d'axiomes de conversion :

• ``K E F = E'' est déductible (K-axiome schème)
• ``S F g H = F H (g H)'' est déductible (Axiome S schème)
• ``je E = E'' est déductible (I-axiome schème)

J'ai ajouté le troisième axiome de conversion (je règle) uniquement parce que votre question présuppose que nous n'avons pas défini le combinateur je comme alias/macro pour S K K.

Schémas d'axiomes d'égalité et règles d'inférence

• ``E = E'' est déductible (Réflexivité axiome)
• Si "E = F" est déductible, alors "F = E" est également déductible (Symétrie règle d'inférence)
• Si "E = F" est déductible, et "F = g" est déductible aussi, donc aussi "E = g" est réductible (Transitivité règle)
• Si "E = F" est déductible, alors "E g = F g" est également déductible (Règle de Leibniz I)
• Si "E = F" est déductible, alors "g E = g F" est également déductible (Règle de Leibniz II)

Question

Maintenant, étudions votre question.Je suppose que le système de déduction défini jusqu'à présent n'est pas suffisamment solide pour prouver votre question.

Est-ce que la proposition "je = S K K" déductible ?

Le problème est que nous devons prouver l’équivalence des fonctions.Nous considérons deux fonctions comme équivalentes si elles se comportent de la même manière.Les fonctions agissent de manière à être appliquées aux arguments.Nous devons prouver que les deux fonctions agissent de la même manière si elles sont appliquées à chacun des arguments possibles.Encore une fois, le problème de l'infini !Je soupçonne que les schémas d'axiomes ne peuvent pas nous aider ici.Quelque chose comme

Si E F = g F est déductible, alors aussi E = g est déductible

ne parviendrait pas à faire le travail :nous pouvons voir que cela ne donne pas ce que nous voulons.En l'utilisant, nous pouvons prouver que

``je E = S K K E'' est déductible

pour chaque E terme instance, mais ces résultats ne sont que des instances séparées et ne peuvent pas être utilisés dans leur ensemble pour des déductions ultérieures.Nous n’avons que des résultats concrets (une infinité), sans pouvoir les résumer :

• ça tient pour E := K
• tient pour E := S
• ça tient pour E := K K
• .
• .
• .

...

nous ne pouvons pas résumer ces instances de résultats fragmentés en un seul grand résultat, en affirmant l'extensionnalité !Nous ne pouvons pas verser ces fragments de faible valeur dans l’entonnoir, une règle d’inférence qui les fusionnerait en un seul résultat plus précieux.

Nous devons augmenter la puissance de notre système de déduction.Nous devons trouver un outil formel capable de saisir le problème.Vos questions mènent à l'extensionnalité, et je pense qu'en déclarant l'extensionnalité, nous devons pouvoir poser des propositions valables pour les instances *****arbitraires*****.C'est pourquoi je pense que nous devons autoriser les variables libres dans notre langage objet.Je suppose que la règle d'inférence supplémentaire suivante fera le travail :

• Si la variable x ne fait pas partie des termes non plus E ni F, et la déclaration (E x) = (F x) est déductible, alors E = F est également déductible (Extensionnalité règle d'inférence)

La chose difficile dans cet axiome, qui prête facilement à confusion :x est un objet variables, parties pleinement émancipées et respectées de notre langage objet, tout en E et g sont métavariables, qui ne font pas partie du langage objet, mais sont utilisées uniquement pour une notation concise des schémas d'axiomes.

(Remarque:Plus précisément, la règle d’inférence d’extensionnalité devrait être formalisée de manière plus prudente, en introduisant une métavariable X dans tout ce qui est possible objet variables x, y, z..., et aussi un autre type de métavariable E dans tout ce qui est possible instances de terme.Mais cette distinction entre les deux types de métavariables plus les variables objets n'est pas si didactique ici, elle n'affecte pas trop votre question.)

Preuve

Démontrons maintenant la proposition selon laquelle ``je = S K K''.

Étapes pour le côté gauche :

• proposition ``je x = x'' est une instance de I-axiome régime avec instauration [E :=x]

Étapes pour le côté droit :

• Proposition "S K K X = K X (K x)" est un exemple de Axiome S schéma avec instanciations [E := K, F := K, g := x], donc c'est déductible
• Proposition "K X (K x) = x" est une instance de K-axiome schéma avec instanciations [E :=x, F := K x], il est donc déductible

Transitivité de l'égalité :

• Déclaration "S K K X = K X (K x)" correspond à la première prémisse de transitivité règle d'inférence et déclaration "K X (K x) = x" correspond à la deuxième prémisse de cette règle d'inférence.Les instanciations sont [E := S K K X, F := K X (K X), g =x].Ainsi, la conclusion est également valable : E = g.En réécrivant la conclusion avec les mêmes instanciations, on obtient l'énoncé "S K K x = x", ceci est donc déductible.

Symétrie d'égalité :

• En utilisant "S K K x = x", nous pouvons en déduire "x = S K K X"

Transitivité de l'égalité :

• En utilisant "je x = x" et "x = S K K x", on peut en déduire "je X = S K K X"

Nous avons désormais ouvert la voie au point crucial :

• Proposition "je X = S K K x" correspond à la première prémisse de Extension règle d'inférence :(E x) = (F x), avec des instanciations [E := je, F := S K K].Ainsi, la conclusion doit également être valable, c'est-à-dire : "E = F" avec les mêmes instanciations ([E := je, F := S K K]), ce qui donne la proposition "je = S K K", ce qu'il fallait démontrer.

---

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

Answer 2

Vous ne devez-je définir comme un axiome. Commencez par ce qui suit:

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

Depuis SKanything = anything, puis SKanything est une fonction d'identité, tout comme I.

Alors, I = SKK et I = SKS. Pas besoin de définir I comme un axiome, vous pouvez le définir comme le sucre de syntaxe qui alias SKK.

Les définitions de S et K sont vous seulement axiomes.

Answer 3

Les axiomes habituels sont complets pour l'égalité bêta, mais ne donnent pas l'égalité des eta. Curry a trouvé un ensemble d'une trentaine axiomes aux habituelles pour obtenir l'exhaustivité pour l'égalité bêta-eta. Ils sont répertoriés dans Hindley et Seldin de Introduction à combinateurs et lambda-calcul .

Roger Hindley, Dernière problème de Curry, énumère quelques-uns supplémentaires nous desiderata pourrait vouloir de correspondances entre le lambda-calcul et les notes que nous n'avons pas les correspondances qui satisfont tous. Vous aurez probablement pas beaucoup de soin sur tous les critères.