このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

2016-12-01から1ヶ月間の記事一覧

滝沢カレンさんの言語芸術

滝沢カレンさんの変な日本語が2015年に評判になったようです。もうすぐ2017年ですけど。 モデルプレス 2015-10-06: 間違い連発の日本語が話題に 僕は知らなかったので、「どんな日本語だったんだろう?」とYouTubeを探したら過去の動画がけっこうあります。…

僕の「フローチャート」のイメージ(と心情)はこんなです

昨日書いた記事「「フローチャート」騒ぎ、もう少し頭使って考えてみようよ」のなかで: そもそも、批判/否定している対象であるフローチャートって何なの? 厳密な定義じゃなくてもいいから、どんなイメージを持っているのか知りたいですね。どこがそんな…

「フローチャート」騒ぎ、もう少し頭使って考えてみようよ

割と最近、次の記事がブックマークと注目を集めたようです。 若手プログラマー保存版!フローチャート徹底解説と作成カンニングペーパー 見る前に予想したように、「何言ってんだ!? コイツ」「アホかバカか」的な扱いでしたね。雰囲気としては、「ホメオパシ…

Mizar証明の抜群な分かりやすさ

Mizarの処理系はまったく使いにくいです。その使い勝手は極悪ですわ。それにも関わらず僕が我慢して使おうとしているのは、Mizarの構文と意味モデルが素晴らしいからです。最高ですわ。特に、他の証明系のタクティク言語の難読さに辟易した人には感激もんで…

朗報! Mizar MMLの検索ブラウズツール(追記に悲報)

Mizarは、集合論と一階述語論理を組み込みで持っています。何もない所から(from scratch)、集合論+一階述語論理により意味のある定理を記述するのは労力がかかり過ぎて現実的ではありません。付属のライブラリMML(Mizar Mathematical Library)に頼らざ…

Mizar、嫌いじゃないんだけどな

証明検証系Mizar試用報告、第三弾です。「証明検証系Mizarのジレンマと証明系の村」にて: Mizarの難しさは、言語仕様やモデルに起因するというよりは、システムの機能が古臭すぎて多大なストレスを強いる点にあります。[...snip...]「もったいないなーー」…

証明検証系Mizarのジレンマと証明系の村

証明検証系Mizarを試した印象の続報です。内容: 「これはひどい!」が、「これは素晴らしい!!」 Mizarコミュニティ Mizarの可能性 「これはひどい!」が、「これは素晴らしい!!」Mizarの解説にあるサンプルコードはほぼ動きません*1。僕が試した範囲ではひと…

証明検証系Mizarを試してみる

Mizarは証明検証系です。形式的な証明記述言語とその処理系という括りではCoqやIsabelleの仲間ですが、対話的ではないので使い勝手はだいぶ違います。とりあえずインストールして使ってみましょう。内容: インストール 使ってみる 感想 インストールMizarの…

モノイド圏の随伴性を“豊饒圏の圏”の随伴性に持ち上げる: 計画編

「テンパリー/リーブ圏とカウフマンのスケイン関係式」において、「たぶん成立するだろう」みたいなことを幾つか書いています。そのひとつに次の随伴性があります。 k-LinCat(Link(C), D) Cat(C, U(D)) ここで、k-LinCatはk-線形圏の圏です。Link(-)は単な…