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

日常

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

2016-12-27

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

雑記／備忘

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

2016-12-26

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

雑記／備忘

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

2016-12-16

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

雑記／備忘

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

2016-12-12

朗報！ Mizar MMLの検索ブラウズツール（追記に悲報）

雑記／備忘

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

2016-12-10

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

雑記／備忘

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

2016-12-09

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

雑記／備忘

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

2016-12-08

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

雑記／備忘

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

2016-12-05

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

雑記／備忘

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

2016-11-30

高次圏の下部構造を箙〈えびら〉で表現してみる

雑記／備忘

Cが2次元の圏であって、対象、射、2-射（2-セル）を持っているとします。このとき、2-射を忘れて対象と射だけを考えることに何の問題もありません。Cを通常の（1次元の）圏とみなせます。では、対象を忘れて射と2-射だけを考えたいときはどうでしょう。射の…

2016-11-25

簡易版：図から作ったモノイド圏のテンパリー／リーブ線形表現

雑記／備忘

「テンパリー／リーブ圏とカウフマンのスケイン関係式」で述べた状況は、もっと簡単な例でも確認できるので、簡単な例も紹介します。ブレイド図の代わりにアミダ図を使います。アミダ図は、“あみだくじ”でお馴染みの次のような図です。横棒の部分を次のよう…

2016-11-24

「量子と古典の物理と幾何＠名古屋」の話題

雑記／備忘

日時: 2017/02/11 (土) 10:00 ~ 2017/02/12 (日) 17:30 会場: 名古屋大学情報科学棟１階第１講義室（名古屋大学東山キャンパス）登録URL: https://atnd.org/events/82626 ここで何を話そうかな、ってことですが：僕は谷村先生の「物理学者のための圏論入門…

2016-11-22

テンパリー／リーブ圏とカウフマンのスケイン関係式

雑記／備忘

だいぶむかし -- 2008年6月、テンパリー／リーブ代数を話題にしたことがあります。圏論勉強会：3点テンパリー／リーブ代数の掛け算九九ジョニーへの伝言：3点テンパリー／リーブ代数の行列表現 3点テンパリー／リーブ代数の行列表現の作り方テンパリー／…

2016-11-17

巴

日常

同時に発表された2つのニュース［速報］マイクロソフトがThe Linux Foundationへ加盟、プラチナメンバーとして。［速報］Googleが.NET Foundationに加盟、.NETプラットフォームの方向性に関与へ。を見て、頭のなかに巴〈ともえ〉の図が浮かんだ*1 *1:画像…

2016-11-14

モンスター・小林優香選手

日常

ガールズケイリンの小林優香選手：*1こっ、この太もも、筋肉のかたまり、とんでもないパワーが出そうだ。こりゃ無敵なわけだ。今年は怪我や手術で欠場が多かったようですが、2016-11-09の西日本新聞のニュースによると、久留米F1で復帰とのこと。近況成績で…

2016-11-12

言葉の問題だと片付けたがる人々

日常

「ネイティブ広告ハンドブック」という語がなんか目立っていたので、これ何だろう？と思って、境治〈さかい・おさむ〉さんという方の記事「ネイティブ広告ハンドブック」はライターなら読み込んだほうがいい。それがなぜかを解説しておくをチラ読みしまし…

2016-11-09

スパンの圏と行列の圏

雑記／備忘参照用一時参照用

最近気付いたことを大雑把に記します。細部は記述していません。ファイバー積（引き戻し、pullback）が存在する圏Cに対して、スパンの圏Span(C)が定義できます。特にCが集合圏Setである場合を考えます。Span(Set)の話ですね。Span(Set)のなかに、関係圏Relを…

2016-11-03

電話

日常

1986年リリースの「レイニーブルー」（徳永英明）の歌詞は、電話ボックスの外は雨、かけなれたダイアル回しかけて、ふと指を止める。もはや「電話ボックス」を見ることはないし、「ダイアル回す」こともないですね。屋外の電話ボックス以外に、飲食店など…

2016-10-31

量子と古典の物理と幾何

雑記／備忘

というイベントが来年（2017年）あります。日時: 2017/02/11 (土) 10:00 ~ 2017/02/12 (日) 17:30 会場: 名古屋大学情報科学棟１階第１講義室（名古屋大学東山キャンパス）登録URL: https://atnd.org/events/82626 二日目に僕もしゃべります。谷村省吾先…

2016-10-28

Ring, Rng, Rig

雑記／備忘

環（ring）から単位元必須の要求を外した代数系をRngと呼ぶことがあるんですね。知らなかった。 Wikipedia項目： Rng 語源は「a ring without "i"」というダジャレです。ルングと発音すると書いてあるけど、（カタカナじゃない）日本語訳をどうするか？困り…

2016-10-25

真面目に「arXiv vs. viXra」、そしてトンデモ判定器

雑記／備忘

昨日、viXraはもとよりarXivにもトンデモは混じってるよ、と書きました。もちろん、平均的な質はarXivのほうが高いのは間違いありません。arXivとviXraの比較を真面目にやっている人達がいました。その報告がarXivに載っています。 Title: A Scienceographic…

2016-10-24

viXraのトンデモとarXivのトンデモ

日常

「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/p…