計算モデルと論理とゲーデルの不完全性定理 - Gemmaの日記
ゲーデルの不完全性定理は、数学を扱う数学、つまりメタ数学を考えるが、それだと理解が難しい。しかし、証明(数学)＝プログラムという悟りを開くと、プログラムを扱うプログラム、つまりメタプログラムを考えればよくなり、それならコンパイラ等でなじみがあるので理解が優しくなる。 話の流れは以下。 1. プログラムとは何か 2. 証明とは何か 3. 証明＝プログラム , （ {、 { ヽ.ｰ､､ ＼､__ぃ._ゝ⌒ヾ iヾ）}､_ ﾝ_ｰ-_二ｰ-, 〉 {厶 _､ヽ _ ヽ._＞'´ ／ /,ィ／ / ハYﾍい ,. -- 〃⌒ r−-､ ィ´ 〃 ,ｲ/7' ,ｲイ/ 小ヽ 丶、 ,. ‐ '´ﾊ i ″｀ヽ、 、ヽ、 ／幺ィ {从{小込v' jｩ仏厶川ﾘ} YV, 小 Vj. |丶 ヽ ｀ ｰ-ミー--'_,辷三彡
今日のCoq: 型づけ規則とそれに関する補題 - みずぴー日記
とうとう、型づけ規則の定義ができました。 というわけで、簡単な補題を証明しようとしたところ、string_decがうまく扱えなくて挫折しました。 証明したかった補題はTAPLに載っている「Inversion of the typing relation」という補題です。TAPL曰く、Immediate from the definitionらしいです。 (* typing t tenvは、型環境tenvにおいてtが型づけ可能ならSome type、型がつかないならNoneを返す。 *) Lemma InvTypeRelVar : forall (tenv : list (string * type)) (x : string) (r : type), Some r = typing (Var x) tenv -> In (x,r) tenv. というわけで証明にチャレンジします。 まずは、
Lambda Tamer
The Lambda Tamer project tackles the issues surrounding computer formalization of programming languages and their tools, based around the Coq proof assistant. The Lambda Tamer methodology centers on higher-order and dependently-typed abstract syntax and aggressive automation. The main project output is a library of Coq definitions, theorems, and tactics in support of building certified compilers f
第14回 型＝命題，プログラム＝証明
MLの型と型推論 この連載でも何回か触れたが，MLやHaskellなど多くの静的型付き関数型言語には，「型推論」という機能がある。これは，プログラム中の変数や関数の型を省略しても，「もっとも一般的」な型を言語処理系が勝手に推論してくれる，という機能だ。 例えば，次のように，二つの引数xとyを受け取って，(x, y)という組を返す関数pairを定義してみよう。 > ocaml Objective Caml version 3.10.0 # let pair = fun x y -> (x, y) ;; val pair : 'a -> 'b -> 'a * 'b = <fun> # このように，pairは「何らかの型'aを持つ値と，何らかの型'bを持つ値を受け取り，'a型の値と'b型の値の組を返す」と推論される。一般に，t1 -> t2は，型t1の値を受け取って，型t2の値を返す関数の型であ
ホワット・ア・ワンダフル・ワールド Proof Assistant Coq
The Coq proof assistant を，とりあえず apt-get でインストール (coq，coq-libs，coqide) してみようと思ったら，debian パッケージが壊れているっぽくて，インストールできませんでした (stable/testing/unstable いずれも)．残念．そのうち直ると思うので，しばらく様子を見てみます(軟弱者)． ちなみに Coq ってのは，Agda や Isabelle/HOL と同じような，定理証明支援系のこと．Calculus of Inductive Construction とかいう，あまり聞きなじみが無い論理体系をベースにしているそうな． # これについては，Interactive Theorem Proving And Program Development: Coq'art: The Calculus Of Inducti
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Yoshihiro503 on Twitter: "推論規則Tシャツを着る息子 http://t.co/vCUcWljb8l"
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください) on Twitter: "@yoshihiro503 Wikipedia等では議論のある用語ですけど、私の知る限り研究コミュニティでは「型検査が成功したら、stuck状態にならない」のが「強い型付け」(strong typing)だと思います"
情報処理学会コンピュータサイエンス領域奨励賞を受賞しました - soutaroブログ
らくがきえんじん
Lambda C Interpreter