定理証明系イベント
- 9/25で名古屋勢と調整して、だめなら9/17の関数型イベントへの相乗りを考えよう
9.1
- 保守的になりすぎないようにするけど限度はあるよ
- 関数がどんな型を返すか知らないといけない
- 9.1.1 右結合のイメージつかない
T_1->T_2->T_3とT_1->(T_2->T_3)
括弧は優先順位なんじゃないの
9.2
型付けの:が関係を示しています
- |- ジャッジメント、ターンスタイル
- P101 t2の中にxがあったら、それは型T1になってる
- base typeがないって・・・BoolがFig9-1にないよね
- T->T syntax term だから、どの特定の型にも対応。
- 9.2.1
- base typeがないので、T->Tの型しかない
- 具体的なtermがないから
- Boolとかあれば具体的な型になるけど
- ラムダキューブでもλ_{->}になってるよ
f:Bool->Bool e {f:Bool->Bool}
----------------------------- T-Var
gamma |- f:Bool->Bool
----------------------------- T-Var
:
:
: gamma |- false:Bool gamma |- true:Bool gamma |- false:Bool
--------------------------- T-Var --------------------------------------------------------------------------------T-If
gamma |- f:Bool->Bool gamma |- if false then true else false : Bool
--------------------------------------------------------------------------------------------- T-App
{f:Bool->Bool} |- f(if false then true else false):Boolifは関数じゃなくて公理なのね
T-Varはまさに変数宣言ですね
9.3.2
再帰するんじゃないのこれ？
x:S->T ∈ g x:S ∈ g -------------T-var ---------T-Var g |- x:S->T g |- x:S ----------------------------T-App g |- x x :T
S = S->Tを言ってるけど、
S = (S->T)->Tって再帰してしまう。
再帰型があると、ret recが無くても再帰できる
http://togetter.com/li/95541
ここでは型のサイズは有限の表現でないといけない。詳しくは20章でやります。
9.3.1.3のところとか。
9.3.3
サブタームも含めて、帰納的に一意に決まるよ、ってやっていけば証明できる
9.3.4
導出木は下から作っていくけど
上から下を全部上げていく
only ifであることを示せばよい
syntaxのところで繰り返してえられるものと定義した
9.3.1.1は、T-Varを逆転してる関係だね
9.3.1.3,4に対して、uniqueness(9.3.3)が言えるので、9.3.4.1が決定できる
uniquenessがないと、trueが複数の型を持ててしまうので推論できない
Fig9.1ではBoolが出てきてないけど、9.3.4ではBoolが出てきてる
8章との違い
closed termに注目する。free variableがないものを対象にする。
計算できないけどvalueじゃないのはこまるので対象外。
9.3.5
型のつかないものはそもそも評価が先に進めない
valueでもない状態でstuckはしないということか
x:T1 |- t1:T2 --------------T-Abs g |- (lambda x:T1.t1) :T1->T2 g|- t2:T1 ------------------------------------------T-App g |- t1 t2 : T2
intermission
- 圏論の話
- magmaってのがあるよ
9.3.5続き
structural lemmaって何
部分構造論理
gammaってここまでListだったの？可換てことは集合になっちゃうよ
Coqで証明するときも可換にする
Linear Type
一意型uniqueness type
Advanced types and programming languageとか
9.3.8
Typingのルールについてのみ行っています。T-Var,T-App,T-Abs
g,x:S |- t:T g |- s:S
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- -
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
g |- [x |-> s] t:T
E-AppAbsでは型が書いてなかった。これを証明する。
引数を先に評価しないといけないかどうか、評価戦略が変わってくる
やり方は、場合わけしてfig9.1のそれぞれを適用していく
Case T-App
g |- [x |-> s]t1 : T2->T1 g |- [x |-> s]t2 : T2
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- T-App
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
g |- [x |-> s]t1 [x |-> s]t2 : T
9.3.9
t=t1 t2の場合
帰納法の仮定より
t1:T1->t1':T1
t2:T2->t2':T2
t1 -> t1'がある場合
g |- t1':T11->T12 g |- t2:T11
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- -
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
g |- t1' t2:T12
なのでt1 t2 :T12
ない場合は、
t1=
true x = V1
false x
(lambda x:T11,t12)
t1がvalueなら
t1 -> t2'
-
-
-
-
-
-
-
- -
-
-
-
-
-
-
v1 t2 -> v1 t2'
intermission
- Isabelle/HOLは高階関数だけど、高階じゃないIsabelleもあるよ
9.3.10
well-typedじゃないやつは、評価しても型がつかないよ
evaluation ruleにはわざと型が書かれてないし
lambda抽象の後ろに何を書いてもvalueになるってことか
(\x:Bool->Bool. \y:Bool. y) (\z:Bool. true true)
という式でも、
(\y:Bool.y)
が返ってくる。
(\x:Bool->Bool. \y:Bool. y) true
でもこの演習の例になる。
9.4
(P => Q) => P => Q
(pq:P->Q,p:Q):Q
これid使っていいの？(id:P->P)
前提がない場合はidを持ってきちゃいけないので使えない。
interface Func<P,Q> {
public Q apply(P p);
}
class Proof<Q> {
public Q proof(Func<P,Q> pq,P p) {
return pq.apply(p);
}
}すべてにおいて成り立たないといけないんじゃないのか。
P,Qの具体的な形に依存しない。
Djinn, a theorem prover in Haskell, for Haskell.
type inferenceの次はcode inference
以下は同じ f x f $ x $:(a -> b) -> a -> b これはまさにapplyじゃないか flip: (a -> b -> c) -> b -> a -> c flip($) flip id ってやると何が起こる？ id: a -> a flipが適用できるってことはidが2引数だということ id:(b -> c) -> b -> c f 'id' x ってできる。 flip($) とflip idは同じこと。
脚注3
排中律(or Q (not Q))は、constructive logicでは使えない。
具体的に値が決まらないといけないことになってしまうため。
not Q : Q -> False Either Q (Q -> unit)
なんだけど、call-ccがあればうまくいく、という話が
http://www.kmonos.net/wlog/61.html#_0538060508
にあるよ。
9.5.1
評価規則は型に依存していないってところがポイント
Typed Assembly Languageなんてのがあるよ。
配列を扱うのは大変だけど。
