Agda
MenuAgda は関数型プログラミング言語で、テキストで記述していく。Haskell に似た構文を持つ。Haskell で実装されている。
プログラムは必ず以下のように始める。
module lambda where
この時に、このファイルは、
lambad.agdaと同じ名前を持つ必要がある。
プログラムは、
name : type name = valueという形で関数型言語での関数の型と定義を与える形式。
仮定なしに使えるのは Set という型しかない。あとは、これから構成していく。構成する要素には、
関数 ( 型は A → B、値は λ x → y ) record data
の三種類。この三種類だけ憶えればよい。
Agdaの操作は、
load と型のチェック 何か入力して、C-C C-L 値の計算 C-C C-N の後に式を入力 (プログラムの実行に相当する)
の二つだけ。その他には、C-C C-C (case文の生成)などがある。
Agda は indent でblockを構成する文法を持ち、Haskell に近い。しかし、以下のことに気をつけよう。
(){}. は変数名には使えない(それ以外は全部使える = とかも) : と = と → の前後には空白が必要空白がないと「ひと続きの名前」として扱われたり、エラーになったりする。-> でも→でも良い。\ x -> y でも λ x → y でも良い。統一しよう。
A → B → C は、 A → ( B → C ) のことf x y は (f x) y のこと
これは複数引数の関数を「少ない引数の関数を返す高階関数」と見るカーリー化に対応している。
f : A → B → Cの時に f x は B → C という型を持つ関数を返していると考える。これは Haskell でも同じ。
型と値は組で書く。型は省略できるが、Agda で重要なのは論理式に相当する型の方である。
name : type name = value定義抜きに使えるのは Set のみである。(正確には Set と、レベルの付いた Set n 。Set は Set zero の省略形)
引数には{}を付けることができる。
id : ( A : Set ) → A → A id x = xは引数の数があっていないので怒られる。
id : ( A : Set ) → A → A id A x = xしかし、A は使われていない。使われてない変数は _ で省略できる。
id : ( A : Set ) → A → A id _ x = xここでAに{}を付ける。
id : { A : Set } → A → A id {_} x = x推論できる{}な変数は省略することが可能である。
id : { A : Set } → A → A id x = x省略された呼出を明示することもできる。
f1 : Nat → Nat f1 = id {Nat}Haskell で id x = x で定義された id の型を調べてみよう。
Agda の infix operator
_・_と書くことにより、
a ・ bは
_・_ a bと同じに扱われる。infix により演算子の順位などを制御することができる。(・の代わりに.を使うと構文エラーになる)
Agda での?
わからない部分には ? と書くことができる。
_・_ : {A : Set } → ? f ・ g = λ x → f ( g x )この? を埋めていく作業が証明になる。
Agda でのエラー
C-C C-L の時に、Agda は
赤 型が衝突していることを示す (書き直しが必要) 黄 十分に引数が具体化(instanciate)されてないことを示す緑 ? で、まだ決めてない部分
などのerrorを出す。これをなくすごとが証明の目標である。
黄色の場合は、{}で省略された型変数を指定するとなおることがある。
エラーが残っている modulde を import することはできない。
他にも
f = f Termination checking failed for the following functions: fなどのerrorがでる。
Agda の設定
% brew info agdaを見ると、
==> Caveats To use the Agda standard library by default: mkdir -p ~/.agda echo /usr/local/lib/agda/standard-library.agda-lib >>~/.agda/libraries echo standard-library >>~/.agda/defaultsとある。~/.agda がちゃんと設定されているかどうかを確認しよう。
文字がずれる場合は、
atton のblog を参考にして、eaw.el を入れます。