天泣記

Coq の (Gallina の) 項はマニュアルに以下のように定義されている。

term    ::=     forall binders , term
        |       fun binders => term
        |       fix fix_bodies
        |       cofix cofix_bodies
        |       let ident [binders] [: term] := term in term
        |       let fix fix_body in term
        |       let cofix cofix_body in term
        |       let ( [name , … , name] ) [dep_ret_type] := term in term
        |       let ’ pattern [in term] := term [return_type] in term
        |       if term [dep_ret_type] then term else term
        |       term : term
        |       term <: term
        |       term :>
        |       term -> term
        |       term arg … arg
        |       @ qualid [term … term]
        |       term % ident
        |       match match_item , … , match_item [return_type] with
                   [[|] equation | … | equation] end
        |       qualid
        |       sort
        |       num
        |       _
        |       ( term )

arg     ::=     term
        |       ( ident := term )

binders ::=     binder … binder

binder  ::=     name
        |       ( name … name : term )
        |       ( name [: term] := term )
        |       ’ pattern

型と普通の式がごちゃまぜになっているように感じられるが、依存型 (値に依存する型) を扱う世界なのでそれはそういうものである。

ここで気になるのが binder である。たとえば、無名関数の fun binders => term には、仮引数っぽいところに binder というものが使われている。

binder は 4種類あり、最初のふたつは見慣れた感じであるが、あとのふたつは見慣れない感じである。

とりあえず、全種類使ってみた。

Check fun x => (x : nat).     (* fun x : nat => x : nat       : nat -> nat *)
Check fun (x : nat) => x.     (* fun x : nat => x             : nat -> nat *)
Check fun (x := 0) => x.      (* let x := 0 in x              : nat *)
Check fun '(x, y) => x + y.   (* fun '(x, y) => x + y         : nat * nat -> nat *)

3つめの (x := 0) というのはなんのためにあるのかちょっと謎だが、引数ではなく、let である。 fun なのに関数じゃないものを返すことがあるのか、ということでちょっと驚く。

引数ではないが、変数の束縛は行うものがあるので、引数を示すような名前じゃなくて、binder という名前なのかもしれない。

あと、4つめの '(x, y) というのは、'(pair x y) ということだが、他のコンストラクタでもよい。

Inductive I := c : nat -> nat -> nat -> I.
Check fun '(c x y z) => 0.    (* fun '(c _ _ _) => 0          : I -> nat *)

ただし、関数は total でないといけないので、コンストラクタがひとつしかない帰納型でなければならないだろう。 2つ以上のコンストラクタをもつ帰納型のコンストラクタを指定するとエラーになる。

Fail Check fun 'O => 0. (* nat has two constructors: O and S *)
(* Non exhaustive pattern-matching: no clause found for pattern S _ *)

Inductive I2 := c1 | c2 | c3.
Fail Check fun 'c2 => 0.
(* Non exhaustive pattern-matching: no clause found for pattern c1 *)

天泣記

2018-01-31 (Wed)