Agda に関する覚書
Menu Menu最初にすること
ここでは、Agda についての自分の Know How を書いていきます。いきなり、これを読まずに install と起動方法、命題論理 を試した方がわかりやすいはずです。
Agda では、
関数名 : 関数の型
関数名 = 関数の定義
という形で命題と証明を記述します。
これは、もちろん、
証明はλ式であり、命題は、そのλ式の型に対応する
という Curry-Howard 対応に沿って作られているからです。また、Agda が型付きλ計算そのものでもあることに対応しています。
まず最初に、Agda を使った List 処理について調べます。Agda には data と record がありますが、まずは data について調べます。これは、Haskell の data と同じものなので、Haskell を知っていれば楽でしょう。
data と List
ここでは、 liast-nag.agda を例題として使います。data は、複数の型を組み合わせる方法の一つです。List は Agda の Data.List に定義されているので、まずは、それを使ってみましょう。
module list where
open import Data.List
postulate A : Set
postulate a : A
postulate b : A
postulate c : A
l1 = [ a ]
l2 = ( a :: [] )
普通の List の Cons ( List の Head と Tail の組み ) を作るのが _::_ という演算子になっています。ここで、postulate は仮定であり、定義を書かないで受け入れる命題です。
Data.List の中身を見てみると、
infixr 40 _::_
data List {a} (A : Set a) : Set a where
[] : List A
_::_ : A -> List A -> List A
と書いてあります。data の下に書いてあるのは、data の Constructor です。ここでは、List は [] と _::_ の二つの作り方、二つの種類のケース型を持つことがわかります。List A は自分自身なので、Recursive Type になっています。
Agda はindent が構文の一部なので、data と [] の行は、このとおりでなければなりません。[] と _::_ の先頭は確実に合っている必要があります。その代わり余計な括弧は少なくてすみます。
List {a} の {a} は、 集合のLevel を表しています。 ℓ とかを使うことが多いらしいです。今は気にしない。{} も今は気にしないでおきましょう。
infixr 40 _::_
は、:: は infix operator として使うことができるので、その優先順位などを指定しています。かっこを省略できる程度のメリットがあります。例えば、
a :: b :: c :: []
と書きたいと思いますが、infixr を書かないと、
a :: (b :: (c :: [] ))
と書かないと Parse Error と言われてしまいます。
List の Append は以下のように記述します。
infixl 30 _++_
_++_ : {A : Set } -> List A -> List A -> List A
[] ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)
l1 = a :: []
l2 = a :: b :: a :: c :: []
l3 = l1 ++ l2
= で書かれた定義が二つあるのは、List data のケース型への Patern Matching になっているからです。data で定義された Constructor ( [] と _::_ ) を pattern として、すべて列挙する必要があります。そうしないと文句を言ってきます。
定義の head ( = の左辺 ) に書けるのは、関数名と引数名、そして、Pattern としての data の引数ということになります。_++_ は infix 中置演算子 なので、そいういう使い方をしています。
右辺に現れている :: ( _::_ と中置い演算子であることを明記して書くのが普通らしい ) は、data (この場合は List ) を作っています。左辺で分解して、右辺で構成ていることになります。
Haskell での append と、ほとんど同じ。
append1 [] y = y
append1 (h:t) y = (h:append t y)
C-c C-n を使って、List や Append を試してみましょう。
l1 ++ l2 では、x, xs, ys には、a や c :: [] などが入る。これは Unification と呼ばれる操作になります。
型が合わない場合
Agda では、型を書く時に、その＊型の型＊が合っている必要があります。そして、値の定義を書く時には、その値は型の定義に合っている必要があります。つまり、Agda では、一つの命題と、その証明を書くのに、二段階の型のチェックがあることになります。最初は、
hoge : fuga
hoge = ?
として置いて、型の部分の型の整合性を合わせることに集中します。
data と Equality
data のもう一つの重要な使い方は、等号(Equality)です。
infixr 20 _==_
data _==_ {n} {A : Set n} : List A -> List A -> Set n where
reflection : {x : List A} -> x == x
これは、Relation.Binary.PropositionalEquality に _≡_ として定義されているものと同じです。reflection は反映、鏡に映った同じもの。Agda では refl と書かれることが多いようです。
data の下に書いてあるものは Constructor なので、reflection は、x == x を作る関数ということになります。
{x}
------------- reflection
x == x
というわけなので、x == x は常に正しい。ここで、x は List A つまり、A という型の要素を持つリストになっています。Agda の要素は、結局は集合なので、集合に対して定義されている _≡_ で、ほとんどの場合はすむはずです。実際、_≡_ の refl を使って List の等式を作っても問題ありません。
[] ++ a は a に等しい。したがって、[] ++ a == a のはずです。これは証明するべき型で記述された命題です。Haskell では [] や ++ は値で出くることはできますが、型には出きません。Agda の高階型システムが、それを可能にしています。
list-id-l : { A : Set } -> { x : List A} -> [] ++ x == x
list-id-l = reflection
2行目の reflection は、X == X という data を作成しています。ここで、X は、[] ++ x と x と両方の型に対応する必要があります。そうでなければ等号は成立しません。_++_ の定義の一つ、
[] ++ ys = ys
により、[] ++ x は x に簡約 (reduction) されるので証明自体は x == x として自明です。型としては、[] ++ x == x だが、list-id-l は {x} -> x == x という data 型を返す関数になります。つまり、型の証明がλ式に対応する Curry-Howard 対応を示したのが上の Agda の証明ということになります。
==-to-≡ : {A : Set } {x y : List A} -> x == y -> x ≡ y
==-to-≡ reflection = refl
を使うことにより、_==_ による等式を _≡_ の等式に変換することができます。等式を data で書かない場合 (Relation (関係)として記述する場合とか}は、このような変換ができない場合もあります。
自分で定義した _==_ に関して、合同則、推移則を証明することができます。
cong1 : {A : Set } { B : Set } ->
( f : List A -> List B ) -> {x : List A } -> {y : List A} -> x == y -> f x == f y
cong1 f reflection = reflection
eq-cons : {A : Set } {x y : List A} ( a : A ) -> x == y -> ( a :: x ) == ( a :: y )
eq-cons a z = cong1 ( \x -> ( a :: x) ) z
trans-list : {A : Set } {x y z : List A} -> x == y -> y == z -> x == z
trans-list reflection reflection = reflection
eq-cons は、cong1 の特殊な場合に過ぎません。_≡_ に対しては、cong と trans という名前で定義されています。
cong1 は f x == f x を生成していて、eq-cons は a :: x == a :: y を生成しています。trans-list は結局は、x == x と x= = x から x==x を生成しているだけです。
eq-cons は x == x の x を a :: x で置き換えています。これは unification (単一化) と呼ばれる作業で、変数の値をより詳細に規定することに相当します。この置き換えを適切に行うのが、Agda の型推論のすることになります。
暗黙の変数 {x}
型の引数の変数に {x}を付けることができます。普通に () を使った場合と意味は変わりません。しかし、{} を付けた変数は呼び出し時に省略することができます。省略された引数は、Agda によって推論されます。適切に推論されない場合は、Agda は黄色の表示で文句を言いいます。その場合は、省略せずに{}付きで値を指定してやると直る場合があります。しかし、実際にはいろいろ複雑で場合場合によって対処することになります。