論理と圏論のオイシイ話｜マスログ
※本記事はロマ数トレラン「カリー・ハワード対応から見る『プログラミング言語、論理システム、圏』」の講師である檜山正幸先生によるカリー・ハワード対応の入門記事になります。ご興味を持った方は是非ゼミにご参加ください。ガイダンス回は無料となっております。 ロマ数トレラン「カリー・ハワード対応から見る『プログラミング言語、論理システム、圏』」のお申し込みはこちらのページよりお願いいたします。⇒http://romanticmathnight.org/1245 数学をする上でほとんどの人が（潜在的にでも）使っている古典論理は、強力で万能な論理です。この記事では、古典論理より非力で小さい論理である連言含意論理というものを話題にします。非力で小さいからといって、つまらないわけではありません。非力で小さい論理を糸口にたどっていった先には、けっこう壮大なメカニズムがあったりします。 古典論理 古典論理の「古
Why3 で遊んでみた - amutake's blog
Why3 で遊んでみたのでメモ．インストールで手間取った．環境は Mac OS X 10.9.1 です． Why3 のインストール ※この方法は Mac OS X かつ Homebrew 専用です．Linux や MacPorts でのインストールはわかりません． ソースからは面倒なので，OCaml のパッケージマネージャである opam でいれます．(追記: https://github.com/mht208/homebrew-formal に Why3 の formulae があったのでそっちのほうが簡単かもしれない(試してない)) まず依存ライブラリなどをインストール． XQuartz をインストール インストール後は再ログインが必要かもしれない brew install gmp brew install gtksourceview XQuartz が必要 次に，https://gi
議論を形式論理化することの重要性について - 言語装置hisaket公開記憶域
前置き 以降、「定理」や「証明」のような語はすべて数理論理学における意味だと思ってもらって問題ないはずです。 また、この文章は理解を容易にするための具体例などが欠如しています。時間があれば加筆したい所ですが期待はしないでください。 議論について 議論とは、つまりは複数の人同士が互いに定理とその証明を主張をし合うような活動のことです（強い主張）。 相手の主張が間違っている、すなわち定理が公理から導出不可能であれば、それがなぜ正しくないかを説明すること（反論）、 すなわち相手の主張する命題の証明において推論規則を誤って適用している箇所を提示することで、その証明と結論を修正する手助けをすることができます。 すなわち議論とは、複数の人間というheuristicな計算機を用いて、並列処理的に証明を探索する作業と見なせるということです。 さらには一般に、議論の参加者全員が同一の公理を共有しているとは限
証明の“お膳立て”のやり方 - 檜山正幸のキマイラ飼育記 (はてなBlog)
N君が「こういうのは、どうやって証明したらいいのか… わかんないなー？」と困った顔をしてました。的確な処方箋を述べることは出来ないのですが、ヒントになりそうなことを記しておきます。 目的： 証明の“お膳立て”とは 例題 命題、証明可能性判断、証明要求 連言の分解 含意の変形 全称限量子を型宣言に お膳立てルールの繰り返し適用 同値な命題に置き換える お膳立てを完成させる シリーズ目次： 証明の“お膳立て”のやり方 証明の“お膳立て”のやり方 2： 証明の顧客・業者モデル 証明の“お膳立て”のやり方 3： さらに事例 証明の“お膳立て”のやり方 4： 随伴による集合差の定義 証明の“お膳立て”のやり方 5： 証明可能性判断と推論規則 証明の“お膳立て”のやり方 オマケ1： 集合の内包的記法の困惑 有限集合とは何だろう（ストーリー付き練習問題集） 有限集合とは何だろう への補足 距離空間と位相
フォワード・リーズニングとバックワード・リーズニング - 檜山正幸のキマイラ飼育記 (はてなBlog)
現状の証明支援系〈proof assistant〉について、僕はしょっちゅう愚痴と文句を言っています（twitterでぼやいたりしてる）。大きな不満点は、フォワード・リーズニングの対話的サポートがまったくない点です。不便だし面白くない。 内容： 証明ソフトウェアの進歩は遅い バックワード・リーズニング フォワード・リーズニング フォワード・リーズニングの対話的サポート 証明ソフトウェアの進歩は遅い 「プログラミング言語Lean 4の現状」に書いたように、証明ソフトウェアの開発は膨大な時間と手間がかかるもので、Coq, Isabelle, Mizar は30年から50年ほどの開発期間を経ています。新しいソフトウェアであるLeanでも、もう10年になります。どの開発チームも最優秀の人材を揃えています。それでも「使いものにならない」事実が、証明ソフトウェアの開発が極めて困難であることを物語ってい
単項化定理と群コホモロジー - tsujimotterのノートブック
こんにちは。最近、群コホモロジーがマイブームのtsujimotterです。 群コホモロジーといえば、以前の記事で群コホモロジーに関する定理「ヒルベルトの定理90」を使って、クンマー理論を導く話を書いたことがありました。 tsujimotter.hatenablog.com 今回は ヒルベルトの定理94 という定理について紹介したいと思うのですが、実はこの証明にも群コホモロジーが登場し、クンマー理論のときとほとんど同じような流れで議論ができるのです。 なかなか面白いので、ぜひ最後までお付き合いください。 目次： 単項化定理 ヒルベルトの定理94 ヒルベルトの定理94の証明 おわりに 参考文献 単項化定理 まずは「単項化」とは何かについて説明するところから始めましょう。 代数体 の有限次ガロア拡大 を考え、 の整数環をそれぞれ とします。 の任意のイデアル に対して、 を のイデアルに「持ち上
Martin-Lofの 理論とそのパラドックス - あいまいな本日の私 blog
Martin-Lofの1971年の論文では、循環性がその中核を占めています。彼は、この条件があるので、彼の理論は圏論と非常に相性が良い（ご存知のように、圏論では、圏全体は圏をなし、その意味で強い循環性を持ちます）と主張しています。しかし、翌年に、Girardがこの中核部分の（もしくは現代の書き方では Type: type）からパラドックス（ブラリ-フォルティのパラドックスの一般化）が導けることを証明し、彼の夢は消えました。現在では、循環的部分を削除した、厳格な可述性に基づく依存型理論（おそらく整合的だろうと思われるもの）が、Martin-Lofの体系ということになっています。 さて、Girardのパラドックスですが、文献は Girardの論文は仏文？だったはずなので、Thierry Coquandの An Analysis of Girard's Paradox (LICS 1986)をど
自動テストに限界を感じた私がなぜ形式手法に魅了されたのか - 若くない何かの悩み
長らく自動テストとテスト容易設計を生業としてきましたが、最近は色々な限界を感じて形式手法に取り組んでいます。 この記事では、既存の自動テストのどこに限界を感じてなぜ形式手法が必要なのかの私見を説明します。なお、私もまだ完全理解には程遠いため間違いがあるかもしれません。ご指摘やご意見はぜひ Kuniwak までいただけると嬉しいです。 著者について プログラマです。開発プロセスをよくするための自発的な自動テストを支援する仕事をしています（経歴）。ここ一年は R&D 的な位置付けで形式手法もやっています。 自動テストの限界 自動テストとは 私がここ数年悩んでいたことは、iOS や Web アプリなどのモデル層のバグを従来の自動テストで見つけられないことでした。ただ、いきなりこの話で始めると理解しづらいと思うので簡単な例から出発します。 この記事でいう自動テストとは以下のようにテスト対象を実際に
スマホで「マイナンバーカード」を申請してみた--意外と簡単な手順、旧姓併記はどうなる？
このところ急に注目を集めているマイナンバーカード。10万円の特別定額給付金のオンライン申請にはマイナンバーカードが必須となるためだ。 早々にオンライン申請を済ませた人をSNSで見かけるたび、なぜ取得していなかったのかと思うこともあったが、これまで特に必要になるシーンがなかったのが正直なところ。 マイナンバーカードの取得率は約15％程度だという。今回のことで急速に取得率が上がっていると思うが、実はまだ持っている人のほうが少ないものだったのだ。 そうした中、追い打ちをかけるかのように住民にマイナンバー（個人番号）を知らせるための紙製のカードである「通知カード」が、5月下旬に廃止されるとの発表があった。ただし、当面の間は、通知カードに記載された氏名、生年月日、住所などに変更がない限り、引き続き通知カードをマイナンバーを証明する書類として使えるという。 マイナンバーカード、4つの申請方法 マイナン
ゼロから学んだ形式手法 - DeNA Testing Blog
2020年1月に入社し、SWETの仕様分析サポートチームに加わったtakasek（@takasek）です。 仕様分析サポートチームでは、社内のプロダクト開発に対する形式手法の活用可能性を模索しています。当ブログでも、継続的に形式手法に関する情報発信をしています（形式手法 カテゴリーの記事一覧）。 この記事では、加入3か月を経てようやく形式手法の輪郭が掴めてきた私の視点から、学習前後での理解の変化について振り返ります。想定読者として学習前の私と近い属性——すなわちコンピュータサイエンスや数学の専門教育を受けておらず、主に現場での実務と自習に頼ってきたソフトウェアエンジニアを想定しています。 形式手法を学ぶ前の認識と疑問 ソフトウェアエンジニアとしての私の一番の興味関心は設計手法です。設計は、なんらかの解決したい問題に対して、ある一面を切り取った構造（モデル）を与え、そのモデルを解決の機構に落
形式手法のこれまでとこれから - ヾﾉ*＞ㅅ＜)ﾉｼ帳
2019年が終わろうとしています あけおめ～さて2020年になりました。歴史が長い形式手法の今後を占うため、過去と直近の出来事を振り返りたいと思います。 ツッコミやタレコミは私のTwitter宛かあなたのブログかその他経路でお願いします～ シンボリック実行は形式的であるため本稿では形式手法に含めることにします。 Fuzzing関連はサーベイが甘いので漏れが多いかもしれません。 形式手法・形式検証とは 形式検証とは、厳密に定義された意味論の下で仕様やプログラムが所定の性質を満たすことを形式的に検証するための手法をいいます。「形式的に」とは、検証が事前に定義された知識だけに基づいており、検証手順が決定的であることをいうと私は理解しています。 形式手法は、形式検証に加えて、形式的にプログラムの仕様を厳密に定義するための手法を包含します。 本記事では形式手法を以下の通り大きく3つに独自に分類します
定理証明リンク集
定理証明、特に定理証明支援系(Proof Assistant)はその存在こそ少しずつ浸透しつつあるような気がしないでもないけれど資料とか全然まとまってないのが不便だなと前々から思っていたのでリソースをまとめておきます。 これも追加してほしいみたいなのあったら教えてください。 Proof Assistants 始めるなら次の中から選ぶのがよいと思います。 Coq Calculus of constructionsベースの型システムとリッチなコマンドを備えた言語 このリストの中では最もコミュニティが大きい、入門書等も豊富 型システムと項を書くためのGallina, コンパイラへの命令を記述するためのVernacular, タクティクスの定義に使うLtacなどの言語が混ざって出てくるのが初心者には混乱必至 結構複雑な言語なので使いこなすのはそれなりに大変 Agda Martin-Löf type
Coqで学ぶ証明プログラミング！ テストだけでなく「証明」で安全性を保証する - エンジニアHub｜Webエンジニアのキャリアを考える！
Coqで学ぶ証明プログラミング！ テストだけでなく「証明」で安全性を保証する プログラミング言語「Coq」では、プログラムを「証明」して間違いを防ぐことができます。プログラムの正しさを保証できる一歩進んだエンジニアになりましょう！ coqtokyoを主催する今井宜洋さんの解説です。 みなさん、Coqってご存知ですか？ プログラムを証明して間違いを防ぐという優れものです。今回はそのCoqについて、coqtokyoという勉強会を主催している今井宜洋がお届けします。 プログラムをただ作るだけではなく、その正しさを保証できる一歩進んだエンジニアになってみましょう！ Coqって何？ プログラムを「証明する」ってどういうこと？ Coqを使ってみよう Coqのインストール方法 CoqIDE：Coqによる証明開発のフロントエンド Coqで関数プログラミング プログラムの仕様を記述しよう 証明開発モード ゴ
F*(F Star)の複雑な型システムの何が嬉しいのか？ - Amosapientiam
マイクロソフトが開発中のF* という依存型プログラミング言語を少し触ってみました。 この言語には強力で複雑な型システムが組み込まれています。 現状、依存型言語は世間にはあまり広まっていませんので F*とは？ 複雑な型ってなんだろう？ 複雑な型システムを組み込んで何が嬉しいんだろう？ 何が嬉しくないんだろう？ と疑問をお持ちになる方も多いだろうと思います。 この記事ではF*で使われている複雑な型の一部と、複雑な型を持つことの利点・欠点の一部を述べ、それを簡単なコード例を通じて体感してみます。 疑問に対する答え F*とは？ マイクロソフトと Inria が開発中のプログラミング言語です。 依存型や monadic effect などが組み込まれており、複雑な仕様が型で表現できます。構文は OCaml や F#などのML系関数型言語に似ています。 詳しくは下記のリンクたちを参照。 F* (プログ
Coqによる証明駆動開発で Merge Sort プログラムをつくってみた - にわとり小屋でのプログラミング
OCaml合宿で帰りの車の中でid:zyxwv さんにMergeSortの正しさをどうやって証明するか聞かれてとっさに証明できなかったので、合宿から帰ったあとに一生懸命証明してみた。 プログラムと証明の全体はこちら: yoshihiro503 / mergesort / source / — Bitbucket。 思ったより簡単ではなく、いろいろなテクニックが必要で非常に勉強になった。Coq初心者の人はMergeSortの問題をとりあえずの目標にして証明を頑張ると非常に効率がいいのではないかと思う。 私は、だいたい以下の流れでプログラムした。 Sortedという命題を作り、リストがソート済みであるという状態を定義する mergesort関数があるとして、満たすべき性質(i)を定理として記述する mergesort関数を定義する mergesort関数に必要な補助関数 merge関数を定義し
ipc_botの紹介 - 簡潔なQ
この記事はTheorem Prover Advent Calendarの22日めの担当記事です． 今年の僕の持ちネタの一つですが，ipc_bot というTwitter botを作りました． https://twitter.com/ipc_bot このbotは直観主義命題論理の命題を投げると解いてくれるbotです． 仕組み 証明を探すのは適当にやっても出来るのですが，証明が存在しないことを確認するのは結構大変です． (古典論理の場合は与えられた命題の否定をSATソルバーにかければ正誤がわかりますが，直観主義論理命題論理だとそう簡単ではありません) 証明が存在するかどうかを有限時間内で判定するには，推論規則を色々いじる必要があります．しかしその説明をはてなブログで書くのが面倒になってしまったので過去に某所に寄稿したものを見て下さい． http://www.tsg.ne.jp/buho/305/
ブラウザ上でAgdaを試せるサイトを作ってみた - ぼくのぬまち 出張版
この記事は Theorem Prover Advent Calendar 2014 の4日目の記事です． Agdaがコンパイルできないんだがとか，agda-modeってEmacsだけなんでしょ？とか，そういった話をちょくちょく耳にするし，ProofSummit2014で明日の記事担当のamutakeくんがブラウザからCoq使えるやつを発表してたりしたので，Try Agda というサイトを作ってみた． リポジトリはここ https://github.com/notogawa/agda-interactive-server バックエンドはHaskellでwai+warp+websocketでAgdaのライブラリからAgdaを直に利用．フロントはjquery+ACE editor．画面レイアウトはもちろんbiim兄貴リスペクトだ． サーバ強くないし，あんまりデカい証明に使ったりするとガバガバなリ
日記は効果あり。科学的にも証明されたメリットとは | ライフハッカー・ジャパン
歴史上の人物には、毎日の生活を詳細な日記に残している人がいます。それらの日記には、2つの効果があります。1つが、後世に伝えるための永久に残る記録。もう1つが、書くことによる感情浄化作用です。そんなのどっちも必要ないよというあなたにも、日記をつけることで得られるメリットは絶大なものがあります。では、毎日の考えを記録しておくことに、どんな意味があるのでしょうか。 子どもたちのために自分の生き様を残しておきたい。自分のクリエイティビティを存分に発揮したい。書くことによって感情を吐きだしたい。どんな理由であれ、日記を記すことには大きな意味があります。この記事では、そのひとつひとつの意義について考えてみたいと思います。 書くことは精神的な健康をもたらす 書くことは、あなたの健康に素晴らしい影響を及ぼします。クリエイティビティを保つこと以外にも、日々の生活のストレスを解き放つ働きをしてくれるのです。こ
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
http://coq.inria.fr/pylons/pylons/contribs/bycat/v8.3?cat1=None&cat2=None