Agacement formalisation de machine abstraite

Salut GA ! La forme j’espère

Pour le test à 0 si tu parles du goto conditionnel je l’ai mis, si tu parles de mettre à 0 un registre, je l’ai pas dans la def de programme goto.

Je refais la formalisation pour qu’elle colle plus à la démo « calculable=> récursif »... et la traduction en terme d’apps récursives se fasse naturellement à codage près.

J’appelle MA, l’ensemble des machines abstraites à programme goto.
Formellement c’est $\{(M,E_{M}), \exists k\exists n \exists I\exists (S_{1},...,S_{n})\in \mathbb{N}^{n}, \\
I=\{(0,i), i\in [1,k]\}\cup \{(1,i), i\in [1,k]\}\cup \{(2,i,j), i\in [1,k],j\in [1,n]\}\cup \{(3.0)\},\\ M=(k,(S_{1},...,S_{n})),\\E_{M}=[1,n]\times \mathbb{N}^{k} \}$
$M1=\{M,\exists E, (M,E)\in MA\}$
$UM2=\cup\{E,\exists M, (M,E)\in MA\}$
-Reg1 est l’app de UM2 dans $\mathbb{N}$ telle que pour $e\in UM2$ Reg1(e)=$R_{1}$ tel qu’il existe $(R_{2},...,R_{k})$ et $i\in [1,n]$ tel que $e=(i,(R_{1},...,R_{k}))$

-Tr est l’app de $\underset{M\in M1}\cup\{M\}\times E_{M}$ dans $\underset{M\in M1}\cup E_{M}$ telle que pour (M,e) dans son domaine $Tr(M,e)=e’$ tel que, si $M=(k,(S_{1},...,S_{n}))$, $e=(i,(R_{1},...R,_{k}))$, et soit $m\in [1,k]$ et $p\in [1,n]$,
-Si $S_{i}=(0,m)$ alors $e’=(i+1,(R_{1},...,R_{m}+1,..,R_{k}))$
-Si $S_{i}=(1,m)$ alors, si $R_{m}=0$ alors $e’=(i+1,(R_{1},...,R_{m},..,R_{k}))$, sinon $e’=(i+1,(R_{1},...,R_{m}-1,..,R_{k}))$
-Si $S_{i}=(2,m,p)$ alors si $R_{m}=0$ alors $e’=(p,(R_{1},...,R_{k}))$ sinon $e’=(i+1,(R_{1},...,R_{k}))$
-Sinon e’=e

Remarque: Tr est bien définie comme ça, on peut le vérifier pour toutes les autres apps que je définis

-Init est l’app de $M1\times \underset{p>0}\cup \mathbb{N}^{p}$ dans $\underset{M\in M1}\cup E_{M}$ qui à M,x1,...,xp dans son domaine associe (1,(x1,...,xk)) si k tel que c’est l’entier qu’on imagine est plus petit que p, sinon on complète avec des 0. c’est très salement défini comme ça mais ça se fait par induction si on veut être propre.

-Halte est l’app de $\underset{M\in M1}\cup\{M\}\times E_{M}$ dans {0,1} telle que pour (M,e) dans son domaine avec M=(k,(S1,...,Sn)), e=(i,(R1,...,Rk)), Halte(M,e)=1 si Si = (3,0), vaut 0 sinon.

-Run est une app de $M1\times \underset{p>0}\cup \mathbb{N}^{p}\times \mathbb{N}$ dans $\underset{M\in M1}\cup E_{M}$ telle que pour M,(x1,...,xp),0 dans son domaine elle donne init(M,x1,...,xp)
Et par induction, M,x1,...,xp,y+1 donne Tr(M,Run(M,x1,..,xp,y)).

-j’appelle MuRun une fonction de domaine inclus dans $M1\times \underset{p>0}\cup \mathbb{N}^{p}$ qui est l’ensemble des (M,(x1,...,xp)) tels qu’il existe n tel que Halte(M,Run(M,x1,...,xp,n))=1... j’appelle ce domaine Dom(MuRun)
Pour M,x1,...,xp dans Dom(MuRun), MuRun vaut min(n, tq Halte(M,Run(M,x1,...,xp,n))=1).


Enfin je définis Phi une fonction de domaine Dom(MuRun) qui à M,x1,..,xp dans son domaine associe Reg1(Run(M,x1,...,xp,MuRun(M,x1,...,xp)))

Je dis qu’une fonction partielle F de $\mathbb{N}^{p}$ dans les entiers est calculable SSI il existe $M\in M1$ tel que $\{M\}\times Dom(F)$ est inclus dans Dom(Phi) et que Phi et F « coïncident » dessus (enfin formellement c’est faux c’est juste que pour tout x1,...,xp dans Dom(F), F(x1,...,xp)=Phi(M,x1,...,xp)


Question: est-ce qu’il existe une définition générale de machine abstraite ? Sinon, est-ce que c’est parce que répondre à cette question revient à formaliser la thèse de church ?

« Ça ne parle aucunement de machine »
« [...] qu’une machine »
:-D

Je plaisante, j’attends ton lien avec plaisir !

Édit: de ce que je connais [large]C[/large]hurch c’est « calculable <=> récursif »
Mais calculable dans un sens qui n'est pas formel (au sens ne s’écrit pas en langue mathématique/des ensembles), on a jusqu’à maintenant ses instances de calculable formalisées par la notion de machine qui sont censées rendre compte du sens de calculable et pour lesquelles [large]C[/large]hurch est vrai avec l’homonyme « calculable pour telle machine ».

Je dis ça juste pour que tu saches ce dont je suis au courant pour que tu me situes.
Sachant que concrètement toutes les considérations autour de [large]C[/large]hurch que je connais sont des bruits de couloir. En pratique, je peux démontrer calculable pour certaines machines <=> récursif. Le côté « mais il y a un sens informel que les maths ne capturent pas et pour lequel le calculable défini mathématiquement est une forme de trace dans le langage maths qui ne satisfait pas le sens intuitif qu’on voudrait voir dans calculable » est flou dans ma tête parce que récent et très «raconté avec les mains » pour l’instant.

[Alonzo Church (1903-1995) prend toujours une majuscule. AD]

nan ça me parait pas clair encore, mais j’y reréfléchirai demain, ne serait- ce que pour te dire clairement ce qui me parait gênant. Mais du coup rapidement, est-ce qu’on peut dire que la thèse de [large]C[/large]hurch c’est « est-ce qu’il existe dans la nature une fonction des entiers dans les entiers qui n’est pas récursive ?»

Édit: question bête d’ailleurs, indépendamment de la thèse de [large]C[/large]hurch, est-ce qu’il y a moyen de tester dans la réalité si une fonction est récursive ou non ? (Vu que tous les ensembles d’entiers finis sont récursifs)

[Alonzo Church (1903-1995) prend toujours une majuscule. AD]