MiniLisp

データ型

1. Nat
2. Bool
3. String
4. Nil
5. Basic := Nat | Bool | String | Nil
6. Tree(X)
7. List(X)

基本関数

1. Nat, Bool, String の色々
2. Tree: left, right, pair, isBasic
3. List: fst, rest, cons, nth, isNil

プログラム式の評価：

$`\quad (p, \rho) \overset{E}{\mapsto} v`$

演繹システム・ソフトウェアの評価

$`\quad (S(A), \rho) \overset{E}{\mapsto} v`$

証明可能性

$`\quad \vdash_S A \iff
(S(A), \rho) \overset{E}{\mapsto} (\mathrm{True}, p)\\
`$