Comment montrer que deux modèles de calcul sont équivalents?

21

Je cherche des explications sur la façon dont on pourrait prouver que deux modèles de calcul sont équivalents. J'ai lu des livres sur le sujet, sauf que les preuves d'équivalence sont omises. J'ai une idée de base sur ce que cela signifie pour deux modèles de calcul d'être équivalents (la vue des automates: s'ils acceptent les mêmes langages). Y a-t-il d'autres façons de penser l'équivalence? Si vous pouviez m'aider à comprendre comment prouver que le modèle de la machine de Turing est équivalent au calcul lambda, ce serait suffisant.

saadtaame
la source
Je suppose que vous avez choisi les mauvais livres.
Raphael
@Raphael Qu'est-ce qu'un bon livre sur le sujet?
saadtaame
Je voudrais dire "n'importe quel livre sur les automates", mais apparemment c'est vrai. Malheureusement, je n'ai pas de livres en anglais à portée de main, désolé.
Raphael
1
Un livre sur les automates ne suffira pas.
reinierpost
Quels livres utilisez-vous?
saadtaame

Réponses:

20

Vous montrez que l'un ou l'autre modèle peut simuler l'autre, auquel est attribuée une machine dans le modèle A, montrez qu'il existe une machine dans le modèle B qui calcule la même fonction. Notez que cette simulation n'a pas besoin d'être calculable (mais l'est généralement).

Considérons, par exemple, les automates pushdown avec deux piles (2-PDA). Dans une autre question , les simulations dans les deux sens sont décrites. Si vous le faisiez formellement, vous prendriez une machine de Turing générale (un tuple) et construiriez explicitement ce que serait le 2-PDA correspondant, et vice versa.


Formellement, une telle simulation peut ressembler à ceci. Laisser

M=(Q,Σje,ΣO,δ,q0,QF)

être une machine de Turing (avec un ruban). Alors,

UNEM=(Q{q1,q2},Σje,ΣO,δ,q1,QF)

avec ΣO=ΣO.{$} et δ donnés par

(q1,a,hl,hr)δ(q1,ahl,hr) pour toutaΣI ethr,hlΣO ,
(q1,ε,hl,hr)δ(q2,hl,hr) pour touthr,hlΣO ,
(q2,ε,hl,hr)δ(q2,ε,hlhr) for all hr,hlΣO with hl$,
(q2,ε,$,hr)δ(q0,$,hr) for all hrΣO,
(q,ε,hl,hr)δ(q,ε,hla)(q,hr)δ(q,a,L) for all qQ and hlΣO,
(q,ε,$,hr)δ(q,$,a)(q,hr)δ(q,a,L) for all qQ,
(q,ε,hl,hr)δ(q,ahl,ε)(q,hr)δ(q,a,R) for all qQ,hlΣO,
(q,ε,hl,$)δ(q,hl,$) for all qQ and hlΣO, and
(q,ε,hl,hr)δ(q,hl,a)(q,hr)δ(q,a,N) for all qQ,hlΣO

is an equivalent 2-PDA. Here, we assume that the Turing machine uses ΣO as blank symbol, both stacks start with a marker $ΣO (which is never removed) and (q,a,hl,hr)δ(q,l1li,r1rj) means that AM consumes input a, switches states from q to q and updates the stacks like so:

stack update
[source]

It remains to show that AM enters a final state on xΣI if and only if M does so. This is quite clear by construction; formally, you have to translate accepting runs on M into accepting runs on AM and vice versa.

Raphael
la source
@frabala You were right, I had the initial states the wrong way around. Fixed now, thanks!
Raphael
4

At the beginning of Communicating and Mobile Systems: the Pi-Calculus by Robin Milner, there is a introduction on automata and how they can simulate each other so that they cannot be distinguished : Bisimulation. (cf Bisimulation on wikipedia)

I don't remember well, I should re-read the chapter, but there was a trouble with simulation and bisimulation that made them not sufficient for computational equivalences.

Thus Robin Milner introduces his Pi-Calculus and exposes it for the rest of the book.

Ultimately, in his last book The Space and Motion of Communicating Agents, you could have a look at Robin Milner's Bigraphs. They can model Automata, Petri nets, Pi-Calculus and other computational methodologies.

Stephane Rolland
la source
2

As far as I know, the only (or at least most common) way to do this is to compare the languages the machines/models accept. That's the whole point of Automata theory: it takes the vague concept of a problem or algorithm and turns it into a concrete mathematical set (i.e. a language) which we can reason about.

The easiest way to do this is, given an arbitrary machine/function from one model, to construct a machine from the second model that computes the same language. Odds are you'll use induction in the length of the expression, states in the machine, rules in the grammar, etc.

I haven't seen this done with Lambda and TMs (though I'm 99% sure it's possible), but I have definitely seen this kind of thing for proving equivalence of NFAs and Regular expressions. First you show a NFA which can accept any atom, then using induction, you make NFAs which accept the union/concatenation/Kleene-star of any smaller NFAs.

Then you do the opposite, to find an RE for any NFA.

jmite
la source