Domanda

Ho sentito dell'induzione (strutturale). Esso consente di costruire strutture finite da quelli più piccoli e ti dà i principi di prova per ragionare su tali strutture. L'idea è abbastanza chiaro.

Ma per quanto riguarda coinduzione? Come funziona? Come si può dire nulla conclusivo su una struttura infinita?

Ci sono (almeno) due angoli di indirizzo, vale a dire, coinduzione come un modo di definire le cose e come tecnica di prova.

Per quanto riguarda coinduzione come una tecnica di prova, qual è il rapporto tra coinduzione e bisimulazione?

È stato utile?

Soluzione

In primo luogo, per dissipare un possibile dissonanza cognitiva: ragionamento sulle strutture infinite non è un problema, lo facciamo tutto il tempo. Fino a quando la struttura è finitamente descrivibile, che non è un problema. Qui ci sono alcuni tipi comuni di strutture infinite:

  • lingue (insiemi di stringhe su alcuni alfabeto, che possono essere finiti);
  • Lingue albero (serie di alberi sopra un po 'di alfabeto);
  • tracce di esecuzione di un sistema non-deterministico;
  • numeri reali;
  • insiemi di interi;
  • set di funzioni da interi a numeri interi; ...

Coinductivity come il più grande punto fisso

Dove definizioni induttive costruire una struttura da blocchi elementari, le definizioni coinduttive forma strutture da come possono essere decostruite. Ad esempio, il tipo di liste cui elementi sono in una A set è definito come segue Coq: 

Inductive list (A:Set) : Set :=
  | nil : list A
  | cons : A -> list A -> list A.

Informalmente, il tipo di list è il tipo più piccolo che contiene tutti i valori costruiti dai nil e cons costruttori, con l'assioma che $ \ forall x \, y, \: \ mathtt {nil} \ ne \ mathtt {cons} \: x \: y $. Al contrario, siamo in grado di definire il tipo più grande che contiene tutti i valori costruiti da questi costruttori, mantenendo l'assioma discriminazione: 

CoInductive colist (A:Set) : Set :=
  | conil : colist A
  | cocons : A -> colist A -> colist A.

list è isomorfo a un sottoinsieme di colist. Inoltre, colist contiene infinite liste:. Liste con cocons su cocons 

CoFixpoint flipflop : colist ℕ := cocons 1 (cocons 2 flipflop).
CoFixpoint from (n:ℕ) : colist ℕ := cocons n (from (1 + n)).

flipflop è l'infinito (lista circolare) $ 1 :: 2 :: 1 :: 2 :: \ ldots $; from 0 è la lista infinita dei numeri naturali $ 0 :: 1 :: 2 :: \ ldots $.

Una definizione ricorsiva è ben formata se il risultato è costruito da blocchi più piccoli: chiamate ricorsive devono lavorare ingressi più piccoli. Una definizione corecursive è ben formata se il risultato costruisce oggetti più grandi. Induzione guarda costruttori, coinduzione guarda distruttori. Si noti come il dualità non solo piccoli cambiamenti al più grande, ma anche gli ingressi alle uscite. Ad esempio, la ragione le flipflop e from definizioni di cui sopra sono ben formate è che la chiamata corecursive è protetta da una chiamata al costruttore cocons in entrambi i casi.

Se le dichiarazioni sugli oggetti induttivi hanno prove induttive, frasi con oggetti coinduttive avere prove coinduttive. Per esempio, definiamo il predicato infinito su colists; intuitivamente, le infinite colists sono quelli che non terminano con conil. 

CoInductive Infinite A : colist A -> Prop :=
  | Inf : forall x l, Infinite l -> Infinite (cocons x l).

Per dimostrare che colists della forma from n sono infinite, possiamo ragionare da coinduzione. from n è uguale a cocons n (from (1 + n)). Questo dimostra che from n è maggiore di from (1 + n), che è infinita dall'ipotesi coinduzione, quindi from n è infinita.

bisimilarità, una proprietà coinduttiva

coinduzione come una tecnica di prova si applica anche agli oggetti finitari. Intuitivamente parlando, prove induttive di un oggetto sono basate su come l'oggetto viene costruito. prove coinduttiva si basano su come l'oggetto può essere scomposto.

Quando si studia sistemi deterministici, è comune per definire l'equivalenza attraverso regole induttive: due sistemi sono equivalenti se si può ottenere da uno all'altro da una serie di trasformazioni. Tali definizioni tendono a non riuscire a catturare i molti modi diversi sistemi non deterministici possono finire per avere lo stesso comportamento (osservabile) pur avendo differente struttura interna. (Coinduzione è utile anche per descrivere i sistemi non fatale, anche quando sono deterministico, ma questo non è quello che mi concentrerò su qui.)

sistemi non deterministiche quali sistemi concorrenti sono spesso modellate da etichettato sistemi . Un LTS è un grafo orientato incui i bordi sono etichettati. Ciascun bordo rappresenta una possibile transizione del sistema. Una traccia di un LTS è la sequenza di etichette di bordo su un percorso nel grafico.

Due LTS può comportarsi in modo identico, in quanto hanno gli stessi eventuali tracce, anche se la loro struttura interna è differente. Grafico isomorfismo è troppo forte per definire la loro equivalenza. Invece, un LTS $ \ mathscr {A} $ si dice che simulare un'altra LTS $ \ mathscr {B} $ se ogni transizione del secondo LTS ammette una transizione corrispondente nel primo. Formalmente, sia $ S $ essere l'unione disgiunta degli stati dei due LTS, $ L $ il (comune) serie di etichette e $ \ rightarrow $ la relazione di transizione. La relazione $ R \ subseteq S \ volte S $ è una simulazione, se $$ \ forall (p, q) \ in R,% \ forall p '\ in S, \ forall \ alpha \ in L, \ Text {if} p \ stackrel \ alpha \ rightarrow p' \ Text {} quindi \ esiste q', \; q \ stackrel \ alpha \ rightarrow q '\ text {} e (p', q ') \ in R $$

$ \ mathscr {A} $ simula $ \ mathscr {B} $ se v'è una simulazione in cui tutti gli stati di $ \ mathscr {B} $ sono legati a uno stato in $ \ mathscr {A} $. Se $ R $ è una simulazione in entrambe le direzioni, si parla di un bisimulazione . La simulazione è una proprietà coinduttiva:. Alcuna osservazione da una parte deve avere una corrispondenza sul lato opposto

Ci sono potenzialmente molte bisimulazioni in un LTS. Diversi bisimulazioni potrebbero identificare i diversi stati. Dati due bisimulazioni $ R_1 $ e $ R_2 $, la relazione data prendendo l'unione del rapporto rappresenta graficamente $ R_1 \ tazza R_2 $ è essa stessa una bisimulazione, dal momento che gli stati relativi danno origine a stati correlati per entrambi i rapporti. (Questo vale per le unioni infiniti come bene. La relazione vuoto è un bisimulazione Unintersting, come è il rapporto identità.) In particolare, l'unione di tutte bisimulazioni sé è una bisimulazione, chiamato bisimilarità. Bisimilarità è il modo più grossolano di osservare un sistema che non distingue tra stati distinti.

bisimilarità è una proprietà coinduttiva. Esso può essere definito come il più grande punto di rilevamento di un operatore: è il più grande rapporto che, quando esteso per identificare stati equivalenti, rimane la stessa

.

Bibliografia

  • Coq e il calcolo delle costruzioni induttivi

    • Yves Bertot e Pierre CASTERAN. Interactive teoremi e Programma di Sviluppo - Coq'Art: The Calculus of induttivo edili . Springer, 2004. Ch. 13. [ sito ] [ Amazon ]
    • Eduardo Giménez. Un'applicazione di tipo co-induttivo in coq: verifica del protocollo bit alternata . In Workshop sui tipi di prove e programmi , il numero 1158 in Lecture Notes in Computer Science , pagine 135-152. Springer-Verlag, 1995. [ di Google Libri ]
    • Eduardo Giménez e Pierre CASTERAN. Un tutorial su tipologie [Co] induttivi in ??Coq. 2007. [ PDF ]

  • sistemi di transizione etichettati e bisimulazioni

    • Robin Milner. Comunicazione e concorrenza . Prentice Hall, 1989.
    • Davide Sangiorgi. Sulle origini di bisimulazione e coinduzione . Le transazioni ACM su Linguaggi di Programmazione e Sistemi (TOPLAS), il volume 31 numero 4, maggio 2009. [ PDF ] [ ACM ] associate diapositive corso: [ PDF ] [ CiteSeer ]

    • Davide Sangiorgi. Il pi-calcolo: A Theory of mobile Processi . Cambridge University Press, 2003. [ Amazon ]

    • Un capitolo in Programmazione Certificato con tipi dipendenti A. Chlipala

    • D. Sangiorgi. "Introduzione alla bisimulazione e coinduzione". 2011. [ PDF ]
    • D. Sangiorgi e J. Rutten. Argomenti avanzati in bisimulazione e coinduzione . Cambridge University Press, 2012. [ CUP ]

Altri suggerimenti

Si consideri la seguente definizione induttiva:

$ \ qquad \ displaystyle \ begin {* align} & \ Phantom {\ Rightarrow} \ quad \ epsilon \ in \ mathcal {} T \\ w \ in \ mathcal {T} \ quad & \ Rightarrow \ quad aw \ in \ mathcal {} T \\ aw \ in \ mathcal {T} \ quad & \ Rightarrow \ quad baw \ in \ mathcal {T} \ End {align *} $

Qual è $ \ mathcal {} T $? Chiaramente, l'insieme di stringhe senza due successive $ b $, cioè

$ \ qquad \ displaystyle \ mathcal {T} = \ {\ epsilon, A, AA, BA, aaa, ABA, \ dots \} = \ mathcal {L} \ left ((BA \ metà a) ^ * \ right) \ subseteq \ Sigma ^ *. $

A destra? Ebbene, che cosa abbiamo bisogno per questo è la frase innocua "e $ \ mathcal {T} $ è l'insieme più piccolo che soddisfa queste condizioni". Abbastanza vero, altrimenti $ \ mathcal {T} = \ {a, b \} ^ * $ avrebbe funzionato, anche.

Ma c'è di più ad esso che quello. Scrivi sopra definizione in quanto (monotona) funzione $ f: 2 ^ {\ Sigma ^ \ infty} \ 2 ^ {\ Sigma ^ \ infty} $:

$ \ qquad f (T) = T \ tazza \ {\ epsilon \} \ tazza \ {aw \ mid w \ in T \} \ tazza \ {baw \ metà aw \ in T \} $

Ora $ \ mathcal {T} $ è il più piccolo punto fisso di $ f $. Infatti, a causa $ f $ è monotona e $ \ left (2 ^ {\ Sigma ^ \ infty}, \ subseteq \ right) $ è una completa reticolo , Knaster-Tarski teorema ci dice che un tale piccolo punto fisso esiste ed è un linguaggio corretto. Perché Questo funziona con qualsiasi definizione induttiva reasonable¹, normalmente non parliamo di questo. Si adatta solo la nostra intuizione: si comincia con $ \ {\ epsilon \} $ e applicare il passo per passo le regole; al limite, otteniamo $ \ mathcal {T} $.

Ora noi cambiare le cose. Invece di dire "se è incluso $ w $, quindi è $ $ aw" diciamo "se $ $ AW è incluso, così deve essere stato $ w $". Non possiamo girare l'ancora in giro, così si va via. Che ci lascia con un problema: dobbiamo essere in grado di prendere arbitrariamente lungo prefissi lontano da qualsiasi parola a $ \ mathcal {T} '$ e rimangono in $ \ mathcal {T}' $! Questo non è possibile con le parole finite; buona cosa che furtivamente in $ \ Sigma ^ \ infty $ sopra! Si finisce con il set di parole infinite senza un fattore (stringa) $ bb $, vale a dire $ \ mathcal {T} '= \ mathcal {L} \ left ((BA \ metà a) ^ \ omega \ right) $.

In termini di $ F $, $ \ mathcal {T} '$ è la sua più grande fixpoint². Questo è in realtà abbastanza intuitivo: non possiamo sperare di colpire $ \ mathcal {T} '$ da sotto , cioè induttivamente partendo da $ \ {\ epsilon \} $ e aggiungendo roba che soddisfa le regole, così si passa da sopra , cioè coinductively partendo da $ \ Sigma ^ \ infty $ e rimozione roba che fa non essere conformi alle regole.

Notazione:

  • $ \ Sigma ^ \ infty = \ Sigma ^ * \ tazza \ Sigma ^ \ omega $
  • $ \ Sigma ^ \ omega $ è l'insieme di tutte le infinito le sequenze di oltre $ \ Sigma $.

¹ Lei non è permesso di fare cose come $ w \ in \ mathcal {T} \ Rightarrow aw \ notin \ mathcal {T} $; la funzione corrispondente non sarebbe monotona.
² Dobbiamo spazzare $ \ {\ epsilon \} $ sotto il tappeto in qualche modo.

Autorizzato sotto: CC-BY-SA insieme a attribuzione
Non affiliato a cs.stackexchange
scroll top