■

人は忙しくなったりする事は無いし、忙しいからという理由で何かやらないのは何か個人的に嫌だからやら無いのであって忙しいからソレみたいな事は無いかなーと思っていたけれども、実は私が今忙しくて、人間は相対的に忙しく成る事は在ると思った。

私の忙しいはプログラマの皆さんからしてみれば何が忙しいのか分からないって感じだと思うが、私はプログラマではなくて大学生ですから、ダメです。

例えば、

なんかFirefoxが重い！！

Firefoxが重いのか、Firefoxに寄生しているAdobe Flash Player(ニコニコなんとかさんを再生している)が重いのか知らないけれどもこれはかなり重い。

その重さにめげず書くとすると

data Nat : Set0 where
  zero : Nat
  succ : Nat -> Nat

f : Nat -> Nat -> Nat
f x y with x
f x y | zero with y
f x y | zero | zero = zero
f x y | zero | succ _ = zero
f x y | succ _ = zero

data NatHold : Nat -> Set0 where
  natHold : (n : Nat) -> NatHold n

v : (a1 : Nat) -> (b1 : Nat) -> NatHold (f a1 (succ zero))
v a2 b2 = natHold (f a2 zero)

これは死ぬ。

Inductive Nat : Set := zero : Nat | succ : Nat -> Nat.

Inductive NatHold : Nat -> Set := natHold (n : Nat) : NatHold n.

Definition f (x : Nat) (y : Nat) : Nat :=
  match x with
    | zero => match y with
                | zero => zero
                | succ _ => zero
              end
    | succ _ => match y with
                  | zero => zero
                  | succ _ => zero
                end
  end.

Definition v (a : Nat) (b : Nat) : NatHold (f a (succ zero)) :=
  natHold (f a zero).

これは生きる。

実装は見てないので想像するに、Agda2は関数名と型チェック時に判明している値、判明していない値で区別していて、今回の場合だと

f [判明していない値a,判明している値zero]

みたいな持ち方をしていて判明していない値が「出るまで」は当然の如くcaseも分岐可能なので評価を進めて行けるが、判明しない値が出た時点でそれ以降は判明している値が出ても無駄で、だってまぁそのcaseには到達出来ないので諦める。(今回の場合だと判明している値zeroはダイレクトにsucc zeroと比較されて、ダメ。実際そのようなエラーメッセージが出る。)

諦めた上で一致性をどう扱うかというと、単にリストの要素が各々conversion-ableかどうか見て、ソレみたいな。

一方Coqの場合だと、割と頑張って「case式自体」の一致性を比較出来るようにしてるんじゃないかなっていうソレ。

別の見方をすると

data Nat : Set0 where
  zero : Nat
  succ : Nat -> Nat

data NatHold : Nat -> Set0 where
  natHold : (n : Nat) -> NatHold n

add1 : Nat -> Nat -> Nat
add1 x y with x
... | zero = y
... | succ z = succ (add1 z y)

add2 : Nat -> Nat -> Nat
add2 x y with x
... | zero = y
... | succ z = succ (add2 z y)

v : (a1 : Nat) -> (b1 : Nat) -> NatHold (add1 a1 b1)
v a2 b2 = natHold (add2 a2 b2)

えらーめっせーじ
add2 a2 b2 | a2 != add1 a2 b2 | a2 of type Nat
when checking that the expression natHold (add2 a2 b2) has type
NatHold (add1 a2 b2 | a2)

これは死ぬ。Agda2は名前付きで見てるので、add1とadd2で異なるのでっていうそれで、一方Coqの場合は

Inductive Nat : Set := zero : Nat | succ : Nat -> Nat.

Inductive NatHold : Nat -> Set := natHold (n : Nat) : NatHold n.

Fixpoint add1 (x : Nat) (y : Nat) : Nat :=
  match x with
    | zero => y
    | succ z => succ (add1 z y)
  end.

Fixpoint add2 (x : Nat) (y : Nat) : Nat :=
  match x with
    | zero => y
    | succ z => succ (add2 z y)
  end.

Definition v (a : Nat) (b : Nat) : NatHold (add1 a b) :=
  natHold (add2 a b).

これはおっけーなのだが、

Fixpoint add3 (x : Nat) (y : Nat) : Nat :=
  match x with
    | zero => y
    | succ zero => succ y
    | succ z => succ (add3 z y)
  end.

Definition v (a : Nat) (b : Nat) : NatHold (add1 a b) :=
  natHold (add3 a b).

これはダメだと言われてしまう。

とかいう他にも色々色々こういう事をやってるのです。嘘です・・・。

まぁそれは嘘だけど人は忙しく成る！！っていう事で舌。

と思ってたけど

h : Nat -> Nat -> Nat
h x y with x
h x y | zero with y
h x y | zero | zero = zero
h x y | zero | succ _ = zero
h x y | succ _ with y
h x y | succ _ | zero = zero
h x y | succ _ | succ _ = zero

v : (a1 : Nat) -> NatSame (h zero a1)
v a2 = natSame (h (succ zero) a2)

えらーめっせーじ
h (succ zero) a2 | succ zero | a2 != h zero a2 | zero | a2 of type
Nat
when checking that the expression natSame (h (succ zero) a2) has
type NatSame (h zero a2 | zero | a2)

完全に引数を伴った関数の評価が出来る時と、そうでない時(1つでも評価出来ないcase式その他がある)で分けてて、さっき作ったようにリストな感じにして同じインデクスの値が変換可能か調べているだけな気がする。

しかしそれにしても背中が痛い。なんか温感とか書いてるパナップIDという湿布を買ったけれども、一昨日から痛かった背中に先程張った所非常に痛いというか熱いというか・・・。

腹筋が筋肉痛に成った時にアンメルツを塗って余りの痛さにアルカリ性の何かで流した時よりはマシだなー。