読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

Lambda Cを実装してみた。

404 Not FoundはてなダイアリーでλCが話題になっていたので、Lambda C インタプリタを実装してみた。多相型も依存型もサポート。定理証明もできる。

Lambda C Interpreter

サンプルコード:

  • λ(A:*). λx:A. x (恒等関数)
  • λ(A:*). λ(x:A). λ(y:A). Π(P:Π(a:A). *). Π(p:(P x)). (P y) (ライプニッツイクォリティ(Leibniz equality))
  • λ(A:*). λ(a:A). λ(P:Π(a:A). *). λ(p:(P a)). p (反射律の証明