Substitution simultanée

[Utilisateur supprimé] · February 2022

On se donne un langage $L$.
Pour tous termes $t,s$ de $L$, pour toute variable $v$ de $L$, on notera $(t,v)(s)$ la substitution $s$ à $v$ dans $t$>
Et dans le cas général, on note $(t,(v_1 ,...,v_n))(s_1 ,...,s_n ):= (....((t,v_1),v_2 )(s_2)...)(s_n)$

On rencontre un petit problème lorsque l'on rencontre une expression de la forme $(t,(x,y))(y,x)$ intuitivement, on voudrait juste intervertir les $x$ et $y$ dans $t$, mais cela n'est pas ce que fait notre substitution. Donc mise à part sa définition qui est très informelle et peu rigoureuse, cette notion montre la limitation que j'ai évoqué plus haut.

Ainsi, j'ai construit une substitution simultanée (qui interprète $(t,(x,y))(y,x)$ comme notre intuition le souhaite, par exemple) pour les termes et formules du second ordre, par récursion transfinie.

Par curiosité, dites moi si vous avez déjà rencontré une construction de substitution simultanée dans un livre et aussi quel serait votre construction.

Je ne suis pas sûr d'être très clair, j'ai tapé tout ça avec mon téléphone, donc j'ai du simplifier mon discours. Donc si vous voulez des précisions sur ce que je raconte, n'hésitez pas à me demander.

[Utilisateur supprimé] · February 2022

Bon, je retrouve mon ordinateur. On voudrait une application définie grosso modo sur $\{ (x,y,z)\vert \exists n\in \mathbb N , (x\in \tau (L) \wedge y\in \{ variables-fonctionnelles\} ^n \wedge z\in \{symboles-de-fonction \} ^n) \}$

Heuristique · February 2022

Tel quel, j'utiliserais une variable intermédiaire comme quand tu veux écrire algorithmiquement l'échange entre 2 variables $x$ et $y$.

Après, il faut l'écrire formellement et vérifier que tout se passe bien dans l'$\alpha$-renommage.

Il y a sûrement des ouvrages de $\lambda$-calcul qui traitent de ce genre de questions, mais je n'en ai pas sous la main...

Foys · February 2022

A mon avis si tu veux implémenter des formules (et afin de ménager ta santé mentale) oublie l'alpha-renommage et utilise des indices de Bruijn ou d'autres conventions ("locally nameless") pour représenter les variables.

[Utilisateur supprimé] · March 2022

Merci @Heuristique et @Foys, j'ai trouvé deux solutions à mon problème, mais ça m'a pris du temps:
1)une solution en utilisant la recursion transfinie sur la relation bien-fondée qu'on définie sur l'ensemble des termes, cette solution prend beaucoup de temps et nécessite beaucoup de travail, c'est lourd.

2) une solution plus algébrique qui consiste à voir l'ensemble des termes comme une structure libre $V$ de base $\emptyset$ sur le langage qui a pour fonctions l'ensemble des symboles de fonction de $L$ où on interprétant chaque fonction de façon canonique, à chaque fois qu'on veut faire une substitution, on se donne un morphisme de $V$ dans la structure obtenue en prennent l'ensemble termes comme univers et en interprétant chaque symbole de fonction par ce qui convient (ce par quoi on veut le remplacer).

Et pour l'alpha renommage, je suis d'accord, l'intention est noble mais dans l'exécution, c'est d'un compliqué. Une complication qui ne paraît pas nécessaire et qui oblige à faire maintes démonstrations pour des choses quasi évidentes (si on n'était pas passé par l'alpha renommage). Ça fait des années que je boycotte ce renommage.

Substitution simultanée

Réponses

Bonjour!

Catégories

In this Discussion

Qui est en ligne 8