kencoba/Verified Programming in Guru

## Verified Programming in Guru
(ns Verified_Programming_in_Guru
  (:use L5 L5.layout))

(defcontext
  {:width 640 :height 480
   :font-family "Gill Sans"
   :font-size 25})

(defmacro code [& body]
  `(with {:font-family "ＭＳ ゴシック" :font-size 14}
    (with-padding {:top 110 :right 0 :bottom 0 :left 10}
     (lines ~@body))))

(defslides
  [(t "超訳 Verified Programming in Guru")
   (with {:font-size 15
          :padding {:top 20}}
	 (lines "Formal Methods Forum"
		"ken.coba"
		"2010/12/05"))]

  [(title "Contents")
   (item "1.Introduction"
	 "2.Monomorphic Functional Programming"
	 "3.Equational Monomorphic Proving"
	 "4.Inductive Equational Monomorphic Proving"
	 "5.Logical Monomorphic Proving"
	 "6.Polymorphic Programming and Proving"
	 "7.Dependently Typed Programming"
	 "8.Specificationality and Dependently Typed Proving"
	 "9.Resource Management with CARRAWAY"
	 "10.Compiling CARRAWAY")]
  [(title "1.Introduction")]
  [(title "1.1 Verified Programming")]
  [(title "1.2 Functional Programming")]
  [(title "1.3 What is Guru?")
   (item "純粋関数型言語"
	 "プログラムのプロパティ証明ができる"
	 "依存型"
	 "Guruのexpr:programs(terms),types,proofs,formulas"
	 "Coqのように複雑な多相性、依存型はない"
	 "関数型ではないモデルもサポートする"
	 "  破壊的に変更可能なデータ構造とか")]
  [(title "1.4 Installing Guru")
   (lines "ダウンロード"
	  "http://code.google.com/p/guru-lang/")]
  [(title "1.5 The Structure of This Book")]
  [(title "1.6 Acknowledements")]
  [(title "2.Monomorphic Functional Programming")]
  [(title "2.1 Preview")]
  [(title "ペアノの自然数")
   (code "Inductive nat : type :="
	 "  Z : nat"
	 "| S : Fun(x:nat). nat.")]
  [(title "足し算")
   (code "fun plus(n m : nat) : nat."
	 "  match n with"
	 "    Z => m"
	 "  | S n' => (S (plus n' m))"
	 "  end")]
  [(title "2.2 Inductive Datatypes")]
  [(title "2.2.1 Unary natural numbers")]
  [(title "2.2.2 Unary natural numbers in Guru")]
  [(title "ライブラリを使うには")
   (code "Include ''../guru-lang/lib/plus.g''.")]
  [(title "計算する")
   (code "Interpret (plus (S (S Z)) (S (S Z)))."
	 " "
	 "> guru sample.g"
	 "(S (S (S (S Z))))")]
  [(title "2.3 Non-recursive Functions")]
  [(title "2.3.1 Definitions")]
  [(title "関数を定義するには")
   (code "Define double := fun(x:nat).(plus x x)."
	 " "
	 "Interpret (double (S (S Z)))")]
  [(title "2.3.2 Multiple arguments")]
  [(title "2.3.3 Function types")]
  [(title "2.3.4 Functions as inputs")]
  [(title "2.3.5 Functions as outputs")]
  [(title "2.3.6 Comments")]
  [(title "2.4 Pattern Matching")]
  [(title "2.4.1 A note on parse errors")]
  [(title "2.5 Recursive Functions")]
  [(title "2.6 Summary")
   (item "inductive datatype"
	 "function application ex. (S Z) and (plus x y)"
	 "non-recursive function ex. fun(x:nat).(plus x x)."
	 "pattern matching")]
  [(title "2.7 Exercieses")]
  [(title "3.Equational Monomorphic Proving")]
  [(title "3.1 Preview")]
  [(title "3.2 Proof by Evaluation")]
  [(title "3.3 Foralli and Proof by Partial Evaluation")]
  [(title "3.3.1 A note on classification errors")]
  [(title "3.3.2 Terms, types, formulas, and proofs")
   (item "terms:プログラムとデータを構成する"
	 "ex. (plus Z Z)"
	 "types:termを分類する"
	 "ex. nat  Fun(x:nat).nat."
	 "proofs:formulasを証明する"
	 "ex. join-proofs partial evaluation"
	 "    foralli to prove a universal"
	 "formulas:termsに関する文を構成する"
	 "ex. {(plus two two) = four}")]
  [(title "3.3.3 Instantiating Forall-formulas")]
  [(title "3.4 Reflexivity, Symmetry and Transitivity")]
  [(title "3.4.1 Error messages with trans-proofs")]
  [(title "3.5 Congruence")]
  [(title "3.6 Reasoning by Cases")]
  [(title "3.7 Summary")
   (item "join t1 t2 => {t1 = t2}"
	 "foralli(x:nat).P (Pは別の証明)"
	 "refl t => {t = t}"
	 "symm P => if {t1 = t2} then {t2 = t1}"
	 "trans P1 P2 => {t1 = t2} {t2 = t3} then {t1 = t3}"
	 "cong t* P => {t1 = t2} then {t* [t1] = t* [t2]}"
	 "case")]
  [(title "3.8 Exercises")]
  [(title "3.8.5")
   (code
    "Define 3_8_5 : Forall(x:bool). { (and x x) = x } :="
    "  foralli(x:bool)."
    "    case x with"
    "      ff => trans cong (and * *) x_eq"
    "            trans join (and ff ff) ff"
    "                  symm x_eq"
    "    | tt => trans cong (and * *) x_eq"
    "            trans join (and tt tt) tt"
    "                  symm x_eq"
    "    end."
    "Classify 3_8_5.")]
  [(title "それぞれの意味")
   (item "x_eq → x = caseの値の式を作る"
	 "   ex. x_eq →x = ff"
	 "join 項1 項2 → {項1 = 項2}の式を作る"
	 "symm {項1 = 項2} → {項2 = 項1}の式を作る"
	 "cong 項 式 → 式の両辺に項を追加"
	 "   ex. cong (and * *) x_eq → (and x x) = (and ff ff)"
	 "trans 式 式 → {a = b} {b = c}の式から {a = c}を作る")]
  [(title "3.8.5")
   (code
    "Define 3_8_5 : Forall(x:bool). { (and x x) = x } :="
    "  foralli(x:bool)."
    "    case x with"
    "      ff => trans cong (and * *) x_eq % (and x x) = (and ff ff)"
    "            trans join (and ff ff) ff % (and ff ff) = ff"
    "                  symm x_eq           % ff = x"
    "    | tt => trans cong (and * *) x_eq % (and x x) = (and tt tt)"
    "            trans join (and tt tt) tt % (and tt tt) = tt"
    "                  symm x_eq           % tt = x"
    "    end."
    "Classify 3_8_5.")]

  [(title "4.Inductive Equational Monomorphic Proving")]
  [(title "Commutativity")
   (code
    "Include ''../guru-lang/lib/plus.g''."
    " "
    "Define ch4_th : Forall(n m:nat). { (plus n m) = (plus m n) } :="
    "  induction(n:nat)"
    "    return Forall(m:nat). { (plus n m) = (plus m n) }"
    "  with"
    "    Z => foralli(m:nat)."
    "         trans cong (plus * m) n_eq      % (plus n m) = (plus Z m)"
    "         trans join (plus Z m) m         % (plus Z m) = m"
    "         trans cong * symm [plusZ m]     % m = (plus m Z)"
    "               cong (plus m *) symm n_eq % (plus m Z) = (plus m n)"
    "    | S n' => foralli(m:nat)."
    "         trans cong (plus * m) n_eq                 % (plus n m) = (plus (S n') m)"
    "         trans join (plus (S n') m) (S (plus n' m)) % (plus (S n') m) = (S (plus n' m))"
    "         trans cong (S *) [n_IH n' m]               % (S (plus n' m)) = (S (plus m n'))"
    "         trans cong * symm [plusS m n']             % (S (plus m n')) = (plus m (S n'))"
    "               cong (plus m *) symm n_eq            % (plus m (S n')) = (plus m n)"
    "  end.")]
  [(title "5.Logical Monomorphic Proving")]
  [(title "6.Polymorphic Programming and Proving")]
  [(title "7.Dependently Typed Programming")]
  [(title "8.Specificationality and Dependently Typed Proving")]
  [(title "9.Resource Management with CARRAWAY")]
  [(title "10.Compiling CARRAWAY")]
)
	(ns Verified_Programming_in_Guru
	(:use L5 L5.layout))

	(defcontext
	{:width 640 :height 480
	:font-family "Gill Sans"
	:font-size 25})

	(defmacro code [& body]
	`(with {:font-family "ＭＳゴシック" :font-size 14}
	(with-padding {:top 110 :right 0 :bottom 0 :left 10}
	(lines ~@body))))

	(defslides
	[(t "超訳 Verified Programming in Guru")
	(with {:font-size 15
	:padding {:top 20}}
	(lines "Formal Methods Forum"
	"ken.coba"
	"2010/12/05"))]

	[(title "Contents")
	(item "1.Introduction"
	"2.Monomorphic Functional Programming"
	"3.Equational Monomorphic Proving"
	"4.Inductive Equational Monomorphic Proving"
	"5.Logical Monomorphic Proving"
	"6.Polymorphic Programming and Proving"
	"7.Dependently Typed Programming"
	"8.Specificationality and Dependently Typed Proving"
	"9.Resource Management with CARRAWAY"
	"10.Compiling CARRAWAY")]
	[(title "1.Introduction")]
	[(title "1.1 Verified Programming")]
	[(title "1.2 Functional Programming")]
	[(title "1.3 What is Guru?")
	(item "純粋関数型言語"
	"プログラムのプロパティ証明ができる"
	"依存型"
	"Guruのexpr:programs(terms),types,proofs,formulas"
	"Coqのように複雑な多相性、依存型はない"
	"関数型ではないモデルもサポートする"
	" 破壊的に変更可能なデータ構造とか")]
	[(title "1.4 Installing Guru")
	(lines "ダウンロード"
	"http://code.google.com/p/guru-lang/")]
	[(title "1.5 The Structure of This Book")]
	[(title "1.6 Acknowledements")]
	[(title "2.Monomorphic Functional Programming")]
	[(title "2.1 Preview")]
	[(title "ペアノの自然数")
	(code "Inductive nat : type :="
	" Z : nat"
	"\| S : Fun(x:nat). nat.")]
	[(title "足し算")
	(code "fun plus(n m : nat) : nat."
	" match n with"
	" Z => m"
	" \| S n' => (S (plus n' m))"
	" end")]
	[(title "2.2 Inductive Datatypes")]
	[(title "2.2.1 Unary natural numbers")]
	[(title "2.2.2 Unary natural numbers in Guru")]
	[(title "ライブラリを使うには")
	(code "Include ''../guru-lang/lib/plus.g''.")]
	[(title "計算する")
	(code "Interpret (plus (S (S Z)) (S (S Z)))."
	" "
	"> guru sample.g"
	"(S (S (S (S Z))))")]
	[(title "2.3 Non-recursive Functions")]
	[(title "2.3.1 Definitions")]
	[(title "関数を定義するには")
	(code "Define double := fun(x:nat).(plus x x)."
	" "
	"Interpret (double (S (S Z)))")]
	[(title "2.3.2 Multiple arguments")]
	[(title "2.3.3 Function types")]
	[(title "2.3.4 Functions as inputs")]
	[(title "2.3.5 Functions as outputs")]
	[(title "2.3.6 Comments")]
	[(title "2.4 Pattern Matching")]
	[(title "2.4.1 A note on parse errors")]
	[(title "2.5 Recursive Functions")]
	[(title "2.6 Summary")
	(item "inductive datatype"
	"function application ex. (S Z) and (plus x y)"
	"non-recursive function ex. fun(x:nat).(plus x x)."
	"pattern matching")]
	[(title "2.7 Exercieses")]
	[(title "3.Equational Monomorphic Proving")]
	[(title "3.1 Preview")]
	[(title "3.2 Proof by Evaluation")]
	[(title "3.3 Foralli and Proof by Partial Evaluation")]
	[(title "3.3.1 A note on classification errors")]
	[(title "3.3.2 Terms, types, formulas, and proofs")
	(item "terms:プログラムとデータを構成する"
	"ex. (plus Z Z)"
	"types:termを分類する"
	"ex. nat Fun(x:nat).nat."
	"proofs:formulasを証明する"
	"ex. join-proofs partial evaluation"
	" foralli to prove a universal"
	"formulas:termsに関する文を構成する"
	"ex. {(plus two two) = four}")]
	[(title "3.3.3 Instantiating Forall-formulas")]
	[(title "3.4 Reflexivity, Symmetry and Transitivity")]
	[(title "3.4.1 Error messages with trans-proofs")]
	[(title "3.5 Congruence")]
	[(title "3.6 Reasoning by Cases")]
	[(title "3.7 Summary")
	(item "join t1 t2 => {t1 = t2}"
	"foralli(x:nat).P (Pは別の証明)"
	"refl t => {t = t}"
	"symm P => if {t1 = t2} then {t2 = t1}"
	"trans P1 P2 => {t1 = t2} {t2 = t3} then {t1 = t3}"
	"cong t* P => {t1 = t2} then {t* [t1] = t* [t2]}"
	"case")]
	[(title "3.8 Exercises")]
	[(title "3.8.5")
	(code
	"Define 3_8_5 : Forall(x:bool). { (and x x) = x } :="
	" foralli(x:bool)."
	" case x with"
	" ff => trans cong (and * *) x_eq"
	" trans join (and ff ff) ff"
	" symm x_eq"
	" \| tt => trans cong (and * *) x_eq"
	" trans join (and tt tt) tt"
	" symm x_eq"
	" end."
	"Classify 3_8_5.")]
	[(title "それぞれの意味")
	(item "x_eq → x = caseの値の式を作る"
	" ex. x_eq →x = ff"
	"join 項1 項2 → {項1 = 項2}の式を作る"
	"symm {項1 = 項2} → {項2 = 項1}の式を作る"
	"cong 項式 → 式の両辺に項を追加"
	" ex. cong (and * *) x_eq → (and x x) = (and ff ff)"
	"trans 式式 → {a = b} {b = c}の式から {a = c}を作る")]
	[(title "3.8.5")
	(code
	"Define 3_8_5 : Forall(x:bool). { (and x x) = x } :="
	" foralli(x:bool)."
	" case x with"
	" ff => trans cong (and * *) x_eq % (and x x) = (and ff ff)"
	" trans join (and ff ff) ff % (and ff ff) = ff"
	" symm x_eq % ff = x"
	" \| tt => trans cong (and * *) x_eq % (and x x) = (and tt tt)"
	" trans join (and tt tt) tt % (and tt tt) = tt"
	" symm x_eq % tt = x"
	" end."
	"Classify 3_8_5.")]

	[(title "4.Inductive Equational Monomorphic Proving")]
	[(title "Commutativity")
	(code
	"Include ''../guru-lang/lib/plus.g''."
	" "
	"Define ch4_th : Forall(n m:nat). { (plus n m) = (plus m n) } :="
	" induction(n:nat)"
	" return Forall(m:nat). { (plus n m) = (plus m n) }"
	" with"
	" Z => foralli(m:nat)."
	" trans cong (plus * m) n_eq % (plus n m) = (plus Z m)"
	" trans join (plus Z m) m % (plus Z m) = m"
	" trans cong * symm [plusZ m] % m = (plus m Z)"
	" cong (plus m *) symm n_eq % (plus m Z) = (plus m n)"
	" \| S n' => foralli(m:nat)."
	" trans cong (plus * m) n_eq % (plus n m) = (plus (S n') m)"
	" trans join (plus (S n') m) (S (plus n' m)) % (plus (S n') m) = (S (plus n' m))"
	" trans cong (S *) [n_IH n' m] % (S (plus n' m)) = (S (plus m n'))"
	" trans cong * symm [plusS m n'] % (S (plus m n')) = (plus m (S n'))"
	" cong (plus m *) symm n_eq % (plus m (S n')) = (plus m n)"
	" end.")]
	[(title "5.Logical Monomorphic Proving")]
	[(title "6.Polymorphic Programming and Proving")]
	[(title "7.Dependently Typed Programming")]
	[(title "8.Specificationality and Dependently Typed Proving")]
	[(title "9.Resource Management with CARRAWAY")]
	[(title "10.Compiling CARRAWAY")]
	)