日々の流転

λ. Ruby-CPL (仮称)

む、「Ruby-CPL」で検索されてるー。僕がこないだ始めたばかりの計画なので、検索したって情報は何も無いですよー。……というだけなのは何なので、ちょっとは情報を書いてみよう。

まず、CPLというのは「Categorical Programming Language」の略で、論文「A Categorical Programming Language 」に書かれているプログラミング言語です(簡単な紹介)。こいつを再実装して、ふにふにするのが目標。

Ruby-CPLという名前は、単に当面の実装言語にRubyを使ってるから。何でもRubyとかRとか付けるのは良くない習慣だと思うのだけど、名前を考えんの面倒くさいし。

昨日のユニフィケーションの問題は、とりあえずdomain同士のユニフィケーションとcodomain同士のユニフィケーションを一度にやるようにして、それからfactorizerのmost general annotated expressionの求め方の間違いを直したら、試した限りでは問題が出無くなった。

例えば、CCCのSignatureを仮定すると、「pair(pi1, pi2)」の型もちゃんと「λ(X,Y).prod(X,Y) -> λ(X,Y).prod(X,Y)」になるようになった。

domainとcodomainのユニフィケーションを同時にやるだけで本当に十分かどうかというのは不安だけど、あとは問題が起ってから考えることにしよう……

λ. EKO定演

意中の人には断られてしまったので、家族と聴いてきた。

λ. クリスマス

今年のクリスマスは色々な意味で寂しかった。

λ. だるい

頭痛い。また風邪ひいたかも。