付録B 演習のヒントと解答

まず自分で考えてから、確認してください。

B.1 値と関数

3.1

ans-3-1.taut

let a: i64 := 18
let b: i64 := 5
perform show("sum", a + b)
perform show("difference", a - b)
perform show("product", a * b)

実行結果

sum = 23
difference = 13
product = 90

4.1

ans-4-1.taut

fn maximum(a: i64, b: i64): i64 {
  if a < b { b } else { a }
}

perform show("max", maximum(3, 9))

実行結果

・ maximum

max = 9

5.1 の方針：enum Temperature { Cold, Warm, Hot } の三つの構成子すべてを、match で処理します。_ => に頼らず、どのケースを扱ったかを明示してください。

ans-5-1.taut

enum Temperature { Cold, Warm, Hot }

fn describe(t: Temperature): Text {
  match t {
    Cold => "寒い"
    Warm => "快適"
    Hot => "暑い"
  }
}

perform show("t", describe(Warm))

実行結果

・ describe

t = "快適"

6.1：どちらも、型の形（A、あるいはリストの 2 つの形）に沿って、一つずつ処理するだけで、中身の型を知る必要がありません。identity は A を何も調べずに返し、リストの関数は Nil と Cons に分けて、Cons の残りに同じ関数を適用します。

B.2 借用・効果

7.1：読むだけなら &v で借用するほうが自然です。値を消費しないので、呼び出した側が引き続き所有できます。

8.1：空の Vec には、先頭の要素が存在しません。out_of_bounds は、その失敗の可能性を effect として表します。

9.1：k(5) = 6、k(6) = 7 なので、積は 42 です。perform のあとの + 1 も、継続の一部であることが重要です。

11.1：budget は無限の実行を中断する仕組みであって、元の計算に停止性の証拠を与えるものではないからです。

B.3 証明

13.1：a => a が (A) -> A の証明項です。

ans-13-1.taut

import std::Base

theorem imp_id(A: Prop): (A) -> A {
  a => a
}

✓ 検査を通過

✓ theorem imp_id : ∀ A: Prop. (A) -> A

14.1

ans-14-1.taut

import std::Base

theorem reflexive(x: Nat): x = x {
  Refl
}

✓ 検査を通過

✓ theorem reflexive : ∀ x: Nat. x = x

15.1：Nil を基底部、Cons(_, rest) を帰納段階と見ます。帰納段階では、rest についての仮定（rest に対して同じ関数を呼んで得られるもの）を使います。

16.1：タクティクは証明項を提案するだけで、その項が命題の型を持つかどうかは、カーネルが独立に確かめるからです。

17.1：n = n は、任意の n について、反射律で成り立ちます。n = 0 は、n が零である場合にしか成り立ちません。

18.1：要素が消えるときは、「出力は入力の並べ替えである」という Perm の条件を破っています。

19.1 の方針：n: Nat を受け取り、結果の型を gate_step(GateClosed(n), GateSpend) = GateClosed(n) とする定理です。

src/ans-19-1.taut

import std::Nat

inductive GateState: Type {
  GateClosed(balance: Nat): GateState
  GateOpen(balance: Nat): GateState
}

inductive GateCommand: Type {
  GateAuthorize: GateCommand
  GateRevoke: GateCommand
  GateSpend: GateCommand
}

fn gate_balance(state: GateState): Nat {
  match state: Nat {
    GateClosed(n) => n
    GateOpen(n) => n
  }
}

fn gate_step(state: GateState, cmd: GateCommand): GateState {
  match cmd: GateState {
    GateAuthorize => GateOpen(gate_balance(state))
    GateRevoke => GateClosed(gate_balance(state))
    GateSpend => match state: GateState {
      GateClosed(n) => GateClosed(n)
      GateOpen(n) => GateOpen(Nat::pred(n))
    }
  }
}

theorem closed_spend_noop(n: Nat): gate_step(GateClosed(n), GateSpend) = GateClosed(n) {
  Refl
}

✓ 検査を通過

✓ inductive GateState : Type
✓ inductive GateCommand : Type
✓ def gate_balance : (GateState) -> Nat
✓ def gate_step : (GateState) -> (GateCommand) -> GateState
✓ theorem closed_spend_noop : ∀ n: Nat. gate_step(GateClosed(n), GateSpend) = GateClosed(n)

20.1：ソートの定理が対象とするのは、純粋な sort と、それに関する命題です。ファイル入出力の実装や実行環境は、その定理の結論に入っていないからです。