実例：型付きミニ言語を作る

文法・型付け規則・評価器を書いて文字列のプログラムを実行し、型安全性を証明します。

19a.1 作る言語と、書くもの

この章では、数・真偽値・+・==・if だけを持つ、小さな型付きの式言語を作ります。

1 + 2 + 3                        -- 6 : Nat
if 1 + 1 == 2 then 10 else 20    -- 10 : Nat
1 + true                         -- 型エラー

インタプリタの部品のうち、字句解析・構文解析・型検査器は、Tauto のマクロが作ります。人が書くのは次の三つです。

書くもの	使う機能	できるもの	節
文法	`inductive_syntax!`	構文解析器 `tl::parse` と、証明から見える構文木	19a.2
型付け規則	`inductive` の関係と `@mode!`	型検査器 `check`	19a.3
型安全性の証明	`theorem`	「型が付けば実行は失敗しない」ことの保証	19a.7

残りの評価器（19a.4）と、構文木を核の言語に変換する関数（19a.5）は、普通の関数です。全体の流れは次のとおりです。

文字列 --tl::parse--> tl::Expr --to_i--> tl::Expr::I --lower_expr--> Term --check_ty--> Option(Ty)
                                                                     Term --eval------> Option(Val)

コードは第 12 章の tote として src/ に置き、ファイルごとに import します。同じ構成の完全な例が、リポジトリの examples/typed-lang/ にあります（一行ずつ式を読む REPL 付き）。

19a.2 文法を書く

文法は inductive_syntax! に書きます。17a 章の syntax! と同じ文法の書き方です。

src/syntax.taut

import std::Text { Text }

// 文法を一つ書くと、読む関数 `tl::parse` と、証明から見える木 `tl::Expr::I` が生える。
inductive_syntax!(tl, ```par
%start Expr
%title "typed-lang"
%%
Expr: IfExpr | Cmp;
IfExpr: KwIf Expr KwThen Expr KwElse Expr;
Cmp: Sum [ EqEq Sum ];
Sum: Atom { Plus Atom };
Atom: Num | KwTrue | KwFalse | Paren;
Paren: LParen Expr RParen;
Num: /[0-9]+/;
Plus: '+';
EqEq: '==';
KwIf: 'if';
KwThen: 'then';
KwElse: 'else';
KwTrue: 'true';
KwFalse: 'false';
LParen: '(';
RParen: ')';
```) =>
  enum Atom, struct Cmp, struct Cmp_Opt1, enum Expr, struct IfExpr, struct Paren, struct Sum,
  struct Sum_Rep1, fn parse, inductive Atom::I, inductive Cmp::I, inductive Cmp_Opt1::I,
  inductive Expr::I, inductive IfExpr::I, inductive Paren::I, inductive Sum::I,
  inductive Sum_Rep1::I, fn Atom::to_i, fn Cmp::to_i, fn Cmp_Opt1::to_i, fn Expr::to_i,
  fn IfExpr::to_i, fn Paren::to_i, fn Sum::to_i, fn Sum_Rep1::to_i, fn Cmp_Opt1_opt::to_i,
  fn Sum_Rep1_list::to_i

✓ 検査を通過

%% の下が文法の規則です。'+' のような文字列と /[0-9]+/ のような正規表現が字句になり、空白は読み飛ばされます。Sum: Atom { Plus Atom }; の { … } は 0 回以上の繰り返し、Cmp: Sum [ EqEq Sum ]; の [ … ] は省略できる部分です。+ の両辺を Atom にしているので、1 + 1 == 2 は (1 + 1) == 2 と読まれます。

この宣言から、二組の型と関数ができます。

tl::Expr、tl::Sum など：tl::parse が文字列から作る構文木です。文法に合わない文字列は Err になり、何が期待されていたかを報告します。
tl::Expr::I、tl::Sum::I など：同じ木の inductive 版です。カーネルが読める型なので、証明の中で使えます。tl::Expr::to_i が前者を後者に変えます。

=> … は、作られる宣言の完全な一覧です。足りない名前や余った名前があると、エラーになります。文法を変えたあとは、tauto syntax gen で構文解析の表を作り直します。

19a.3 型付け規則を書くと、検査器ができる

構文木は文法の形をしていて、Sum の繰り返しや括弧を持っています。型検査と評価には、もっと小さな核の言語 Term を使います。

src/core.taut

import std::Mode { mode }

// 型付き式言語の核。木ではなく、型検査と評価が読む形。

pub(open) inductive Ty: Type {
  TNat: Ty
  TBool: Ty
}

pub(open) inductive Term: Type {
  TmNum(n: Nat): Term
  TmBool(b: Bool): Term
  TmAdd(a: Term, b: Term): Term
  TmEq(a: Term, b: Term): Term
  TmIf(c: Term, t: Term, e: Term): Term
}

pub(open) inductive TyDecision(a: Ty, b: Ty): Type {
  TySame(e: a = b): TyDecision(a, b)
  TyDifferent(refute: (a = b) -> False): TyDecision(a, b)
}

pub fn ty_dec(a: Ty, b: Ty): TyDecision(a, b) {
  match a: TyDecision(a, b) {
    TNat => match b: TyDecision(TNat, b) {
      TNat => TySame(Refl)
      TBool => TyDifferent(e => match e: False {})
    }
    TBool => match b: TyDecision(TBool, b) {
      TNat => TyDifferent(e => match e: False {})
      TBool => TySame(Refl)
    }
  }
}

// 人間が読む仕様はこの関係だけ。検査器は、この規則から `mode!` が作る。
@mode!(`check(rec term, out ty) -> Check { Accepted | Rejected } eq Ty: ty_dec { TySame | TyDifferent }`) => inductive Check, fn check
pub(open) inductive HasTy: (Term, Ty) -> Prop {
  TyNum<n: Nat>: HasTy(TmNum(n), TNat)
  TyBool<b: Bool>: HasTy(TmBool(b), TBool)
  TyAdd<a: Term, b: Term>(ha: HasTy(a, TNat), hb: HasTy(b, TNat)): HasTy(TmAdd(a, b), TNat)
  TyEq<a: Term, b: Term>(ha: HasTy(a, TNat), hb: HasTy(b, TNat)): HasTy(TmEq(a, b), TBool)
  TyIf<c: Term, t: Term, e: Term, ty: Ty>(
    hc: HasTy(c, TBool),
    ht: HasTy(t, ty),
    he: HasTy(e, ty)
  ): HasTy(TmIf(c, t, e), ty)
}

実行結果

✓ def ty_dec : ∀ a: Ty. ∀ b: Ty. TyDecision(a, b)

Ty が型、Term が核の言語の式です。HasTy(t, ty) は「式 t は型 ty を持つ」という関係で、構成子の一つ一つが型付け規則です。たとえば TyAdd は、「a と b が Nat なら、TmAdd(a, b) も Nat」と読みます。TyIf は、条件が Bool で、二つの枝が同じ型 ty を持つことを求めます。

@mode! は、この規則から型検査器 check を作ります。

check(rec term, out ty) は、HasTy の一つ目の引数（式）を入力として再帰し、二つ目（型）を出力として求める、という指定です。
TyIf の二つの枝の型が同じかどうかは、eq Ty: ty_dec で比べます。ty_dec は、等しいことの証明（TySame）か、等しくないことの証明（TyDifferent）を返します。
check(t) の答え Check(t) は、受理（Accepted）なら型と HasTy の導出と型の一意性を、拒否（Rejected）なら「どんな型でも型付けできない」ことの反証を持ちます。

検査器を手で書いて、あとから規則と一致することを証明するのではありません。規則から、正しさの証拠付きの検査器が作られます。

19a.4 評価器

値は Val で表します。評価器 eval は別のファイル src/eval.taut に置きます。Term の形に従った再帰です。

src/eval.taut

import "core.taut" { Term }
import std::Base { Nat }

pub(open) inductive Val: Type {
  VNat(n: Nat): Val
  VBool(b: Bool): Val
}

// 評価器。型の合わない演算は `None`（実行時の型エラー）。
pub fn add_val(x: Option(Val), y: Option(Val)): Option(Val) {
  match x: Option(Val) {
    None => None
    Some(vx) => match vx: Option(Val) {
      VBool(xb) => None
      VNat(nx) => match y: Option(Val) {
        None => None
        Some(vy) => match vy: Option(Val) {
          VBool(yb) => None
          VNat(ny) => Some(VNat(Nat::add(nx, ny)))
        }
      }
    }
  }
}

pub fn eq_val(x: Option(Val), y: Option(Val)): Option(Val) {
  match x: Option(Val) {
    None => None
    Some(vx) => match vx: Option(Val) {
      VBool(xb) => None
      VNat(nx) => match y: Option(Val) {
        None => None
        Some(vy) => match vy: Option(Val) {
          VBool(yb) => None
          VNat(ny) => Some(VBool(Nat::eq(nx, ny)))
        }
      }
    }
  }
}

pub fn if_val(c: Option(Val), t: Option(Val), e: Option(Val)): Option(Val) {
  match c: Option(Val) {
    None => None
    Some(vc) => match vc: Option(Val) {
      VNat(n) => None
      VBool(b) => match b: Option(Val) {
        true => t
        false => e
      }
    }
  }
}

pub fn eval(t: Term): Option(Val) {
  match t: Option(Val) {
    TmNum(n) => Some(VNat(n))
    TmBool(b) => Some(VBool(b))
    TmAdd(a, b) => add_val(eval(a), eval(b))
    TmEq(a, b) => eq_val(eval(a), eval(b))
    TmIf(c, t1, e) => if_val(eval(c), eval(t1), eval(e))
  }
}

実行結果

✓ def add_val : (Option(Val)) -> (Option(Val)) -> Option(Val)
✓ def eq_val : (Option(Val)) -> (Option(Val)) -> Option(Val)
✓ def if_val : (Option(Val)) -> (Option(Val)) -> (Option(Val)) -> Option(Val)
✓ def eval : (Term) -> Option(Val)

評価器は型を見ません。TmAdd(TmNum(1), TmBool(true)) のような式では、add_val が None（実行時の型エラー）を返します。eval は構造的な再帰なので、Div のない全域な関数です。

19a.5 構文木を核の言語にする

lower_expr は、inductive 版の構文木 tl::Expr::I を Term に変換します。

src/lower.taut

import "core.taut" { Term }
import "syntax.taut" { tl }
import std::Base { Nat }
import std::Text { Text }

// 木（`tl::Expr::I`）を核の `Term` にする。ここは全域な普通の関数で、型は見ない。

pub fn num_of(t: Text): Nat {
  digits(Text::bytes(t), 0)
}

pub fn digits(bs: List(Nat), acc: Nat): Nat {
  match bs: Nat {
    Nil => acc
    Cons(b, rest) => digits(rest, Nat::add(Nat::mul(acc, 10), Nat::sub(b, 48)))
  }
}

mutual {
  pub fn lower_expr(e: tl::Expr::I): Term {
    match e: Term {
      IfExpr_I(i) => lower_if(i)
      Cmp_I(c) => lower_cmp(c)
    }
  }
  pub fn lower_if(i: tl::IfExpr::I): Term {
    match i: Term {
      Mk(k1, c, k2, t, k3, e) => TmIf(lower_expr(c), lower_expr(t), lower_expr(e))
    }
  }
  pub fn lower_cmp(c: tl::Cmp::I): Term {
    match c: Term {
      Mk(sum, opt) => lower_cmp_opt(lower_sum(sum), opt)
    }
  }
  pub fn lower_cmp_opt(lhs: Term, o: Option(tl::Cmp_Opt1::I)): Term {
    match o: Term {
      None => lhs
      Some(r) => lower_cmp_rhs(lhs, r)
    }
  }
  pub fn lower_cmp_rhs(lhs: Term, r: tl::Cmp_Opt1::I): Term {
    match r: Term {
      Mk(op, rhs) => TmEq(lhs, lower_sum(rhs))
    }
  }
  pub fn lower_sum(s: tl::Sum::I): Term {
    match s: Term {
      Mk(atom, rep) => lower_rep(lower_atom(atom), rep)
    }
  }
  pub fn lower_rep(acc: Term, rep: List(tl::Sum_Rep1::I)): Term {
    match rep: Term {
      Nil => acc
      Cons(r, more) => lower_rep(lower_rep_step(acc, r), more)
    }
  }
  pub fn lower_rep_step(acc: Term, r: tl::Sum_Rep1::I): Term {
    match r: Term {
      Mk(op, atom) => TmAdd(acc, lower_atom(atom))
    }
  }
  pub fn lower_atom(a: tl::Atom::I): Term {
    match a: Term {
      Num_I(t) => TmNum(num_of(t))
      KwTrue_I(t) => TmBool(true)
      KwFalse_I(t) => TmBool(false)
      Paren_I(p) => lower_paren(p)
    }
  }
  pub fn lower_paren(p: tl::Paren::I): Term {
    match p: Term {
      Mk(l, e, r) => lower_expr(e)
    }
  }
}

✓ 検査を通過

✓ def digits : (List(Nat)) -> (Nat) -> Nat
✓ def num_of : (Text) -> Nat
✓ def lower_expr : (tl::Expr::I) -> Term
✓ def lower_if : (tl::IfExpr::I) -> Term
✓ def lower_cmp : (tl::Cmp::I) -> Term
✓ def lower_cmp_opt : (Term) -> (Option(tl::Cmp_Opt1::I)) -> Term
✓ def lower_cmp_rhs : (Term) -> (tl::Cmp_Opt1::I) -> Term
✓ def lower_sum : (tl::Sum::I) -> Term
✓ def lower_rep : (Term) -> (List(tl::Sum_Rep1::I)) -> Term
✓ def lower_rep_step : (Term) -> (tl::Sum_Rep1::I) -> Term
✓ def lower_atom : (tl::Atom::I) -> Term
✓ def lower_paren : (tl::Paren::I) -> Term

tl::Sum::I の繰り返し（Atom { Plus Atom }）は、lower_rep で左から TmAdd に畳み込みます。互いに呼び合う関数は mutual { … } にまとめます。数字の並びは、Text::bytes で読んだバイトから Nat にします。

19a.6 つなげて実行する

check の答えを Option(Ty) にする check_ty と、検査を通ったときだけ評価する run_term を書きます。

src/pipeline.taut

import "core.taut" { Check, Term, Ty, check }
import "eval.taut" { Val, eval }
import "lower.taut" { lower_expr }
import "syntax.taut" { tl }

pub fn decision_ty(t: Term, d: Check(t)): Option(Ty) {
  match d: Option(Ty) {
    Accepted(ty, derivation, unique) => Some(ty)
    Rejected(refute) => None
  }
}

// 型検査器: `mode!` が作った `check` の答えを、型の `Option` にしたもの。
pub fn check_ty(t: Term): Option(Ty) {
  decision_ty(t, check(t))
}

// 検査を通ったものだけを評価する。
pub fn run_if_typed(r: Option(Ty), t: Term): Option(Val) {
  match r: Option(Val) {
    None => None
    Some(ty) => eval(t)
  }
}

pub fn run_term(t: Term): Option(Val) {
  run_if_typed(check_ty(t), t)
}

pub fn run_tree(e: tl::Expr::I): Option(Val) {
  run_term(lower_expr(e))
}

✓ 検査を通過

✓ def decision_ty : ∀ t: Term. (Check(t)) -> Option(Ty)
✓ def check_ty : (Term) -> Option(Ty)
✓ def run_if_typed : (Option(Ty)) -> (Term) -> Option(Val)
✓ def run_term : (Term) -> Option(Val)
✓ def run_tree : (tl::Expr::I) -> Option(Val)

Check(t) は式 t に依存する型です。decision_ty は、受理なら型を取り出し、拒否なら None を返します。

文字列から結果までをつなげて、実行します。

src/main.taut

import "core.taut" { Ty }
import "eval.taut" { Val, eval }
import "lower.taut" { lower_expr }
import "pipeline.taut" { check_ty }
import "syntax.taut" { tl }
import std::prelude::Shared { concat }

fn show_ty(ty: Ty): Text {
  match ty {
    TNat => "Nat"
    TBool => "Bool"
  }
}

fn show_val(v: Option(Val)): Text {
  match v {
    None => "stuck"
    Some(x) => match x {
      VNat(n) => Text::of_nat(n)
      VBool(b) => if b { "true" } else { "false" }
    }
  }
}

fn run_text(src: Text): Text ! {Div} {
  match tl::parse(src) {
    Err(d) => concat("構文エラー: ", d.message)
    Ok(tree) => {
      let t := lower_expr(tl::Expr::to_i(tree))
      match check_ty(t) {
        None => "型エラー"
        Some(ty) => concat(show_val(eval(t)), concat(" : ", show_ty(ty)))
      }
    }
  }
}

perform show("a", run_text("1 + 2 + 3"))
perform show("b", run_text("if 1 + 1 == 2 then 10 else 20"))
perform show("c", run_text("1 + true"))
perform show("d", run_text("if true then 1 else false"))
perform show("e", run_text("1 + * 2"))

実行結果

✓ def show_ty : (Ty) -> Text
・ show_val
・ run_text

a = "6 : Nat"
b = "10 : Nat"
c = "型エラー"
d = "型エラー"
e = "構文エラー: macro.syntax_error: in tl: expected Num or KwTrue or KwFalse or LParen, found Error"

a = "6 : Nat"
b = "10 : Nat"
c = "型エラー"
d = "型エラー"
e = "構文エラー: macro.syntax_error: in tl: expected Num or KwTrue or KwFalse or LParen, found Error"

1 + true と if true then 1 else false は、型検査器が止めるので、評価器には渡りません。1 + * 2 は、文法から作られた構文解析器が、期待した字句の一覧と一緒に報告します。

19a.7 型安全性を証明する

型検査を通った式は、評価しても実行時の型エラーにならない、という性質を証明します。まず、評価の結果が型に合うことを表す関係を定義します。

src/safety.taut

import "core.taut" { HasTy, Term, Ty }
import "eval.taut" { Val, add_val, eq_val, eval, if_val }

// 値が型を持つ、という関係。
pub(open) inductive ValHas: (Val, Ty) -> Prop {
  HNat<n: Nat>: ValHas(VNat(n), TNat)
  HBool<b: Bool>: ValHas(VBool(b), TBool)
}

// 評価が成功して、約束した型の値を返した、という証拠。`None` にはこの証拠が作れない。
pub(open) inductive ResultHas: (Option(Val), Ty) -> Prop {
  Returned<v: Val, ty: Ty>(h: ValHas(v, ty)): ResultHas(Some(v), ty)
}

pub theorem add_safe<x: Option(
  Val
), y: Option(Val)>(hx: ResultHas(x, TNat), hy: ResultHas(y, TNat)): ResultHas(add_val(x, y), TNat) {
  match hx: ResultHas(add_val(x, y), TNat) {
    Returned(vx, tx, hvx) => ⊢ ResultHas(add_val(Some(vx), y), TNat) from match hvx: ResultHas(add_val(Some(vx), y), TNat) {
      HNat(nx) => ⊢ ResultHas(add_val(Some(VNat(nx)), y), TNat) from match hy: ResultHas(add_val(Some(VNat(nx)), y), TNat) {
        Returned(vy, ty, hvy) => ⊢ ResultHas(add_val(Some(VNat(nx)), Some(vy)), TNat) from match hvy: ResultHas(add_val(Some(VNat(nx)), Some(vy)), TNat) {
          HNat(ny) => ⊢ ResultHas(add_val(Some(VNat(nx)), Some(VNat(ny))), TNat) from Returned(HNat)
        }
      }
    }
  }
}

pub theorem eq_safe<x: Option(
  Val
), y: Option(Val)>(hx: ResultHas(x, TNat), hy: ResultHas(y, TNat)): ResultHas(eq_val(x, y), TBool) {
  match hx: ResultHas(eq_val(x, y), TBool) {
    Returned(vx, tx, hvx) => ⊢ ResultHas(eq_val(Some(vx), y), TBool) from match hvx: ResultHas(eq_val(Some(vx), y), TBool) {
      HNat(nx) => ⊢ ResultHas(eq_val(Some(VNat(nx)), y), TBool) from match hy: ResultHas(eq_val(Some(VNat(nx)), y), TBool) {
        Returned(vy, ty, hvy) => ⊢ ResultHas(eq_val(Some(VNat(nx)), Some(vy)), TBool) from match hvy: ResultHas(eq_val(Some(VNat(nx)), Some(vy)), TBool) {
          HNat(ny) => ⊢ ResultHas(eq_val(Some(VNat(nx)), Some(VNat(ny))), TBool) from Returned(HBool)
        }
      }
    }
  }
}

pub theorem if_safe<c: Option(
  Val
), t: Option(
  Val
), e: Option(
  Val
), ty: Ty>(
  hc: ResultHas(c, TBool),
  ht: ResultHas(t, ty),
  he: ResultHas(e, ty)
): ResultHas(if_val(c, t, e), ty) {
  match hc: ResultHas(if_val(c, t, e), ty) {
    Returned(vc, tc, hvc) => ⊢ ResultHas(if_val(Some(vc), t, e), ty) from match hvc: ResultHas(if_val(Some(vc), t, e), ty) {
      HBool(b) => ⊢ ResultHas(if_val(Some(VBool(b)), t, e), ty) from match b: ResultHas(if_val(Some(VBool(b)), t, e), ty) {
        true => ht
        false => he
      }
    }
  }
}

// 型安全性: 型が付いた式を評価すると、必ず値が返り、その値は付いた型を持つ。
pub theorem eval_safe<t: Term, ty: Ty>(h: HasTy(t, ty)): ResultHas(eval(t), ty) {
  match h: ResultHas(eval(t), ty) {
    TyNum(n) => Returned(HNat)
    TyBool(b) => Returned(HBool)
    TyAdd(a, b, ha, hb) => add_safe(eval_safe(ha), eval_safe(hb))
    TyEq(a, b, ha, hb) => eq_safe(eval_safe(ha), eval_safe(hb))
    TyIf(c, t1, e, ty1, hc, ht, he) => if_safe(eval_safe(hc), eval_safe(ht), eval_safe(he))
  }
}

実行結果

✓ theorem add_safe : ∀ x: Option(Val). ∀ y: Option(Val). (ResultHas(x, Ty::TNat)) -> (ResultHas(y, Ty::TNat)) -> ResultHas(add_val(x, y), Ty::TNat)
✓ theorem eq_safe : ∀ x: Option(Val). ∀ y: Option(Val). (ResultHas(x, Ty::TNat)) -> (ResultHas(y, Ty::TNat)) -> ResultHas(eq_val(x, y), Ty::TBool)
✓ theorem if_safe : ∀ c: Option(Val). ∀ t: Option(Val). ∀ e: Option(Val). ∀ ty: Ty. (ResultHas(c, Ty::TBool)) -> (ResultHas(t, ty)) -> (ResultHas(e, ty)) -> ResultHas(if_val(c, t, e), ty)
✓ theorem eval_safe : ∀ t: Term. ∀ ty: Ty. (HasTy(t, ty)) -> ResultHas(eval(t), ty)

ResultHas(r, ty) の構成子は Returned だけなので、None についてこの証拠は作れません。add_safe・eq_safe・if_safe は、演算ごとに「引数が型に合えば、結果も型に合う」ことを示します。eval_safe は HasTy の導出についての帰納法で、型付け規則の一つ一つを、対応する補題で閉じています（第 15 章）。

次に、検査器が規則と一致することを示します。

src/checker.taut

import "core.taut" { Check, HasTy, Term, Ty, check }
import "pipeline.taut" { check_ty, decision_ty, run_if_typed, run_term }
import "safety.taut" { ResultHas, eval_safe }

// 検査器の健全性: 検査器が `Some(ty)` と答えたなら、`t : ty` が成り立つ。
pub theorem decision_sound<t: Term, ty: Ty>(
  d: Check(t),
  said: Eq(Option(Ty), decision_ty(t, d), Some(ty))
): HasTy(t, ty) {
  match d: HasTy(t, ty) {
    Accepted(out, derivation, unique) => match said: HasTy(t, ty) {
      Refl => derivation
    }
    Rejected(refute) => match said: HasTy(t, ty) {}
  }
}

pub theorem check_sound<t: Term, ty: Ty>(
  said: Eq(Option(Ty), check_ty(t), Some(ty))
): HasTy(t, ty) {
  decision_sound(check(t), said)
}

// 検査器の完全性: `t : ty` が成り立つなら、検査器は `Some(ty)` と答える。
pub theorem decision_complete<t: Term, ty: Ty>(
  d: Check(t),
  h: HasTy(t, ty)
): Eq(Option(Ty), decision_ty(t, d), Some(ty)) {
  match d: Eq(Option(Ty), decision_ty(t, d), Some(ty)) {
    Accepted(out, derivation, unique) => Eq::congr(Some, Eq::sym(unique(ty, h)))
    Rejected(refute) => False::elim(refute(ty, h))
  }
}

pub theorem check_complete<t: Term, ty: Ty>(
  h: HasTy(t, ty)
): Eq(Option(Ty), check_ty(t), Some(ty)) {
  decision_complete(check(t), h)
}

// 検査を通した実行は、型の合った値を返す。
pub theorem run_term_safe<t: Term, ty: Ty>(h: HasTy(t, ty)): ResultHas(run_term(t), ty) {
  Eq::subst(
    (r: Option(Ty)) => ResultHas(run_if_typed(r, t), ty),
    Eq::sym(check_complete(h)),
    eval_safe(h)
  )
}

✓ 検査を通過

✓ theorem decision_sound : ∀ t: Term. ∀ ty: Ty. ∀ d: Check(t). (decision_ty(t, d) = Option::Some(Ty, ty)) -> HasTy(t, ty)
✓ theorem check_sound : ∀ t: Term. ∀ ty: Ty. (check_ty(t) = Option::Some(Ty, ty)) -> HasTy(t, ty)
✓ theorem decision_complete : ∀ t: Term. ∀ ty: Ty. ∀ d: Check(t). (HasTy(t, ty)) -> decision_ty(t, d) = Option::Some(Ty, ty)
✓ theorem check_complete : ∀ t: Term. ∀ ty: Ty. (HasTy(t, ty)) -> check_ty(t) = Option::Some(Ty, ty)
✓ theorem run_term_safe : ∀ t: Term. ∀ ty: Ty. (HasTy(t, ty)) -> ResultHas(run_term(t), ty)

check_sound は「検査器が Some(ty) と答えたなら、t : ty」、check_complete はその逆です。どちらも @mode! が Check に入れた導出・一意性・反証を取り出すだけで、規則の場合分けをもう一度書く必要はありません。run_term_safe は、二つを合わせて「型の付く式を run_term で実行すると、型に合う値が返る」ことを示します。

最後に、具体的な式を計算で確かめます。

src/examples.taut

import "core.taut" { Term }
import "eval.taut" { Val }
import "pipeline.taut" { check_ty, run_term }

// 具体的な式は、計算して（`Refl`）確かめる。
theorem sum3_runs(): run_term(TmAdd(TmAdd(TmNum(1), TmNum(2)), TmNum(3))) = Some(VNat(6)) { Refl }
theorem add_bool_rejected(): check_ty(TmAdd(TmNum(1), TmBool(true))) = None { Refl }

✓ 検査を通過

✓ theorem sum3_runs : run_term(Term::TmAdd(Term::TmAdd(Term::TmNum(1), Term::TmNum(2)), Term::TmNum(3))) = Option::Some(Val, Val::VNat(6))
✓ theorem add_bool_rejected : check_ty(Term::TmAdd(Term::TmNum(1), Term::TmBool(true))) = Option::None(Ty)

これらの証明は、公理を使っていません。

19a.8 保証されないこと

tl::parse と tl::Expr::to_i は、表から生成された実行用のコードで、証明の対象外です。そのため、「この文字列の意味がこの木である」ことは証明していません。run_term_safe は、lower_expr が作ったどの Term についても成り立ちます。評価器は Nat を数学の自然数として扱い、実行時の数の表現の上限は扱いません（第 20 章）。

演習 19a.1：* を加えるには、文法・Term・HasTy・eval・lower_expr・証明のどこを変えればよいでしょうか。

演習 19a.2：TyIf から「二つの枝が同じ型」という条件を外すと、eval_safe のどこで証明が通らなくなるでしょうか。