On considère le langage propositionnel engendré par l'élément 0, le connecteur binaire d'implication →, et des variables muettes x,y,z,... Une proposition est un arbre, où les nœuds ont toujours deux fils et ont tous la même étiquette →, et où les feuilles sont soit 0 ou soit une variable parmi x,y,z,...
On renomme les variables 1,2,3,... dans l'ordre de leur première occurrence dans le parcours de l'arbre (de la proposition) en profondeur d'abord, pour produire la proposition sous sa forme normale.
Les variables sont désignées par une ou plusieurs lettres et chiffres collés. Les propositions sont écrite sous forme de chaine de caractères. Exemple de proposition :
((x2→y)→0)→(y→x2)
Je demande à claude de programmer une fonction qui prend en argument une proposition et la convertie en sa forme normale. Il crée le module norm_form.py dans lequel la fonction forme_normale est définie. Exemple :
forme_normale('((x2→y)→0)→(y→x2)') = '((1→2)→0)→(2→1)'
forme_normale('2→1') retourne '2→1'. Or il devrait retourner '1→2'. Je demande à claude de corriger forme_normale pour qu'il fonctionne correctement même lorsque les variables sont des entiers.
On enrichie le langage des propositions qui sont des arbres en permettant de définir des propositions qui ont des graphes. On conçoit pour cela une notation pratique pour désigner ces propositions graphes. On utilise des noms de variables supplémentaires qui, accolés au signe égal, servent de label. Le label ne doit être présent qu'une seul fois par telle variable. (Le signe d'égalité s'apparente à une opération binaire de priorité syntaxique plus forte que l'opération →). Exemples :
x=(y→z)→x
y→x=(y→x)
x=(y=(z→x)→y)
Je demande à claude de reprogrammer les fonctions précédentes (forme_normale et unifier) pour qu'elles intègrent cette extension du langage propositionnel.
Je demande à claude de programmer une unifier_fini qui n'autorise pas l'affectation de variable à une proposition cyclique (qui est un graphe contenant au moins un cycle).
`"R1"` : `|-- a"→"(b"→"a)` `"R2"` : `|-- (a"→"(b"→"c))"→"((a"→"b)"→"(a"→"c))`
`"R3"` : `|-- ((a"→⊥")"→"(b"→⊥")) "→"(b"→"a)`
`"R4"` : `a, a"→"b |-- b`