Agda

Agda は関数型プログラミング言語で、テキストで記述していく。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 を入れます。