次のメニューの英訳部分がどうも解せなかったのですが、 googleで出すことに成功。「そば」はちゃんと訳すので「傍」にしました。 「椎茸うま煮そば」は出せませんでした。
野菜そば - 檜山正幸のキマイラ飼育記
次のメニューの英訳部分がどうも解せなかったのですが、 googleで出すことに成功。「そば」はちゃんと訳すので「傍」にしました。 「椎茸うま煮そば」は出せませんでした。
上付き・下付き添字をマジに考えたら頭痛がした - 檜山正幸のキマイラ飼育記 (はてなBlog)
先日の記事「古典的微分幾何・ベクトル解析のモダン化： ダイレクトインデックス記法」で、上付き・下付き添字の説明をしたのですが、説明の対象である上付き・下付き添字以外に、上付き・下付き添字の記法を大量に使っている事実に気が付きました。随分とひどいオーバーロード〈多義的使用〉だわ。「過度のオーバーロードはやめよう」と主張している僕としては、ちょっと愕然としました。 僕自身が上付き・下付き添字をどんな目的で使っているかを解説することにより、反省の材料にしたいと思います。また、「古典的微分幾何・ベクトル解析のモダン化： ダイレクトインデックス記法」の分かりにくい記法への補足説明でもあります。 「古典的微分幾何・ベクトル解析のモダン化： ダイレクトインデックス記法」と強く関係している節（第5節です）を読み流してもらえれば、上付き・下付き添字記法がどのように使用されているかの調査報告（ただし、サンプル
有限集合とは何だろう（ストーリー付き練習問題集） - 檜山正幸のキマイラ飼育記 (はてなBlog)
「Xは有限集合である」とか「Xは有限集合でない」とかの表現はよく出てきますが、この有限性ってのはいったい何なんでしょう？ 少しマジメに考えてみることにします。これといった予備知識を要求しませんが、マジメに考える態度は必要です。 実は、有限性を調べるのは目的じゃなくて手段です。証明の“お膳立て”シリーズとか、自然演繹ダメじゃんシリーズ（って、そんなシリーズねえけど、「存在記号の除去規則について考える」とか）に対して、例題を提供するのが、この記事の主たる目的です。この記事を読みながら、ハッキリとは書いてない証明を全部書いていくことが練習問題になります。内容的には超カンタン（当たり前）なので、明示的な証明は逆にハードです。 内容： 自然数についてよく知っているとする 論理記号など 有限性の定義 個数勘定の原理 個数勘定の補題と鳩の巣原理 個数勘定の補題と数学的帰納法 もう少し数学的帰納法のための
奥野幹也『理論から学ぶデータベース実践入門』はどこがダメなのか - 檜山正幸のキマイラ飼育記 (はてなBlog)
言い訳から始めます。この記事を（途中まででも）読んだ人は、次のように言いたくなるでしょう。 『理論から学ぶデータベース実践入門』は良い本なのか悪い本なのか、いったいどっちなんだよ?! この本は間違いや説明不足があり、誤読されやすい表現も多く、その点では残念な本です。しかし、面白いアイディア、するどい観察も含まれていて、行間を補い深読みすれば、多くの示唆を得られる本でもあります。 よって、「良い／悪い」の二択では答えられません。良い点と悪い点の両方を、できるだけ客観的に記述するしかないのです。それをした結果、長い記事となりました。 内容： ことの発端： zhanponさんの批判 奥野本擁護と奥野本批判 僕の擁護・批判の方針 zhanponさんの指摘の再検討 1. 論理的な矛盾とデータの不整合を混同している 2. 命題論理の限界についての説明がおかしい 3. 古典論理の定義を間違えている 4.
2017年 圏論に関する参考文献の案内（無料オンライン版含む） - 檜山正幸のキマイラ飼育記 (はてなBlog)
2017年最初のコメントとして、内海さんから次の情報を教えていただきました; 2016年12月30日に、レンスター（Tom Leinster）の書籍"Basic Category Theory"がオンラインに無料公開されました。 ※ 書籍の表紙画像が表示されないときは、このページをリロードしてみてください。 Basic Category Theory (Cambridge Studies in Advanced Mathematics) 作者: Tom Leinster出版社/メーカー: Cambridge University Press発売日: 2014/07/24メディア: ハードカバーこの商品を含むブログを見る Title: Basic Category Theory Author: Tom Leinster AuthorHomePage: http://www.maths.ed.
viXraのトンデモとarXivのトンデモ - 檜山正幸のキマイラ飼育記 (はてなBlog)
「arXiv.orgのオルタナティブ!? viXra.org」で紹介したviXraは、案の定トンデモの巣窟ですね。だいぶ香ばしい例を紹介すると： Title: The Answers to Two Millennium Prize Problems (2012-12-23) Author: Andrew Nassif Pages: 5p URL: http://vixra.org/pdf/1212.0137v1.pdf Part I: The P vs NP は7行のテキスト、Part II: Riemann Hypothesis は4行のテキストと4枚の画面キャプチャ画像からなります。この2つのミレニアム懸賞問題について“何か”書いてあります。「解いた」つもりなんでしょうか？ 意味不明です。 本家arXivは、トンデモ野放し状態ではないので、ある程度の質は担保されていると言われます。しか
Isabelleについて： 証明支援系は何を目指し、どこへ向かうのか - 檜山正幸のキマイラ飼育記 (はてなBlog)
昨日の記事「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」では、Isabelleのユーザーインターフェースが備えている特徴的な機能である「継続的チェッキング」だけを取り上げました。ここで改めて、証明支援系としてのIsabelleシステムを紹介しましょう。客観的な紹介ではなくて、僕の雑駁な印象記です。 内容： Isabelleの独自な世界 Isabelleの未来 Isabelleの独自な世界 「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」より： PIDE構想は、Isabelleプロジェクト／コミュニティを世の趨勢とは離れた孤立化へと導くのか、それとも、時代がPIDEの先進性にいずれ追いつき、PIDEがスタンダードな証明支援系UIとなるのか？ なかなかに興味深いですな。 Isabelleが世の趨勢と離れるのか？
林晋さんのこと、根拠なきイチャモンのこと - 檜山正幸のキマイラ飼育記 (はてなBlog)
先週のことでタイミングが遅れていますが、 http://d.hatena.ne.jp/JavaBlack/20151103/p1 相変わらず、何の根拠も示さずに知ったふうな事をのたまう。無根拠・非論理の芸風は死ぬまで治らない（治さない）のでしょう。 林晋さん*1へのたちの悪い言及を目にしてしまったので、一言いわずにはおれない気分です。 まず、林晋さんの著書について述べます。林さんの本は3冊持っていて、目次と索引しか見ない僕*2にしてはよく参照してます。 コロナ社の『数理論理学』*3は手が届く場所に置いてあります。 数理論理学 (コンピュータ数学シリーズ) 作者:晋, 林発売日: 1989/12/20メディア: 単行本 カリー／ハワード対応について説明している論理の本は少ないので、非常に助かります。かつてラムダセミナー／モニャドセミナーでカリー／ハワード対応を題材にしたときのネタ本はこれです
もうGitは怖くない： 自信を持って使いたいあなたへ - 檜山正幸のキマイラ飼育記 (はてなBlog)
2014初頭に書いた「WindowsにおけるGit利用環境は整った： Git for Windows と SourceTree for Windows」の最後の文： ブランチは、Gitのなかで最も重要でありながら最も分かりにくい概念でしょう。表面的な言葉に騙されず、先入観を持たず、SourceTreeの視覚的表示（樹形図）の力を借りながら学習するのが、理解への一番の近道です。 そんへんの詳しいことはまたの機会に述べるかも知れません。 1年半以上たってしまいましたが、「またの機会」がやって来ましたよ。ええ、Gitの説明をします、ブランチを中心に詳しく。 「基礎編」と「ブランチ編」で2回に分けようかと思ったけど、長大な記事として一挙公開。これからGitを使う人が対象ではありません。Gitが何をやっているのか、自分が何をやっているのかイマイチ自信が持てない方向けです。 ブランチやマージって、なん
形式言語理論のための代数 - 檜山正幸のキマイラ飼育記 (はてなBlog)
形式言語理論は、かなりの程度、代数的に定式化できます。例えば、形式言語の全体は順序半環、オートマトンはその順序半環を係数とする正方行列だと思えます。オートマトンの初期状態と終状態、オートマトンのあいだの模倣（simulation）関係なども行列により表現できます。 ここでは、できるだけ手短に形式言語理論のための代数、特に半環係数行列の概念を説明します。形式言語とオートマトンの基礎事項についても概要を述べますが、とてもラフな記述なので、他の資料や教科書で予備知識は仕入れておいたほうがいいでしょう。図を多用して幾何的・物理的な比喩を使うと分かりやすくなるとは思うのですが、今回は絵は描きませんでした。絵による説明はまたの機会に。 目標はオートマトンと模倣の圏を作ることです。オートマトンは代数的には正方行列となります。関係圏Rel（の部分圏）をインデキシング圏とするインデックス付き圏を作り、そのグ
1+1ができない子と線形論理 - 檜山正幸のキマイラ飼育記 (はてなBlog)
1+2と1+1 森毅さんが書いていたのだったかな？ 「1+2はできるが、1+1はできない子」の話を読んだことがあります。ちゃんとは憶えてないのですけど、だいたい次のようなことだったかと： 大人：まず1があるだろう。 子供：うん。 大人：そこに2を持ってきて。 子供：うん。 大人：一緒にしたらいくつだ？ 子供：3 と、1+2=3はOK。 大人：まず1があるだろう。 子供：うん。 大人：そこにまた1を持ってきて。 子供：えっ、1はさっき持ってきちゃったから、もうないじゃん。 大人：別な1を持ってくる。 子供：別のだったら、1じゃないでしょ。 僕も似た感覚を持ったことがあるので、この子の発想は理解できます。計算結果を出す前に、計算式を組み立てるとして、そのとき、□+□ のようなテンプレートを考えましょう。また、このテンプレートとは別に、（一桁の数に限定して）1から9の数が書いてあるカードがそれぞ
Makefileの書き方：プログラミング言語Make - 檜山正幸のキマイラ飼育記 (はてなBlog)
「Makefileの書き方、その勘どころ」にて： まだ、関数を使ってソースやターゲットを生成する方法とかパターン規則の説明をしてないので、続きを書くと思います。調べているうちに、GNU Makeの構文（の一部）はある種のプログラミング言語だという気がしてきました；そのことも書きたい気がしてます。 というわけで続きを書きます。 実は、関数呼び出しを使うときは、代入に「=」を使うより「:=」のほうが適切かつ効率的なときが多いのですが、その話は次の機会にします。 これの説明が中心になります。 内容： 前置き 変数の種類と変数定義 ソースコードの後のほうを参照すること Makeは上から下へと実行していくのだ MakeとLispは似ている 実例 ●前置き 以下、Make一般ではなくてGNU Makeの話です。GNU Makeより古いMakeにも備わっていた伝統的機能の説明はしません。 GNU Mak
シェルのリダイレクトを「こわいものなし」というくらい完全に理解しよう - 檜山正幸のキマイラ飼育記 (はてなBlog)
「Java BlockingQueueで遊ぶ：パイプラインごっこ」でパイプラインの話をしたので、本来の、つまりUnixのパイプやリダイレクトを少し調べてみました。 たまに話題となる some-command >file 2>&1 と some-command 2>&1 >fileの挙動の違いについて、「シェルはコマンドラインリダイレクトの指定を右から左に解釈実行する」なんて説明が見つかりました。んなバカな！ パージングは左から右にするものですよ。パーズツリーを逆順にたどることはできるけど、そんなことする必然性はなんにもないよ。 次の記事を読むと、「右から左」なんて事情じゃないことが分かるでしょう。 UNIXの部屋 検索: リダイレクト シェルのリダイレクトにまつわる失敗 さてここでは、複雑なリダイレクト処理も完全に理解できる処方箋を示しましょう。例えば、次のコマンドラインが何をするか分かる
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
この広告怖いよ - 檜山正幸のキマイラ飼育記 (はてなBlog)