Teória typov

Jazyk NBL

Ciele

  1. Formalizovať syntax, sémantiku a typy jazyka NBL.
  2. Odvodzovať kroky vyhodnotenia a typové úsudky.
  3. Dokazovať progres a zachovanie typu.
  4. Porovnať malé a veľké kroky a načrtnúť dôkaz ich ekvivalencie.

Obsah

Na základe predchádzajúcej prednášky o induktívnych výrokoch a uzáveroch na jazyku čísel a pravdivostných hodnôt NBL spojíme induktívne definované tvrdenia s opisom programovacieho jazyka. Definujeme termy, hodnoty, vyhodnocovanie a typové pravidlá. Následne dokážeme jednoznačnosť typu a bezpečnosť vyhodnocovania. Nasledujúca prednáška o zobrazeniach pripraví prostriedky na modelovanie kontextov; NBL premenné ani kontexty nepotrebuje.

  • Syntax a konkrétna notácia termov
  • Hodnoty, malé kroky, viackrokové vyhodnocovanie a veľké kroky
  • Typový systém a typové odvodenia
  • Kanonické hodnoty, progres a zachovanie typu
  • Ekvivalencia sémantík ako úloha na samostatný dôkaz

NBL – jazyk čísel a pravdivostných hodnôt

Úvod k jazyku NBL

Jazyk NBL je minimalistický jazyk, ktorý kombinuje:

  • booleovské hodnoty (true, false),
  • prirodzené čísla (0, succ, pred , iszero),
  • a základné podmienené výrazy (if ... then ... else ...).

V systéme Rocq formálne zadefinujeme a analyzujeme:

  • syntaktickú štruktúru programu (ako sa termy skladajú),
  • sémantiku (ako sa termy vyhodnocujú krok za krokom),
  • typový systém, ktorý zaručuje, že "správne typovaný program sa nikdy nezasekne",
  • a formálne dokážeme bezpečnosť navrhnutého jazyka.

Postup:

  1. Syntax jazyka NBL
    • Definícia termov a notácie
    • Príklady konštrukcie jednoduchých výrazov
  2. Sémantika (vyhodnotenie)
    • Relácia malých krokov (t → t')
    • Viackrokové vyhodnotenie (t →* t')
    • Prirodzená sémantika veľkých krokov ($t\Downarrow v$)
    • Normálne formy
  3. Typový systém
    • Typy: Bool a Nat
    • Typové pravidlá
    • Príklady typovania
  4. Kanonické hodnoty a základné vety
    • Veta o jednoznačnosti typu
    • Vety o kanonických hodnotách
  5. Bezpečnosť jazyka (type soundness)
    • Veta o progresii
    • Veta o zachovaní typu (preservation)
  6. Ekvivalencia sémantík
    • Znenie vety a slovný náčrt dôkazu
    • Samostatné dokončenie formálneho dôkazu v zadaní

Syntax jazyka NBL

Termy zapisujeme v Backusovej–Naurovej forme (BNF). Metapremenná $t$ označuje ľubovoľný term a symbol $\mid$ oddeľuje alternatívy:

$$ t ::= \mathsf{true}\mid\mathsf{false}\mid\mathsf{if}\ t\ \mathsf{then}\ t\ \mathsf{else}\ t\mid 0\mid\mathsf{succ}\ t\mid\mathsf{pred}\ t\mid\mathsf{iszero}\ t. $$

Kódové bloky vykonávame postupne v poradí prednášky, v module nbl. Rozlišujeme termy jazyka NBL a výrazy hostiteľského jazyka Rocq.

Definícia v Rocq:

Module nbl.

Inductive nbl : Type :=
| tru : nbl
| fls : nbl
| zro : nbl
| iszro : nbl -> nbl
| prede : nbl -> nbl
| scc : nbl -> nbl
| ite : nbl -> nbl -> nbl -> nbl.

Príklad: Term zadaný abstraktnou syntaxou

Definition p := tru.
Print p. (* p = tru : nbl *)

Notácia pre konkrétnu syntax

Pre lepšiu čitateľnosť definujeme notáciu podobnú syntaxi NBL:

  • notácia ako v NBL,
  • potrebný vlastný rozsah (scope),
  • vlastná gramatika (custom entry) pre termy NBL

Notácia pre konkrátnu syntax:

Declare Custom Entry tm.
Declare Scope tm_scope.

Notation "'true'" :=
  (tru) (in custom tm at level 0): tm_scope.
Notation "'false'" :=
  (fls) (in custom tm at level 0): tm_scope.
Notation "<{ e }>" :=
  e (e custom tm at level 99): tm_scope.
Notation "( x )" :=
  x (in custom tm, x at level 99): tm_scope.
Notation "x" :=
  x (in custom tm at level 0, x constr at level 0): tm_scope.
Notation "'0'" :=
  (zro) (in custom tm at level 0): tm_scope.
Notation "'succ' x" :=
  (scc x) (in custom tm at level 90, x custom tm at level 80): tm_scope.
Notation "'pred' x" :=
  (prede x) (in custom tm at level 90, x custom tm at level 80): tm_scope.
Notation "'iszero' x" :=
  (iszro x) (in custom tm at level 80, x custom tm at level 70): tm_scope.
Notation "'if' c 'then' t 'else' e" :=
  (ite c t e)
    (in custom tm at level 90, c custom tm at level 80,
    t custom tm at level 80, e custom tm at level 80): tm_scope.

Local Open Scope tm_scope.

Zápis <{ t }> používa vlastnú gramatiku tm na vytvorenie termu NBL. Mimo neho zostávajú true a if ... then ... else ... bežnými výrazmi Rocq. Tieto dve úrovne zápisu preto nezamieňame.

Taktiež je možné využiť abstraktnú syntax z induktívnej definície typu nbl.

Príklad: Rozlíšenie termov NBL a výrazov Rocq

Check true.         (* true : bool *)
Check <{ true }>.   (* <{ true }> : nbl *)
Check tru.          (* <{ true }> : nbl *)

Definition p1 := <{ if true then 0 else true }>.
Check p1.   (* p1 : nbl *)
Definition p2 :=  if true then 0 else 1.
Check p2.   (* p2 : nat; podmienka má typ bool v Rocq. *)
Definition p3 := ite tru zro tru.
Check p3.   (* p3 : nbl *)

Príkaz Check p1 overuje typ nbl v Rocq, nie správnu typovanosť programu podľa typového systému NBL, ktorý zavedieme nižšie. Termy p1 a p3 sú syntakticky totožné, no v NBL nemajú typ: ich vetvy 0 a true majú odlišné typy.

Hodnoty jazyka NBL

Metapremenná $v$ označuje hodnotu a $nv$ numerickú hodnotu. Hodnotami sú booleovské konštanty alebo numerické hodnoty:

$$ v ::= \mathsf{true}\mid\mathsf{false}\mid nv. $$ $$ nv ::= 0\mid\mathsf{succ}\ nv. $$

Predikáty $\operatorname{bval}(t)$ a $\operatorname{nval}(t)$ vyjadrujú, že term má príslušný tvar hodnoty. Ich pravidlá sú:

$$ \frac{}{\operatorname{bval}(\mathsf{true})}\,{\scriptstyle(\mathrm{bvtrue})} $$ $$ \frac{}{\operatorname{bval}(\mathsf{false})}\,{\scriptstyle(\mathrm{bvfalse})} $$ $$ \frac{}{\operatorname{nval}(0)}\,{\scriptstyle(\mathrm{nv0})} $$ $$ \frac{\operatorname{nval}(t)}{\operatorname{nval}(\mathsf{succ}\ t)}\,{\scriptstyle(\mathrm{nvscc})} $$

$$ \operatorname{value}(t)\iff\operatorname{nval}(t)\lor\operatorname{bval}(t). $$

Definícia v Rocq:

Inductive bval : nbl -> Prop :=
| bvtrue : bval tru
| bvfalse : bval fls.

Inductive nval : nbl -> Prop :=
| nv0 : nval zro
| nvscc : forall t, nval t -> nval (scc t).

(** Hodnota je numerická alebo booleovská hodnota. *)
Definition value (t : nbl) := nval t \/ bval t.

Štrukturálna operačná sémantika

Nazývaná aj sémantika malých krokov (small step semantics).

Úsudok $t\to t'$ znamená, že term $t$ vykoná jeden krok na $t'$. V Rocq mu zodpovedá t --> t':

$$ \boxed{t\to t'} $$

Nad odvodzovacou čiarou sú premisy, pod ňou záver a napravo názov zodpovedajúceho konštruktora Rocq. Bezpremisové pravidlá možno použiť priamo. Premisu $\operatorname{nval}(v)$ zachovávame explicitne: pravidlá pre predchodcu a test nuly vyžadujú numerickú hodnotu.

Vyhodnocovacie pravidlá:

$$ \frac{}{\mathsf{if}\ \mathsf{true}\ \mathsf{then}\ t_1\ \mathsf{else}\ t_2\to t_1}\,{\scriptstyle(\mathrm{st\_iftrue})} $$ $$ \frac{}{\mathsf{if}\ \mathsf{false}\ \mathsf{then}\ t_1\ \mathsf{else}\ t_2\to t_2}\,{\scriptstyle(\mathrm{st\_iffalse})} $$ $$ \frac{t_1\to t_1'}{\mathsf{if}\ t_1\ \mathsf{then}\ t_2\ \mathsf{else}\ t_3\to\mathsf{if}\ t_1'\ \mathsf{then}\ t_2\ \mathsf{else}\ t_3}\,{\scriptstyle(\mathrm{st\_if})} $$
$$ \frac{t_1\to t_1'}{\mathsf{succ}\ t_1\to\mathsf{succ}\ t_1'}\,{\scriptstyle(\mathrm{st\_succ})} $$ $$ \frac{}{\mathsf{pred}\ 0\to 0}\,{\scriptstyle(\mathrm{st\_pred0})} $$ $$ \frac{\operatorname{nval}(v)}{\mathsf{pred}\;(\mathsf{succ}\ v)\to v}\,{\scriptstyle(\mathrm{st\_predsucc})} $$ $$ \frac{t_1\to t_1'}{\mathsf{pred}\ t_1\to\mathsf{pred}\ t_1'}\,{\scriptstyle(\mathrm{st\_pred})} $$ $$ \frac{}{\mathsf{iszero}\ 0\to\mathsf{true}}\,{\scriptstyle(\mathrm{st\_iszero0})} $$ $$ \frac{\operatorname{nval}(v)}{\mathsf{iszero}\;(\mathsf{succ}\ v)\to\mathsf{false}}\,{\scriptstyle(\mathrm{st\_iszeronv})} $$ $$ \frac{t_1\to t_1'}{\mathsf{iszero}\ t_1\to\mathsf{iszero}\ t_1'}\,{\scriptstyle(\mathrm{st\_iszero})} $$

Definícia v Rocq:

Reserved Notation "t '-->' t'" (at level 40).

Inductive smallstep : nbl -> nbl -> Prop :=
  | st_iftrue : forall t1 t2,
      <{ if true then t1 else t2 }> --> t1
  | st_iffalse : forall t1 t2,
      <{ if false then t1 else t2 }> --> t2
  | st_if : forall c c' t2 t3,
      c --> c' ->
      <{ if c then t2 else t3 }> --> <{ if c' then t2 else t3 }>
  | st_succ : forall t1 t1',
      t1 --> t1' ->
      <{ succ t1 }> --> <{ succ t1' }>
  | st_pred0 :
      <{ pred 0 }> --> <{ 0 }>
  | st_predsucc : forall v,
      nval v ->
      <{ pred (succ v) }> --> v
  | st_pred : forall t1 t1',
      t1 --> t1' ->
      <{ pred t1 }> --> <{ pred t1' }>
  | st_iszero0 :
      <{ iszero 0 }> --> <{ true }>
  | st_iszeronv : forall v,
       nval v ->
      <{ iszero (succ v) }> --> <{ false }>
  | st_iszero : forall t1 t1',
      t1 --> t1' ->
      <{ iszero t1 }> --> <{ iszero t1' }>

where "t '-->' t'" := (smallstep t t').
#[local] Hint Constructors smallstep : core.

Poznámka

Príkaz #[local] Hint Constructors smallstep : core. definuje, že všetky konštruktory induktívnej relácie smallstep sa majú automaticky používať pri taktikách auto a eauto.

Atribút local obmedzuje hinty na tento modul. V praxi to znamená, že pri pokuse o dôkaz tvrdenia v tvare t --> t' (teda že t vykoná malý krok na t'), Rocq sa pokúsi sám nájsť vhodný konštruktor ako napríklad st_iftrue, st_predsucc, st_iszero, atď.

Príklad: Jeden krok vyhodnotenia

Podmienka true vyberie prvú vetvu v jednom kroku.

$$ \mathsf{if}\ \mathsf{true}\ \mathsf{then}\ \mathsf{succ}\ 0\ \mathsf{else}\ \mathsf{succ}\ 0\to\mathsf{succ}\ 0. $$

Formalizácia a dôkaz v Rocq:

Theorem ex1:
  <{if true then succ 0 else succ 0 }> --> <{ succ 0 }>.
Proof.
  apply st_iftrue.
Qed.

Print ex1.

Podmienka true vyberie prvú vetvu v jednom kroku.

$$ \mathsf{if}\ \mathsf{true}\ \mathsf{then}\ \mathsf{succ}\ 0\ \mathsf{else}\ \mathsf{succ}\ 0\to\mathsf{succ}\ 0. $$

Formalizácia a dôkaz v Rocq:

Theorem ex1_auto:
  <{if true then succ 0 else succ 0 }> --> <{ succ 0 }>.
Proof.
  auto. (* Automaticky nájde st_iftrue *)
Qed.

Print ex1_auto.

Reflexívno-tranzitívny uzáver (multi-step)

Relácia multistep opisuje nula alebo viac krokov relácie smallstep. Konštruktor multi_refl predstavuje nula krokov a multi_tran pripája jeden krok pred zvyšok konečnej cesty. Ide o reflexívno-tranzitívny uzáver z prednášky 06; namiesto spájania dvoch celých ciest ho tu definujeme skladaním po jednom kroku.

$$ \frac{}{t\to^{*}t}\,{\scriptstyle(\mathrm{multi\_refl})} $$ $$ \frac{t_1\to t_2\qquad t_2\to^{*}t_3}{t_1\to^{*}t_3}\,{\scriptstyle(\mathrm{multi\_tran})} $$

Matematický zápis $t\to^{*}t'$ zodpovedá multistep t t', resp. t -->* t'. Hviezdička pripúšťa aj nulový počet krokov.

Inductive multistep : nbl -> nbl -> Prop :=
  | multi_refl : forall t, multistep t t
  | multi_tran : forall t1 t2 t3,
      smallstep t1 t2 ->
      multistep t2 t3 ->
      multistep t1 t3.

Notation "t1 '-->*' t2" := (multistep t1 t2) (at level 40).
#[local] Hint Constructors multistep : core.

Príklad: Viackrokové vyhodnotenie troma spôsobmi

Podmienený výraz sa vo viacerých krokoch vyhodnotí na nulu.

$$ \mathsf{if}\ \mathsf{true}\ \mathsf{then}\ \mathsf{pred}\ 0\ \mathsf{else}\ 0\to^{*}0. $$

Formalizácia a dôkaz v Rocq:

Example ex_multistep :
  multistep <{(if true then pred 0 else 0)}> <{0}>.
Proof.
    apply multi_tran with (t2 := <{pred 0}>).
    - (* ============================
        <{ if true then (pred 0) else 0}> --> <{ pred 0 }> *)

      apply st_iftrue.
    - (* ============================
        <{ pred 0 }> -->* <{ 0 }> *)

       apply multi_tran with (t2 := <{0}>).
        + (* ============================
             <{ pred 0 }> --> <{ 0 }> *)

          apply st_pred0.
        + (* ============================
             <{ 0 }> -->* <{ 0 }> *)

           apply multi_refl.
Qed.

Print ex_multistep.

Rovnaký dôkaz s eauto:

Podmienený výraz sa vo viacerých krokoch vyhodnotí na nulu.

$$ \mathsf{if}\ \mathsf{true}\ \mathsf{then}\ \mathsf{pred}\ 0\ \mathsf{else}\ 0\to^{*}0. $$

Formalizácia a dôkaz v Rocq:

Example ex_multistep_eauto :
  multistep <{(if true then pred 0 else 0)}> <{0}>.
Proof.
  eauto.
Qed.

Dôkaz s eapply:

Podmienený výraz sa vo viacerých krokoch vyhodnotí na nulu.

$$ \mathsf{if}\ \mathsf{true}\ \mathsf{then}\ \mathsf{pred}\ 0\ \mathsf{else}\ 0\to^{*}0. $$

Formalizácia a dôkaz v Rocq:

Example ex_multistep_eapply :
  <{if true then pred 0 else 0}> -->* <{0}>.
Proof.
eapply multi_tran .
    - (* ============================
        <{ if true then (pred 0) else 0 }> --> ?t2 *)

       apply st_iftrue.
    - (* ============================
        <{ pred 0 }> -->* <{ 0 }> *)

       eapply multi_tran.
        + (* ============================
             <{ pred 0 }> --> ?t2 *)

          apply st_pred0.
        + (* ============================
             <{ 0 }> -->* <{ 0 }> *)

           apply multi_refl.
Qed.

Prirodzená operačná sémantika (veľké kroky)

Sémantika veľkých krokov opisuje úspešné vyhodnotenie celého termu na výslednú hodnotu. Úsudok čítame „term $t$ sa vyhodnotí na hodnotu $v$“:

$$\boxed{t\Downarrow v}$$

V Rocq ho zapíšeme t ==> v. Relácia bigstep má typ nbl -> nbl -> Prop; to, že jej druhý argument je hodnota, vyplýva z pravidiel, nie zo samotného typu relácie.

Vyhodnocovacie pravidlá:

$$ \frac{}{\mathsf{true}\Downarrow\mathsf{true}}\,{\scriptstyle(\mathrm{b\_true})} $$ $$ \frac{}{\mathsf{false}\Downarrow\mathsf{false}}\,{\scriptstyle(\mathrm{b\_false})} $$ $$ \frac{}{0\Downarrow0}\,{\scriptstyle(\mathrm{b\_zero})} $$
$$ \frac{t_1\Downarrow\mathsf{true}\qquad t_2\Downarrow v_3}{\mathsf{if}\ t_1\ \mathsf{then}\ t_2\ \mathsf{else}\ t_3\Downarrow v_3}\,{\scriptstyle(\mathrm{b\_iftrue})} $$ $$ \frac{t_1\Downarrow\mathsf{false}\qquad t_3\Downarrow v_3}{\mathsf{if}\ t_1\ \mathsf{then}\ t_2\ \mathsf{else}\ t_3\Downarrow v_3}\,{\scriptstyle(\mathrm{b\_iffalse})} $$ $$ \frac{t_1\Downarrow nv_1\qquad\operatorname{nval}(nv_1)}{\mathsf{succ}\ t_1\Downarrow\mathsf{succ}\ nv_1}\,{\scriptstyle(\mathrm{b\_succ})} $$ $$ \frac{t_1\Downarrow0}{\mathsf{pred}\ t_1\Downarrow0}\,{\scriptstyle(\mathrm{b\_predzero})} $$ $$ \frac{t_1\Downarrow\mathsf{succ}\ nv_1\qquad\operatorname{nval}(nv_1)}{\mathsf{pred}\ t_1\Downarrow nv_1}\,{\scriptstyle(\mathrm{b\_predsucc})} $$ $$ \frac{t_1\Downarrow0}{\mathsf{iszero}\ t_1\Downarrow\mathsf{true}}\,{\scriptstyle(\mathrm{b\_iszerozero})} $$ $$ \frac{t_1\Downarrow\mathsf{succ}\ nv_1\qquad\operatorname{nval}(nv_1)}{\mathsf{iszero}\ t_1\Downarrow\mathsf{false}}\,{\scriptstyle(\mathrm{b\_iszerosucc})} $$

Pravidlá pre if najprv vyhodnotia podmienku a potom iba vybranú vetvu. Pravidlá pre succ, pred a iszero vyhodnotia argument; pri numerických výsledkoch explicitne požadujú $\operatorname{nval}(nv_1)$. Metapremenná $nv_1$ označuje numerickú hodnotu, zatiaľ čo v deklarácii Rocq je nv1 : nbl obyčajným termom a dôkaz nval nv1 musíme uviesť zvlášť.

Formalizácia v Rocq:

Reserved Notation "t '==>' v" (at level 40).

Inductive bigstep : nbl -> nbl -> Prop :=
  | b_true :
      <{ true }> ==> <{ true }>
  | b_false :
      <{ false }> ==> <{ false }>
  | b_zero :
      <{ 0 }> ==> <{ 0 }>
  | b_iftrue : forall t1 t2 t3 v3,
      t1 ==> <{ true }> ->
      t2 ==> v3 ->
      <{ if t1 then t2 else t3 }> ==> v3
  | b_iffalse : forall t1 t2 t3 v3,
      t1 ==> <{ false }> ->
      t3 ==> v3 ->
      <{ if t1 then t2 else t3 }> ==> v3
  | b_succ : forall t1 nv1,
      t1 ==> nv1 ->
      nval nv1 ->
      <{ succ t1 }> ==> <{ succ nv1 }>
  | b_predzero : forall t1,
      t1 ==> <{ 0 }> ->
      <{ pred t1 }> ==> <{ 0 }>
  | b_predsucc : forall t1 nv1,
      t1 ==> <{ succ nv1 }> ->
      nval nv1 ->
      <{ pred t1 }> ==> nv1
  | b_iszerozero : forall t1,
      t1 ==> <{ 0 }> ->
      <{ iszero t1 }> ==> <{ true }>
  | b_iszerosucc : forall t1 nv1,
      t1 ==> <{ succ nv1 }> ->
      nval nv1 ->
      <{ iszero t1 }> ==> <{ false }>
where "t '==>' v" := (bigstep t v).

#[local] Hint Constructors bigstep : core.

Príklad: Rovnaký výsledok pomocou veľkých krokov

Výraz z príkladu viackrokového vyhodnotenia sa vyhodnotí na nulu. Podmienka true zvolí prvú vetvu a pravidlo pre predchodcu nuly určí jej výsledok:

$$\mathsf{if}\ \mathsf{true}\ \mathsf{then}\ \mathsf{pred}\ 0\ \mathsf{else}\ 0\Downarrow0.$$

Example ex_bigstep :
  <{ if true then pred 0 else 0 }> ==> <{ 0 }>.
Proof.
  apply b_iftrue.
  - apply b_true.
  - apply b_predzero. apply b_zero.
Qed.

Poznámka

Veľký krok opisuje vyhodnotenie až na hodnotu. Relácia $t\to^{*}t'$ však pripúšťa aj zastavenie v medzivýsledku, ktorý ešte nie je hodnotou; obsahuje napríklad nulovú cestu $t\to^{*}t$ pre každý term. Zaseknutý term, napríklad $\mathsf{if}\ 0\ \mathsf{then}\ \mathsf{true}\ \mathsf{else}\ \mathsf{false}$, nemá odvodenie veľkého kroku. Preto pri porovnaní sémantík treba k viackrokovej ceste pripojiť podmienku, že jej koniec je hodnota.

Normálne formy

Term je v normálnej forme, ak nemôže vykonať ďalší krok. Hodnota má tvar určený predikátom value. Zaseknutý term je normálna forma, ktorá nie je hodnotou. Každá hodnota NBL je normálnou formou, opačná implikácia však pre všetky termy neplatí.

$$ \operatorname{normal\_form}(t)\iff\neg\exists t'.\ t\to t'. $$

$$ \operatorname{stuck}(t)\iff\operatorname{normal\_form}(t)\land\neg\operatorname{value}(t). $$

Označenie $\operatorname{stuck}$ používame len v matematickom výklade; v Rocq túto vlastnosť vyjadríme konjunkciou.

Definition normal_form (t : nbl) : Prop :=
   ~exists t', smallstep t t'.

Tvrdenie, že hodnoty nemajú ďalší krok, dokážeme rozborom ich tvaru a indukciou podľa dôkazu nval:

Každá hodnota je v normálnej forme.

$$ \forall t.\quad\operatorname{value}(t)\implies\operatorname{normal\_form}(t). $$

Formalizácia a dôkaz v Rocq:

Lemma value_normal_form : forall t, value t -> normal_form t.
Proof.
  intros t [Hnv | Hbv].
  - unfold normal_form. intros [t' Hstep].
    generalize dependent t'.
    induction Hnv as [| t Hnv IH]; intros t' Hstep.
    + inversion Hstep.
    + inversion Hstep; subst. eapply IH. eassumption.
  - unfold normal_form. intros [t' Hstep].
    destruct Hbv; inversion Hstep.
Qed.

Príklad: Zaseknutá podmienka

Term if 0 then true else false nie je hodnotou a nemá ďalší krok, pretože nula sa nevyhodnocuje a pravidlá výberu vetvy vyžadujú true alebo false.

Podmienený výraz s nulou na mieste podmienky je zaseknutý.

$$ \operatorname{normal\_form}(\mathsf{if}\ 0\ \mathsf{then}\ \mathsf{true}\ \mathsf{else}\ \mathsf{false})\land\neg\operatorname{value}(\mathsf{if}\ 0\ \mathsf{then}\ \mathsf{true}\ \mathsf{else}\ \mathsf{false}). $$

Formalizácia a dôkaz v Rocq:

Example stuck_if_zero :
  normal_form <{ if 0 then true else false }> /\
  ~ value <{ if 0 then true else false }>.
Proof.
  split.
  - intros [t' Hstep].
    inversion Hstep as [| | c c' t2 t3 Hzero | | | | | | |]; subst.
    inversion Hzero.
  - intros [Hnv | Hbv].
    + inversion Hnv.
    + inversion Hbv.
Qed.

Príklad: Term s ďalším krokom nie je v normálnej forme

Test nuly na nule môže vykonať krok, a preto nie je v normálnej forme.

$$ \neg\operatorname{normal\_form}(\mathsf{iszero}\ 0). $$

Formalizácia a dôkaz v Rocq:

Theorem ex_normal_form_not_true :
~(normal_form <{iszero 0}>).
Proof.
  unfold normal_form.
  intros H.
  apply H.
  exists <{true}>.
  apply st_iszero0.
Qed.

Typový systém

Kategóriu typov tvorí booleovský typ a typ prirodzených čísel:

$$ T ::= \mathsf{Bool}\mid\mathsf{Nat}. $$

Typovací úsudok vyjadruje, že term $t$ má typ $T$:

$$ \boxed{\vdash t:T} $$

NBL nemá premenné, takže úsudok nevyžaduje kontext. Zápis $\vdash t:T$ zodpovedá formalizácii <{ |-- t of T }>; nejde o súčasť syntaxe termu ani o príkaz Check hostiteľského systému Rocq.

Typovacie pravidlá:

$$ \frac{}{\vdash\mathsf{true}:\mathsf{Bool}}\,{\scriptstyle(\mathrm{t\_true})} $$ $$ \frac{}{\vdash\mathsf{false}:\mathsf{Bool}}\,{\scriptstyle(\mathrm{t\_false})} $$ $$ \frac{\vdash t_1:\mathsf{Bool}\qquad\vdash t_2:T\qquad\vdash t_3:T}{\vdash\mathsf{if}\ t_1\ \mathsf{then}\ t_2\ \mathsf{else}\ t_3:T}\,{\scriptstyle(\mathrm{t\_if})} $$ $$ \frac{}{\vdash 0:\mathsf{Nat}}\,{\scriptstyle(\mathrm{t\_0})} $$ $$ \frac{\vdash t_1:\mathsf{Nat}}{\vdash\mathsf{succ}\ t_1:\mathsf{Nat}}\,{\scriptstyle(\mathrm{t\_succ})} $$ $$ \frac{\vdash t_1:\mathsf{Nat}}{\vdash\mathsf{pred}\ t_1:\mathsf{Nat}}\,{\scriptstyle(\mathrm{t\_pred})} $$ $$ \frac{\vdash t_1:\mathsf{Nat}}{\vdash\mathsf{iszero}\ t_1:\mathsf{Bool}}\,{\scriptstyle(\mathrm{t\_iszero})} $$

Definícia v Rocq:

Inductive ty : Type :=
  | Bool : ty
  | Nat : ty.

Declare Custom Entry ty.
Notation "'Nat'" := Nat (in custom ty).
Notation "'Bool'" := Bool (in custom ty).
Notation "x" := x (in custom ty, x global).

Reserved Notation "<{ '|--' t 'of' T }>"
            (at level 0, t custom tm, T custom ty).

Inductive typed : nbl -> ty -> Prop :=
  | t_true :
       <{ |-- true of Bool }>
  | t_false :
       <{ |-- false of Bool }>
  | t_if : forall t1 t2 t3 T,
       <{ |-- t1 of Bool }> ->
       <{ |-- t2 of T }> ->
       <{ |-- t3 of T }> ->
       <{ |-- if t1 then t2 else t3 of T }>
  | t_0 :
       <{ |-- 0 of Nat }>
  | t_succ : forall t1,
       <{ |-- t1 of Nat }> ->
       <{ |-- succ t1 of Nat }>
  | t_pred : forall t1,
       <{ |-- t1 of Nat }> ->
       <{ |-- pred t1 of Nat }>
  | t_iszero : forall t1,
       <{ |-- t1 of Nat }> ->
       <{ |-- iszero t1 of Bool }>

where "<{ '|--' t 'of' T }>" := (typed t T).
#[local] Hint Constructors typed : core.

Príklad: Typovanie a nemožné typovanie

Booleovská konštanta true má typ Bool.

$$ \vdash\mathsf{true}:\mathsf{Bool}. $$

Formalizácia a dôkaz v Rocq:

Theorem ex3: <{ |-- true of Bool }>.
Proof.
    apply t_true.
Qed.

Podmienený výraz s vnoreným testom má typ Bool.

$$ \vdash \mathsf{if}\ \mathsf{true}\ \mathsf{then}\;(\mathsf{if}\ \mathsf{iszero}\ 0\ \mathsf{then}\ \mathsf{true}\ \mathsf{else}\ \mathsf{false})\ \mathsf{else}\ \mathsf{true}:\mathsf{Bool}. $$

Formalizácia a dôkaz v Rocq:

Theorem ex4:
<{|-- if true
        then (if iszero 0 then true else false )
        else true of Bool }>.
Proof.
    apply t_if.
        - apply t_true.
        - apply t_if.
            + apply t_iszero. apply t_0.
            + apply t_true.
            + apply t_false.
        - apply t_true.
Qed.

Podmienený výraz s vnoreným testom má typ Bool.

$$ \vdash \mathsf{if}\ \mathsf{true}\ \mathsf{then}\;(\mathsf{if}\ \mathsf{iszero}\ 0\ \mathsf{then}\ \mathsf{true}\ \mathsf{else}\ \mathsf{false})\ \mathsf{else}\ \mathsf{true}:\mathsf{Bool}. $$

Formalizácia a dôkaz v Rocq:

Theorem ex4_eauto:
<{|-- if true
        then (if iszero 0 then true else false )
        else true of Bool }>.
Proof.
    eauto.
Qed.

Výrazu s vetvami 0 a true nemožno priradiť typ Bool.

$$ \neg\bigl(\vdash\mathsf{if}\ \mathsf{false}\ \mathsf{then}\ 0\ \mathsf{else}\ \mathsf{true}:\mathsf{Bool}\bigr). $$

Formalizácia a dôkaz v Rocq:

Theorem ex5 :
  ~ <{ |-- if false then 0 else true of Bool }>.
Proof.
    unfold not.
    intros.
    inversion H.
    (* H5 : <{ |-- 0 of Bool }> *)

    inversion H5.
Qed.

Základné vlastnosti typového systému

Pre tento typový systém NBL dokážeme tri vlastnosti. Jednoznačnosť typu nie je všeobecnou požiadavkou typovej bezpečnosti: napríklad systémy s podtypovaním môžu termu priradiť viac typov. Typovú bezpečnosť tu odvodíme z progresu a zachovania typu.

1. Jednoznačnosť typu (Uniqueness of Types)

Formulácia: Ak $\vdash t:T_1$ a $\vdash t:T_2$, potom $T_1=T_2$. NBL nemá premenné, preto sú všetky jeho termy uzavreté a typový kontext Γ nepotrebujeme.

  • Každý term má najviac jeden typ; netypovateľný term nemá žiadny. Jednoznačnosť typu sama nehovorí nič o deterministickosti vyhodnocovania.

Význam:

  • Zjednodušuje dôkazy o správnosti.
  • Zaručuje, že kompilátor alebo typová kontrola sa „nerozhoduje" medzi rôznymi typmi toho istého výrazu.

2. Progres (Progress Theorem)

Ak ⊢ t : T, potom buď:

  • t je už hodnota (value), alebo
  • existuje t', takže t --> t'.

Správne typovaný term je hodnotou alebo môže vykonať ďalší krok. Aby sme vylúčili zaseknutie aj po viacerých krokoch, potrebujeme navyše zachovanie typu.

Význam:

  • Dobre typované programy nespadnú na runtime chybe typu.
  • Typový systém zachytáva chyby ešte pred spustením programu.

3. Stabilita (zachovanie) typu (Preservation Theorem)

Ak $\vdash t:T$ a $t\to t'$, potom $\vdash t':T$.

  • Typ sa počas vykonávania programu nezmení.

Význam:

  • Každý krok výpočtu zachováva typovú korektnosť.
  • Typový systém a sémantika sú v súlade.

Príklad:

  • Ak t má typ Nat a t --> t', potom aj t' má typ Nat.

Spolu tieto dve vety – Progress a Preservation – tvoria dôkaz o typovej korektnosti (bezpečnosti jazyka) (z ang. Type Soundness):

"Dobre typované programy sa nikdy nezaseknú a počas behu si zachovávajú správny typ."

Veta o jednoznačnosti typu

Teoretické znenie: Ak výraz t má typ T1 aj typ T2, potom tieto typy musia byť rovnaké.

Formálne: $$ \forall t,T_1,T_2.\quad(\vdash t:T_1)\land(\vdash t:T_2)\implies T_1=T_2. $$

Dôkaz prebieha štrukturálnou indukciou nad tvarom termu t.

Theorem type_uniqueness Ak má term dva typy, tieto typy sa rovnajú.

$$ \forall t,T_1,T_2.\quad(\vdash t:T_1)\land(\vdash t:T_2)\implies T_1=T_2. $$

Formalizácia a dôkaz v Rocq:

Theorem type_uniqueness: forall t T1 T2,
        <{ |-- t of T1 }> /\ <{ |-- t of T2 }> -> T1 = T2.
Proof.
  intros.
  destruct H as [HT1 HT2].  (* rozdelíme konjunkciu na dva predpoklady *)
  (* HT1 : <{ |-- t of T1 }>
     HT2 : <{ |-- t of T2 }>
     ============================
     T1 = T2 *)

  induction t.
  (* dôkaz indukciou podľa štruktúry termu t *)

  - (* prípad: t = true *)
    inversion HT1. inversion HT2. reflexivity.
    (** využitím vety o inverzii odvodíme,
        že ak  <{ |-- true of T }>, tak T je Bool*)

  - (* prípad: t = false *)
    inversion HT1. inversion HT2. reflexivity.
    (** rovnaké zdôvodnenie ako vyššie *)

  - (* prípad: t = 0 *)
    inversion HT1. inversion HT2. reflexivity.
    (** nula má vždy typ [Nat]. *)

  - (* prípad: t = iszero t1 *)
    inversion HT1. inversion HT2. reflexivity.
    (** test [iszero] má vždy výsledok typu [Bool]. *)

  - (* prípad: t = pred t1 *)
    inversion HT1. inversion HT2. reflexivity.
    (** pravidlo t_pred určí výsledný typ Nat. *)

  - (* prípad: t = succ t1 *)
    inversion HT1. inversion HT2. reflexivity.
    (** pravidlo t_succ určí výsledný typ Nat. *)

  - (* prípad: t = if t1 then t2 else t3 *)
    inversion HT1; subst.
    inversion HT2; subst.
    apply IHt2; assumption.
Qed.

Kratší dôkaz Ak má term dva typy, tieto typy sa rovnajú.

$$ \forall t,T_1,T_2.\quad(\vdash t:T_1)\land(\vdash t:T_2)\implies T_1=T_2. $$

Formalizácia a dôkaz v Rocq:

Theorem type_uniqueness': forall t T1 T2,
        <{ |-- t of T1 }> /\ <{ |-- t of T2 }> -> T1 = T2.
Proof.
  intros.
  destruct H as [HT1 HT2].
  induction t; inversion HT1; inversion HT2; try reflexivity.
  (** Vyriešených prvých 6 prípadov, ostal prípad pre IF *)

  - inversion HT1; subst.
    inversion HT2; subst.
    apply IHt2.
    assumption.
    assumption.
Qed.

Vety o kanonických hodnotách

Tieto vety sú kľúčovým medzičlánkom medzi typovým systémom a semantikou hodnôt.

Ich úlohou je formálne zachytiť nasledujúcu intuitívnu myšlienku:

Ak je výraz dobre typovaný a je zároveň hodnotou, potom musí mať určitý „kanonický" (štandardný) tvar zodpovedajúci jeho typu.

Inými slovami:

  • Hodnota typu Bool musí byť buď true alebo false.
  • Hodnota typu Nat musí byť 0 alebo succ n, kde n je číselná hodnota.

Lemma bool_canonical Hodnota typu Bool je booleovskou hodnotou, teda true alebo false.

$$ \forall t.\quad(\vdash t:\mathsf{Bool})\land\operatorname{value}(t)\implies\operatorname{bval}(t). $$

Formalizácia a dôkaz v Rocq:

Lemma bool_canonical : forall t,
      <{|-- t of Bool}> /\ value t -> bval t.
Proof.
  intros.
  unfold value in H.
  (* rozbalíme definíciu hodnoty *)

  destruct H as [Ht Hbv].
  (* rozdelíme konjunkciu typovej relácie
    a výroku, že t je hodnota *)

  destruct Hbv as [Hnv | Hbv].
  (* hodnota môže byť nval alebo bval *)

  - (* ============================
       Prípad: t je číselná hodnota

       Ht : <{ |-- t of Bool }>
       Hnv : nval t
       ============================
       bval t *)

    inversion Hnv. subst.
    + (* Hnv : nval <{ 0 }>
         Ht : <{ |-- 0 of Bool }>
         ============================
         bval <{ 0 }> *)

      inversion Ht.
      (* t = 0, ale 0 má typ Nat, nie Bool *)

    + (* Druhý konštruktor nval dá tvar succ u a dôkaz nval u.
         Rovnosť indexov po subst určí t = succ u.
         Názvy pomocných hypotéz môže Rocq generovať odlišne.
         Relevantný cieľ po dosadení: bval <{ succ u }>,
         pričom typovací predpoklad požaduje typ Bool. *)

      subst. inversion Ht.
      (* t = succ t má typ Nat, nie Bool *)

  - (* ============================
       Prípad: t je booleovská hodnota

       Ht : <{ |-- t of Bool }>
       Hbv : bval t
       ============================
       bval t *)

    apply Hbv.
Qed.

Lemma nat_canonical Analogický postup ako v predchadzajúcom prípade. Hodnota typu Nat je numerickou hodnotou.

$$ \forall t.\quad(\vdash t:\mathsf{Nat})\land\operatorname{value}(t)\implies\operatorname{nval}(t). $$

Formalizácia a dôkaz v Rocq:

Lemma nat_canonical : forall t,
      <{|-- t of Nat}> /\ value t -> nval t.
Proof.
  intros.
  destruct H as [Ha Hb].
  unfold value in Hb.
  (* Ha : <{ |-- t of Nat }>
     Hb : nval t \/ bval t
     ============================
     nval t *)

  destruct Hb as [Hnv | Hbv].
  - apply Hnv.
  - inversion Hbv. subst.
    inversion Ha. subst.
    inversion Ha.
Qed.

Dôkaz bezpečnosti jazyka NBL

VETA O PROGRESE (Progress Theorem)

Formulácia: Ak ⊢ t : T (t. j. výraz t je dobre typovaný), potom buď:

  • t je hodnota (value), alebo
  • existuje t', také že t --> t' (t je možné redukovať).

Význam: Progres poskytuje hodnotu alebo ďalší krok pre aktuálny správne typovaný term. Zachovanie typu umožní túto vlastnosť použiť znovu na výsledok každého kroku.

Každý správne typovaný term je hodnotou alebo môže vykonať ďalší krok.

$$ \forall t,T.\quad(\vdash t:T)\implies\bigl(\operatorname{value}(t)\lor\exists t'.\ t\to t'\bigr). $$

Formalizácia a dôkaz v Rocq:

Theorem progress: forall t T,
        <{ |-- t of T}> -> (value t) \/ exists t', (t --> t').
Proof.
  intros.
  (** Dôkaz indukciou nad typovou reláciou *)
  induction H.

  (* true *)
  - left. unfold value. right. apply bvtrue.

  (* false *)
  - left. unfold value. right. apply bvfalse.

  (* if t1 then t2 else t3 *)
  - right. destruct IHtyped1.
    + assert (Hb : bval t1).
      { apply (bool_canonical t1). split; assumption. }
      inversion Hb. subst.
      * exists t2. apply st_iftrue.
      * exists t3. apply st_iffalse.
    + destruct H2 as [t1' Hstep].
      exists (<{if t1' then t2 else t3}>).
      apply st_if. assumption.

  (* 0 *)
  - left. unfold value. left. apply nv0.

  (* succ t1 *)
  - destruct IHtyped.
    + left. assert (nval t1) as Hn.
      { apply (nat_canonical t1).
        split. apply H. apply H0. }
      unfold value. left. apply nvscc. apply Hn.
    + right. destruct H0 as [t' Hstep].
      exists (scc t').
      apply st_succ. apply Hstep.

  (* pred t1 *)
  - destruct IHtyped as [Hv | [t' Hstep]].
    + destruct (nat_canonical t1).
      split. assumption. assumption.
      right. exists zro. apply st_pred0.
      right. exists t. apply st_predsucc. assumption.
    + right. exists (prede t'). apply st_pred. assumption.

  (* iszero t1 *)
  - destruct IHtyped as [Hv | [t' Hstep]].
    + destruct (nat_canonical t1). split.
      * assumption.
      * assumption.
      * right. exists tru. apply st_iszero0.
      * right. exists fls. apply st_iszeronv. assumption.
    + right. exists (iszro t'). apply st_iszero. assumption.
Qed.

VETA O STABILITE (ZACHOVANÍ) TYPU (Type Preservation)

Formulácia: Ak výraz t má typ T a vykoná jeden krok redukcie na t', potom aj t' má typ T: $$ \forall t,t',T.\quad(\vdash t:T)\land(t\to t')\implies(\vdash t':T). $$

Typový systém je konzistentný so sémantikou: každý krok redukcie zachováva typ. Správne typovaný program nikdy „nestratí" svoj typ počas vykonávania.

Túto vetu je možné dokázať dvomi spôsobmi:

  1. Indukciou na typovej relácii.
  2. Indukciou na vyhodnocovacej relácii.

Indukcia na typovej relácii:

Jeden krok vyhodnotenia zachováva typ termu.

$$ \forall t,t',T.\quad(\vdash t:T)\land(t\to t')\implies(\vdash t':T). $$

Formalizácia a dôkaz v Rocq:

Theorem preservation: forall t t' T,
        <{|-- t of T}> /\ (t-->t') ->  <{|-- t' of T}>.
Proof.
  intros.
  destruct H.
  (** rozdelenie konjunkcie na typovací a vyhodnocovací úsudok *)
  (* t' zostáva všeobecné: podterm sa redukuje na iný term než celý výraz. *)

  generalize dependent t'.
  induction H; intros t' Hstep;
  inversion Hstep; subst; try assumption.

  (* try assumption uzavrelo if-true, if-false aj pred-0.
     Zostáva redukcia podmienky if. *)
  - apply t_if.
    + apply IHtyped1. assumption.
    + assumption.
    + assumption.

  (* succ *)
  - apply t_succ. apply IHtyped in H1. assumption.

  (* pred (succ v): z typovania succ v získame typ v. *)
  - inversion H. assumption.

  (* pred *)
  - apply t_pred. apply IHtyped. assumption.

  (* iszero 0 *)
  - apply t_true.

  (* iszero (succ v) *)
  - apply t_false.

  (* iszero *)
  - apply t_iszero. apply IHtyped. apply H1.
Qed.

Indukcia na vyhodnocovacej relácii:

Teraz indukcia sleduje všetkých desať vyhodnocovacích pravidiel; inverzia typovania určuje typy podtermov. Typ T musí v indukčnom predpoklade zostať všeobecný: podmienka má typ Bool, aj keď výsledok celého výrazu má typ Nat. Jeden krok vyhodnotenia zachováva typ termu.

$$ \forall t,t',T.\quad(\vdash t:T)\land(t\to t')\implies(\vdash t':T). $$

Formalizácia a dôkaz v Rocq:

Theorem preservation': forall t t' T,
        <{|-- t of T}> /\ (t-->t') ->  <{|-- t' of T}>.
Proof.
intros.
destruct H as [Ht Hr].
generalize dependent T.
induction Hr.
- (* if true *)
  intros. inversion Ht. subst. assumption.
- (* if false *)
  intros. inversion Ht. subst. assumption.
- (* redukcia podmienky if *)
  intros. inversion Ht. subst. apply t_if.
  + apply IHHr in H2. assumption.
  + assumption.
  + assumption.
- (* redukcia argumentu succ *)
  intros. inversion Ht. subst.
  apply IHHr in H0. apply t_succ. assumption.
- (* pred 0 *)
  intros. inversion Ht. subst. assumption.
- (* pred (succ v) *)
  intros. inversion Ht. subst.
  inversion H1. subst. assumption.
- (* redukcia argumentu pred *)
  intros. inversion Ht. subst.
  apply IHHr in H0. apply t_pred. assumption.
- (* iszero 0 *)
  intros. inversion Ht. apply t_true.
- (* iszero (succ v) *)
  intros. inversion Ht. apply t_false.
- (* redukcia argumentu iszero *)
  intros. inversion Ht. subst.
  apply IHHr in H0. apply t_iszero. assumption.
Qed.

Bezpečnosť po viacerých krokoch

Najprv rozšírime zachovanie typu na celú konečnú cestu. Dôkaz prebieha indukciou podľa odvodenia multistep.

Ľubovoľný konečný počet krokov vyhodnotenia zachováva typ.

$$ \forall t,t',T.\quad(\vdash t:T)\land(t\to^{*}t')\implies(\vdash t':T). $$

Formalizácia a dôkaz v Rocq:

Lemma preservation_multistep : forall t t' T,
  <{ |-- t of T }> -> t -->* t' -> <{ |-- t' of T }>.
Proof.
  intros t t' T Htyped Hmulti.
  induction Hmulti as [t | t1 t2 t3 Hstep Hrest IH].
  - (* Nula krokov: typ sa nemení. *)
    exact Htyped.
  - (* Prvý krok zachová typ; na zvyšok cesty použijeme indukčný predpoklad. *)
    apply IH.
    apply (preservation t1 t2 T).
    split; assumption.
Qed.

Ak je term dosiahnutý zo správne typovaného termu v normálnej forme, musí byť hodnotou. Zachovanie typu mu poskytne typ a progres vylúči zaseknutie: možnosť ďalšieho kroku je v rozpore s normálnou formou.

Normálna forma dosiahnutá zo správne typovaného termu je hodnotou.

$$ \forall t,t',T.\quad(\vdash t:T)\land(t\to^{*}t')\land\operatorname{normal\_form}(t')\implies\operatorname{value}(t'). $$

Formalizácia a dôkaz v Rocq:

Theorem type_safety : forall t t' T,
  <{ |-- t of T }> -> t -->* t' -> normal_form t' -> value t'.
Proof.
  intros t t' T Htyped Hmulti Hnormal.
  assert (Htyped' : <{ |-- t' of T }>).
  { apply (preservation_multistep t t' T); assumption. }
  destruct (progress t' T Htyped') as [Hv | [t'' Hstep]].
  - exact Hv.
  - exfalso.
    apply Hnormal.
    exists t''. exact Hstep.
Qed.

Veta nehovorí, že vyhodnocovanie vždy dosiahne normálnu formu. Ukončenie je samostatná vlastnosť a z progresu ani zachovania typu samotných nevyplýva.

Ekvivalencia malých a veľkých krokov – úloha

Term sa podľa sémantiky veľkých krokov vyhodnotí na $v$ práve vtedy, keď podľa sémantiky malých krokov dosiahne $v$ po konečnom počte krokov a $v$ je hodnota:

$$ \forall t,v.\quad t\Downarrow v\iff\bigl(t\to^{*}v\land\operatorname{value}(v)\bigr). $$

Tvrdenie platí pre všetky termy NBL, nevyžaduje predpoklad správnej typovanosti. Podmienku hodnoty nemožno vypustiť: reflexívna cesta existuje aj pre term, ktorý ešte nie je výsledkom.

Znenie v Rocq na samostatné dokázanie:

Theorem bigstep_smallstep_equiv :
  forall t v,
    (t ==> v) <-> (t -->* v /\ value v).
Proof.
  (* Úloha: doplňte oba smery dôkazu podľa slovného náčrtu. *)
Abort.

Abort tu ukončí rozpracovaný dôkaz bez uloženia vety. Pri riešení úlohy doplňte dôkaz a ukončite ho príkazom Qed. Nejde o hotový dôkaz ani o predpoklad, ktorý by mohli využívať ďalšie vety. V zadaní s booleovským testom hodnôt sa namiesto value v používa isval v = true; pri prepájaní oboch formalizácií treba zohľadniť zhodu tohto testu s predikátom hodnôt.

Slovný náčrt dôkazu:

  1. Z veľkých krokov na malé kroky. Postupujte indukciou podľa odvodenia $t\Downarrow v$. Základné pravidlá pre true, false a nulu dávajú nulovú cestu. V ostatných prípadoch použite indukčné predpoklady na podvýpočty. Pomocnými lemami preneste viackrokové cesty do argumentov succ, pred, iszero a do podmienky if. Pri podmienke potom vykonajte príslušný krok výberu vetvy a pokračujte cestou pre vybranú vetvu; pri číselných operáciách podľa potreby použite pravidlo výpočtu nad numerickou hodnotou. Cesty spojte. Tou istou indukciou overte, že výsledok každého veľkého kroku je hodnota.
  2. Z malých krokov na veľké kroky. Najprv dokážte pomocné tvrdenie: ak $t\to t'$ a $t'\Downarrow v$, potom aj $t\Downarrow v$. Vhodná je indukcia podľa odvodenia jedného malého kroku a inverzia príslušného veľkého kroku. Pripravte si tiež lemu, že každá hodnota sa vyhodnotí sama na seba; pri numerických hodnotách použite indukciu podľa dôkazu nval. Potom postupujte indukciou podľa cesty $t\to^{*}v$. Nulovú cestu uzavriete pomocou predpokladu, že $v$ je hodnota, a uvedenej lemy. Pri neprázdnej ceste získajte z indukčného predpokladu veľký krok pre jej zvyšok a pomocným tvrdením pridajte prvý malý krok spätne.

Úplný formálny dôkaz oboch smerov aj potrebných pomocných lem je úlohou v študentskom zadaní. Ekvivalencia porovnáva úspešné vyhodnotenie na hodnotu; sama nie je dôkazom, že každý term sa na hodnotu vyhodnotí.

End nbl.

Zhrnutie

Malé kroky opisujú jednotlivé prechody a veľké kroky úspešné vyhodnotenie na hodnotu. Ich ekvivalenciu sme sformulovali ako úlohu so slovným náčrtom dôkazu. Progres a zachovanie typu vylučujú zaseknutie správne typovaných termov.

© Copyright 2026 KPI FEI TUKE