記事一覧

プロフィール - 2021/06/29 17:16:08 JST

わたしについて。

初等部分構造を用いたErdős-Radoの定理の証明 [PDF版] - 2020/12/27 00:50:12 JST

Erdős-Radoの定理はRamseyの定理に代表されるような,無限組合せ論における分割・彩色性質の一つです.ここではオリジナルの純粋に組合せ論的な証明ではなく,初等部分構造を用いたより簡単な方法を紹介します.

Hausdorff Gap の証明 [PDF版] - 2020/12/27 00:48:47 JST

集合論における Hausdorff Gap の証明.

古典的実現可能性モデルノート - 2020/10/21 21:28:54 JST

古典的実現可能性モデル(classical realisability)の手法は,Curry–Howard対応を拡張する形でZF\mathrm{ZF}のモデルを与える方法であり,Krivineによって導入された. 強制法を特別な場合として含むが,ZFC\mathrm{ZFC}から開始してもZF+¬AC\mathrm{ZF}+\neg \mathrm{AC}のモデルが得られるという点で強制法を真に一般化するものになっている.

Boole値モデルと強制法 [PDF版] - 2020/06/22 14:26:12 JST

集合論における無矛盾性証明で用いられる主要な手法である強制法と,密接に関連するBoole値モデルの手法について,本稿では幾らか証明を省略しつつ概略を採り上げます.また,Hamkinsら [Hamkins:2012qv] の説明に基づいて,超冪とBoole値モデルの関係についても簡単に解説します.

ゆめにっき20200526 - 2020/05/26 23:47:05 JST
Talks - 2019/11/16 16:55:05 JST

これまでに行った講演

こんさんドットコムを TLS (HTTPS) に乗り換えた話 - 2019/11/16 13:51:26 JST

こんさんドットコムを TLS ベースに乗り換えたのでその顛末を。 特に、はてなブックマークの数が移行されないのでちょっと工夫したという話をする。

latexmk で楽々 TeX タイプセットの薦め(& biblatex+biberで先進的な参考文献処理) - 2019/09/04 23:28:44 JST

TeX ファイルの変更を監視して、必要な回数だけ自動タイプセットしてくれる latexmk の紹介です。OMake はもう古い。あとbibtexの代替である biber と biblatex についても紹介。

Raspberry Pi + VPS で自宅グローバル IP の変更自動検知をやった話 - 2019/03/10 18:01:45 JST

光インターネット契約したらルータに VPN 機能が付いていたが、固定グローバル IP を買うのが面倒だったので、Raspberry Pi と VPS の自前 DNS サーバで何とか頑張った話。

CaTeX(軽鳥/怪鳥)で快適 LaTeX ライフ in VSCode - 2018/11/26 23:17:04 JST

YaTeX の補完機能を Visual Studio Code で実現する CaTeX 機能拡張のご紹介。

Emacs から Visual Studio Code に乗り換える作業のメモ - 2018/11/26 23:13:26 JST

Emacs にそろそろ辟易してきたので、VSCode に乗り換えようとしています。その作業記録。

VSCode で YaTeX のイメージ補完やユニコード数式記号を入力する為の拡張をつくった - 2018/11/26 23:12:23 JST

VSCode で YaTeX のイメージ補完相当の機能を実現したり、Agda や Lean などの定理証明系で必要となるユニコード数式記号の入力を補助するための機能拡張を作った話しです。

欲望の赴くままRustで型レベルPeano自然数とサイズ付きベクトルを書いた - 2018/08/29 18:47:50 JST

あるていど強い型システムを持った言語を見ると、型レベルペアノ自然数サイズ付きベクトルを書きたくなる、というのは人類普遍の欲求だと思います。 という訳で欲求に忠実であることとし、型レベルPeano自然数とサイズ付きベクトルRustで実装しました。実用性?皆無です。

Haskellerの私的Rustチートシート - 2018/08/29 18:35:07 JST

Rustに入門したので、適宜HaskellのこれはRustのこれ、ということをここに蓄積していって、個人的なチートシートにする。

zsh hooks を使って ssh / mosh の接続先によって Terminal.app のテーマを変える - 2018/08/02 20:26:47 JST

この記事はQiitaからの移行記事です。情報は古いので、記録以上の価値はありません。

Haskell で Gentzen の LK - 2018/08/02 20:23:56 JST

この記事はQiitaからの移転記事です。 大昔に書いた、シーケント計算をHaskellの型システムを使って上手くエンコードした実装の記事ですが、正直何も整理されていないので、記録以上の意味はありません。

可算推移的モデルの存在について [PDF版] - 2018/06/20 13:52:20 JST

ZFの可算推移的モデルの存在がCon(ZF)よりも真に強いことに関する説明です.

ぜみにっき20180614 - 2018/06/14 23:43:22 JST
ぎょうむにっき20180613 - 2018/06/14 23:41:49 JST
しむにっき20180612 - 2018/06/14 23:31:41 JST
いえにっき20180611 - 2018/06/11 23:58:01 JST
かいものにっきとか20180610 - 2018/06/10 21:18:46 JST
おうちにっき20180609 - 2018/06/09 22:09:10 JST
こーどにっき20180608 - 2018/06/08 22:17:53 JST
じすぜみにっき20180607 - 2018/06/08 01:17:16 JST
けんきうにっき20180606 - 2018/06/06 21:50:09 JST
かれーにっき20180605 - 2018/06/05 23:45:35 JST
りんごにっき20180604 - 2018/06/05 23:01:49 JST
そばにっき20180603 - 2018/06/05 23:01:41 JST
かいていにっき20180602 - 2018/06/02 20:10:12 JST
きょうのにっき20180601 - 2018/06/02 14:18:01 JST
かんぺきにっき20180531 - 2018/06/02 00:36:38 JST
まじでおぼえてないにっき20180530 - 2018/06/02 00:36:06 JST
きゅうせいしゅ(みすいにっき)20180520 - 2018/05/29 21:54:17 JST
活にっき20180528 - 2018/05/29 20:40:04 JST
たいかいしゅにっき20180527 - 2018/05/29 20:39:37 JST
いえにっき20180529 - 2018/05/29 20:19:54 JST
だっしゅつにっき20180526 - 2018/05/29 20:03:19 JST
おしごとにっき20180525 - 2018/05/29 19:26:31 JST
ゼミにっき20180524 - 2018/05/29 19:19:32 JST
にっき20180523 - 2018/05/23 23:33:54 JST
にっき20180522 - 2018/05/22 22:56:55 JST
ゆめにっき未遂20180521 - 2018/05/22 00:06:12 JST
おてつだいにっき20180519 - 2018/05/19 21:55:50 JST
ほげふがにっき20180518 - 2018/05/18 20:59:30 JST
すいりにっき201517 - 2018/05/18 00:25:40 JST
じむにっき20180517 - 2018/05/17 02:06:18 JST
わせだにっき20180515 - 2018/05/15 23:38:42 JST
のみにっき20180514 - 2018/05/14 23:06:37 JST
おうちにっき20180513 - 2018/05/13 20:55:56 JST
にっき20180512 - 2018/05/12 20:18:49 JST
にっき20180511 - 2018/05/11 22:52:18 JST
でーたにっき20180510 - 2018/05/11 03:14:55 JST
カツにっき20180509 - 2018/05/11 03:10:51 JST
ゆめにっき20180508 - 2018/05/08 22:50:51 JST
ほげにっき20180507 - 2018/05/07 22:59:03 JST
社会派にっき20180417 - 2018/05/07 22:56:35 JST
あめにっき20180424 - 2018/05/07 22:56:06 JST
いえにっき20180426 - 2018/05/07 22:55:09 JST
きゅうせいしゅにっき20180428 - 2018/05/07 22:48:13 JST
文フリにっき20180506 - 2018/05/06 23:56:35 JST
いどうにっき20180505 - 2018/05/06 23:33:06 JST
にっき20180504 - 2018/05/05 13:24:40 JST
えらかったにっき20180502 - 2018/05/03 22:06:08 JST
かいものにっき20180503 - 2018/05/03 22:01:27 JST
あついんだがあほなのかにっき20180501 - 2018/05/01 21:13:46 JST
ぱすたにっき20180429 - 2018/05/01 00:28:16 JST
ほんかくにっき20180430 - 2018/05/01 00:25:12 JST
きのうにっき20180427 - 2018/04/28 23:23:25 JST
ほげにっき20180425 - 2018/04/25 23:13:16 JST
Twitter 波括弧事件についてまとめてみる - 2018/04/24 17:51:08 JST

大昔にTwitterで波括弧を書くとテンプレートとして展開されるという事件があって、その時の話をまとめた今となっては考古学的な資料。

How wonderful to be (statically) typed 〜(静的に)型がつくって素晴しい〜 - 2018/04/24 17:51:08 JST

Haskellの型システムの強力さとその工学的な応用例についての発表。

QuickCheck / SmallCheck の紹介 〜オートマトンの例を通して〜 - 2018/04/24 17:51:08 JST

オートマトンの検証という例を通して、QuickCheck や SmallCheck による性質ベースのテスト手法を紹介します。

初めてのブログ - 2018/04/24 17:51:08 JST

ブログを作った報告。技術的な詳細解説。

Yesod を支える技術 - 2018/04/24 17:51:08 JST

大昔のYesodの内部構造についての紹介。

Haskell で LK の定理証明系を書いた - 2018/04/24 17:51:08 JST

Haskellの型機能をふんだんに使って、古典命題論理の体系であるLKの定理証明系を書いた話ぞ。

GHC 7.4.1 の型レベル新機能を使い倒す 〜GADTs、型族 と DataKinds、ConstraintKinds の円環〜 - 2018/04/24 17:51:08 JST

GADTsや型族が入って、GHCの型システムがリッチになりはじめた頃の解説記事。

サーバのデータが消えました - 2018/04/24 17:51:08 JST

サーバ管理はちゃんとしましょうという話。

さらば愛しき JavaScript —— 愛と欲望の果てに Haskell は fay と出逢う。 - 2018/04/24 17:51:08 JST

Haskell のプログラムからJavaScriptを自動生成する Fay という言語処理系についての紹介記事。Haskell Advent Calendar 2012 の七日目の記事。

konn-san.com を刷新した - 2018/04/24 17:51:08 JST

今みてる konn-san.com 設立当時の設立宣言。こっちがメインになるとは思わなかった。

8つの質問で、GHC の type-level language 業界の現状を知る - 2018/04/24 17:51:08 JST

「8つの質問」という釣り記事が技術クラスタで昔流行って、それに便乗してGHCの型システムの話を書いた。

はてなの数式を綺麗にする Chrome 拡張機能をつくった(※はてな以外も※) - 2018/04/24 17:51:08 JST

はてダなど mimetex を使っている数式をMathJax経由で綺麗にレンダーするようにする Chrome 拡張。

2012年度集合論ゼミ発表資料 - 2018/04/24 17:51:07 JST

2012年度の研究室集合論ゼミでの発表資料。

空から Mandelbrot 集合を見てみよう - 2018/04/24 17:51:07 JST

Mandelbrot 集合はよく知られたフラクタル図形ですが、これを「上から」(あるいは「下から」)見てみたらどう見えるのか、というお話。

圏の骨格と選択公理 - 2018/04/24 17:51:07 JST

圏の骨格の存在定理が選択公理と同値であることの証明。

Martinの公理,範疇定理,小さな基数 [PDF版] - 2018/04/24 17:51:07 JST

研究室の集合論ゼミで,集合論の種々の独立命題を示す方法である強制法の理論の最初の方について発表した時の資料.

Pos 圏の射影的対象と選択公理 [PDF版] - 2018/04/24 17:51:07 JST

「Pos圏における射影的対象のなす充満部分圏が集合圏と同型である」ことと選択公理の同値性の証明。

絶対性チートシート [PDF版] - 2018/04/24 17:51:07 JST

公理的集合論においてあるモデルの性質を調べる際,様々な概念の絶対性を利用します.このプリントは,どのような条件下でどんな概念が絶対性を満たすのかをメモした個人的な覚書です.あくまで手軽に使うための覚え書きなので,そこまで踏み込んだ証明などは載せず,寧ろ一覧表のような体裁になる予定です.

第四回選択公理オフ:数理論理学の初歩の初歩の初歩の…… [PDF版] - 2018/04/24 17:51:07 JST

第四回選択公理オフでの発表資料.選択公理と関連するモデル理論の初歩の話です.初学者向けに論理式やモデルの定義から入り,超積や超冪と選択公理,超準解析の関わりなどを論じています.実は Łoś+超フィルター定理と選択公理は同値だよとかそういう話もあり.

計算機代数ゼミ発表資料 - 2018/04/24 17:51:06 JST

2013年度の計算機代数ゼミの発表資料です。主にGröbner基底の基礎理論から、それを応用した消去理論、連立代数方程式の解法などについてを取り扱っています。

今年の冬は Gröbner 基底でスーパー大学受験ガール! - 2018/04/24 17:51:06 JST

受験問題の大半は、 Gröbner 基底を使うことで楽々解き切ることが出来ます!今回はそうしたGröbner基底の技をドドドーン!とご紹介!!今年の受験数学は Gröbner 基底で乗り切りましょうそうしましょう!

F4, F5 アルゴリズムに関するサーベイ(A survey on F_4 and F_5 algorithms) - 2018/04/24 17:51:06 JST

Gröbner基底の効率的な計算法である F4, F5 アルゴリズムに関するサーベイ、メモ(A note on F4 and F5 algorithms to efficiently compute Gröbner bases)。

On Regularity Properties of Sets of Reals and Inaccessible Cardinals (実数の集合の正則性と到達不能基数) - 2018/04/24 17:51:06 JST

修士論文。Solovayによる「ZF+弱い選択公理+“任意の実数の集合が可測”」という体系の無矛盾性証明と、およびKhomskiiによる一般化、そしてSolovayの逆向きの結果であるShelahの結果についてのサーヴェイ論文。また、上述の体系における代替的な解析学の結果も簡単に紹介。

超積によるコンパクト性定理の証明と超準モデル ──君の知らない自然数── - 2018/04/24 17:51:06 JST

超積によるコンパクト性定理の証明と、無限大を含む自然数の超準モデルの構成法について。

定理証明系 Haskell - 2018/04/24 17:51:06 JST

Haskell Advent Calendar 2013 および Theorem Prover Advent Calendar 2013 参加記事。Haskell における依存型プログラミングおよび定理証明について解説した数少ない日本語文献です。C85 の TCUG に寄稿させて頂いた Haskell で定理証明を行う記事の販促記事でもあります。

絶対に理解出来ないモナドチュートリアル - 2018/04/24 17:51:06 JST

絶対に理解出来ないモナドチュートリアルです。

Extensible Effects はモナド変換子に対する救世主になり得るか? - 2018/04/24 17:51:06 JST

Oleg らによる、モナド変換子に対する大体手法、Extensible Effects の論文を読んだ感想紹介記事です。

Haskell ではじめるふわとろ Cocoa アプリ開発 - 2018/04/24 17:51:06 JST

Haskell による Cocoa アプリ開発の実際についての記事。Haskell Advent Calendar 2014 参加記事です。

イガスレイヤー 最終エピソード ザ・ラスト・ジャッジメント - 2018/04/24 17:51:06 JST

山田風太郎『甲賀忍法帖』をニンジャスレイヤー文体に翻訳したもの。

コントの中に観るミステリ精神 〜Monty Python とラーメンズから〜 - 2018/04/24 17:51:06 JST

Monty Python やラーメンズのコント作品を、ミステリ的視点から鑑賞する。

『夏と冬の奏鳴曲』論 ──或いは喪われた中心と探偵小説 - 2018/04/24 17:51:06 JST

麻耶雄嵩『夏と冬の奏鳴曲』を一種のメタ・ミステリと捉え、本編において提示された世界観や構造を基に、近代科学の台頭とキリスト教的世界観の崩壊とミステリ文学の勃興について新たな視点を提供する。

本格ミステリと『真相』の問題 〜三津田信三『作者不詳 ミステリ作家の読む本』〜 - 2018/04/24 17:51:06 JST

三津田信三『作者不詳』を題材に、本格ミステリにおける真相の問題について考察する。あわせて、ミステリにおける「論理」とはいかなる推論様式であるのかについて明らかにする。

夢野久作の世界 ~破格の異色作家と本格ミステリ~ - 2018/04/24 17:51:06 JST

夢野久作の短編についての考察と久作の作品世界についての紹介。ドグラ・マグラの布教。

Cohen実数はSuslin木を付加する [PDF版] - 2018/04/24 17:51:06 JST

Shelahは実数の集合の性質に関する記念碑的論文 [Shelah:1984] において滅茶苦茶いろいろな事を示していて本当にヤバいんですが,その中で一節割いて「Cohen実数を付加するとSuslin木も足される」という事を示しています.原論文における構成は結構煩雑に見えますが,後にTodorčevićは彼の発明したの手法を用いて自然で比較的簡単な構成を与えました.minimal walkの手法はAronszajn木の構成にも使えますが,これとCohen実数を単に合成してやる事でSuslin木が得られるのです.本稿ではこの方法について(強制法の基礎理論は別にして)証明します.

Definability lemma と Truth lemma [PDF版] - 2018/04/24 17:51:06 JST

研究室の集合論ゼミで,強制法の理論を支える基本的な定理である Definability lemma と Truth lemma の証明を発表したときの資料。

一意分解整域とその商体における Eisenstein の既約判定法 [PDF版] - 2018/04/24 17:51:06 JST

Eisenstein の既約判定法は Q[X] や Z[X] の既約多項式の判定法として広く知られていますが,実は係数環が一般の一意分解整域やその商体であっても使えることはそこまで知られていません.この事実を使うと,例えば多変数多項式環の既約元判定を簡単に行える場合があります.

強い選出原理としての強制公理 [PDF版] - 2018/04/24 17:51:06 JST

強制公理Forcing Axiom)とは,ある種類の強制法による拡大と現在の宇宙がある意味で「近い」ことを述べる公理ですが,これは現代数学で用いられる選出原理であるZornの補題従属選択公理(DC\mathrm{DC}の一般化と見ることも可能です.後者の説明は,強制法の理論に関する知識が必要ないため,集合論以外の分野の人にもある程度理解しやすいことが期待されます.
そこで本稿では,強制公理の強い選出原理としての側面に焦点を当てて,強制法に馴染みの無い人にも強制公理がどんなものなのかを解説し,ついでに強制法とは何かについても軽く説明していきたいと思います.対象読者層としては,学部三〜四年程度の数学を知っていてZornの補題を使って何かを作る議論をしたことがあれば十分なようにしたつもりです.

強制法のはじめのほう(1) [PDF版] - 2018/04/24 17:51:06 JST

研究室の集合論ゼミで,集合論の種々の独立命題を示す方法である強制法の理論の最初の方について発表した時の資料.

集合論の地質学3:Bukovskýの定理──強制拡大の特徴付け [PDF版] - 2018/04/24 17:51:06 JST

集合論の地質学に関する記事の第三回目. 最終目標の下方有向性原理の証明の準備として,Bukovskýによる強制拡大の特徴付けを証明します. 前回はこちら初回はこちら

集合論の地質学1:概観と基礎モデルの定義可能性 [PDF版] - 2018/04/24 17:51:06 JST

集合論の宇宙VVは何らかの内部モデルの強制拡大になっているか?そもそもそういった基礎モデルは幾つあるのか?——こうした問題を考えるのが集合論の地質学Set-theoretic geology)です.本稿では,その入門的な部分の解説を行います.
次回はこちら

集合論の地質学2:マントルの構造と下方有向性原理 [PDF版] - 2018/04/24 17:51:06 JST

集合論の地質学に関する記事の第二回目.今回は地質学の基本定理である下方有向性原理の紹介と,そこから得られるマントルM\mathbb{M}に関する帰結を紹介します.前回はこちら

集合論の地質学4:下方有向性原理の証明 [PDF版] - 2018/04/24 17:51:06 JST

集合論の地質学に関する記事の第四回目. 今回はいよいよ,マントルや生成多宇宙の構造の大部分を確定させる基本定理である下方有向性定理を証明します.
前回はこちら初回はこちら

Measure Problem と可測基数 [PDF版] - 2018/04/24 17:51:06 JST

選択公理の下で Lebesgue 可測でないような R の部分集合が存在することは広く知られた事実である.本稿では,測度の条件を幾らか緩めることで,Rの全ての部分集合が可測になるように出来ないだろうか?という問題と,そこから派生した集合論・測度論的な話題について紹介する.

うたにっき20180413 - 2018/04/24 17:51:03 JST
うたにっき20180414 - 2018/04/24 17:51:03 JST
うたわないにっき20180415 - 2018/04/24 17:51:03 JST
かじょうがきにっき20180416 - 2018/04/24 17:51:03 JST
ふつかぶんにっき20180418-19 - 2018/04/24 17:51:03 JST
はやおきにっき20180420 - 2018/04/24 17:51:03 JST
すちゅーにっき20180421 - 2018/04/24 17:51:03 JST
いえにっき20180422 - 2018/04/24 17:51:03 JST
いえにっき20180423 - 2018/04/24 17:51:03 JST

Comments