Isabelleについて： 証明支援系は何を目指し、どこへ向かうのか - 檜山正幸のキマイラ飼育記 (はてなBlog)
昨日の記事「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」では、Isabelleのユーザーインターフェースが備えている特徴的な機能である「継続的チェッキング」だけを取り上げました。ここで改めて、証明支援系としてのIsabelleシステムを紹介しましょう。客観的な紹介ではなくて、僕の雑駁な印象記です。 内容： Isabelleの独自な世界 Isabelleの未来 Isabelleの独自な世界 「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」より： PIDE構想は、Isabelleプロジェクト／コミュニティを世の趨勢とは離れた孤立化へと導くのか、それとも、時代がPIDEの先進性にいずれ追いつき、PIDEがスタンダードな証明支援系UIとなるのか？ なかなかに興味深いですな。 Isabelleが世の趨勢と離れるのか？
Globularの使い方 (1) - 檜山正幸のキマイラ飼育記 (はてなBlog)
証明支援系Globularを使っている人っているのかな？ まー、いても少数でしょうね。僕はたまに使います。しばらく使わないでいると使い方を忘れます。少なくとも一人のユーザー（＝僕・檜山）にとっては意味があるので、「Globularの使い方」を記録しておきます。 何回かに分けますが、気が向いたら書くつもりなので全体で何回になるか分かりません。何をどこまで書くかの計画もありません。 内容： はじめに 参考URL ワークスペースの管理など 画面構成 左側がセルパレット 中央がビューペイン ビューコントロールとビューイング方式 シリーズ目次 Globularの使い方 (1) Globularの使い方 (2)： サンプル・ワークスペース Globularの使い方 (3)： 定理と証明 はじめに Globularは、機能的には“ある種の”お絵描きソフトです。普通のお絵描きソフトと違うのは、n次元（n
証明検証系Mizarを試してみる - 檜山正幸のキマイラ飼育記 (はてなBlog)
Mizarは証明検証系です。形式的な証明記述言語とその処理系という括りではCoqやIsabelleの仲間ですが、対話的ではないので使い勝手はだいぶ違います。とりあえずインストールして使ってみましょう。 内容： インストール 使ってみる 感想 インストール Mizarのオフィシャルサイトは： http://mizar.org/ 信州大学の日本語ページもあります。 http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/index-j.html 信州大学のアーカイブから、自分の環境に応じたバイナリをダウンロードします。 ftp://markun.cs.shinshu-u.ac.jp/pub/mizar/system/current/ （バイナリの一覧） Windowsの場合、現時点（2016年12月）ではmizar-8
はじめての圏論 その第1歩：しりとりの圏 - 檜山正幸のキマイラ飼育記
全体目次： 第1歩：しりとりの圏 （このエントリー） 第2歩：行列の圏 第3歩：極端な圏達 第4歩：部分圏 第5歩：変換キューの圏 第6歩：有限変換キューと半圏 第7歩：アミダの圏 第8歩：順序集合の埋め込み表現 第9歩：基本に戻って、圏論感覚を養うハナシとか 付録／番外など： 中間付録A：絵を描いてみた 番外：同期／非同期の結合 中間付録B：アミダとブレイド 番外：米田の補題に向けてのオシャベリ 一部のプログラミング言語の背景として、圏論（カテゴリー論）が使われたりするせいか、以前に比べれば多少は圏論に興味を持つ人が増えたような気がしなくもないような。でも、安直な入門的文書はあまり見かけないですね。もちろん、シッカリした教科書や論説はあるんですが、どうもシッカリし過ぎているような。例えば、圏の例として「コンパクト・ハウスドルフ空間と連続写像の圏」とか言われてもねぇ（この例はいい例なんです
ボブ・クックの「物理系実務者のための圏論入門」 - 檜山正幸のキマイラ飼育記 (はてなBlog)
圏論に関する解説的論文（サーベイ／チュートリアル）で、あまり長くないものというと、次はお勧めです。 題名：A Categorical Manifesto 著者：Joseph A. Goguen 分量：20ページ URL：http://citeseer.ist.psu.edu/goguen91categorical.html 題名：SHORT INTRODUCTION TO ENRICHED CATEGORIES 著者：Francis Borceux, Isar Stubbe 分量：28ページ URL：http://www.win.ua.ac.be/~istubbe/PDF/EnrichedCatsKLUWER.pdf 最近、もう1つ秀逸な記事を見つけました。「幼稚園児のための量子力学」を書いたボブ・クック（↓このニイチャン）*1による「物理系実務者のための圏論入門」（Introducing
Wiki処理系を作る前に知るべきこと／考えるべきこと - 檜山正幸のキマイラ飼育記 (はてなBlog)
Wiki構文（Wiki記法のルール）は山にようにイッパイあります。 「新たにもう1つ構文を付け加えても別にいいだろう」と考えるか、「これ以上新しい構文を増やしてはいけない」と考えるかは人によるでしょう。僕は、「集約・統合してWiki構文を減らすべきだ」と考えています。それで、標準的なWiki構文としてWikiCreole 1.0を採用し、KuwataさんがCreoleパーザーを実装しています。 ところが、WikiCreoleの構文記述が曖昧過ぎてサッパリわからんのです。Kuwataさんもイライラしている様子。このような状況はWikiCreoleに限りません。たいていのWiki構文の記述はイイカゲンです -- いやっ、仕様書があるだけでマシなのです。イイカゲンな仕様に適合した（conformantな）処理系を作れと言われてもそりゃ困りますわな。 WikiCreole仕様の曖昧さは以前にも話題
EmacsでJavaScriptソースを快適に読むために：js2-modeとエグズーベラントCtags - 檜山正幸のキマイラ飼育記 (はてなBlog)
「横道にそれすぎ」に書いた事情で、EmacsでJavaScriptソースコードを読む環境を少し整えようかと。 次の2つのツールを導入してみよう、っと。 js2-mode： http://code.google.com/p/js2-mode/ エグズーベラント（EXUBERANT）Ctags： http://ctags.sourceforge.net/ 内容： より良いEmacs JavaScriptモード -- js2-mode 強烈なタグファイル作成ツール -- エグズーベラントCtags エグズーベラントCtagsを調べてみる EmacsでJavaScriptソースを読む ●より良いEmacs JavaScriptモード -- js2-mode 以前（2006年7月）、ひげぽんさんの記事で、「ecmascript-mode.el ＜ javascript.el みたいだ」と書いてあった
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
