SCGの限界を構成するグラフ列の候補
Haskell をやっていたらいつの間にかに数学にはまってた人です。カタカナではヘキサープと呼んでください。
自分史
2016: たぶん、不可説不可説転とか、その辺りから巨大数を知った。巨大数論に載っている表記を、片っ端から、関数形式で定義しようとしたり、 Haskell で実装しようとしたりしていた（残骸）。別の趣味へと流れていった。
2019-2021: 巨大数 Advent Calender 2018 を発見して再燃する。そこからの活動は知っての通りである。
子記事
- User:Hexirp/メモ
- User:Hexirp/TONの変換
- User:Hexirp/質問
- User:Hexirp/数式の表示について
- User:Hexirp/バシク行列の解析の情報
- User:Hexirp/執筆した記事の一覧
- User:Hexirp/式神巨大数/2020/参加受付
- User:Hexirp/式神巨大数/2020/投稿受付
- User:Hexirp/式神巨大数/2020/応募受付
- User:Hexirp/式神巨大数/2020
- User:Hexirp/式神巨大数/2021/チャット
- User:Hexirp/式神巨大数/2021/規則
- User:Hexirp/式神巨大数/2021/ポータル
テンプレート
- User:Hexirp/Template:Quote Top
- User:Hexirp/Template:Quote Bottom
- User:Hexirp/Template:Scroll Top
- User:Hexirp/Template:Scroll Bottom
- User:Hexirp/tc
- User:Hexirp/tcu
- User:Hexirp/tcm
- User:Hexirp/tcl
- User:Hexirp/bx
- User:Hexirp/bxu
- User:Hexirp/bxl
- User:Hexirp/common.css
お気に入り
- 到達不能基数
- マーロ基数
- 弱コンパクト基数
- 階層内階層基数
- ユーザーブログ:Koteitan/Upper-Branch-Ignoring モデルを使ったバシク行列のヒドラ表現
- ユーザーブログ:Merliborn/Fast-growing hierarchy rivisited
メモ
今日の何か
issue が投稿された日時を x として、その issue についた最後のコメントが投稿された日時を y としよう。今日の日時を z としよう。 2 * (y - x) + day 30 <= z - x の時に ping を行う bot はどうだろうか？
"A Strongly Normalising Curry-Howard Correspondence for IZF Set Theory" が IZF 集合論と同じ強さを持つ型理論を実装している。構成的かどうかには疑問符が付くが。そして、そのアイデアを coq-contribs/izf で実装している。 "the intuitionisitic version of Hilbert's choice operator" なるものが関わっているらしい。
ここでの "the intuitionisitic version of Hilbert's choice operator" は、 HoTT 的には、 Natural_Number(i) : Universe(i) とし P : Universe(i) -> Universe(j) とし epsilon(i)(j) P : Natural_Number(i) -> Universe(i) である。そして、 P : Universe(i) -> Universe(j) とし || Σ { X : Universe(i) } { P ( X ) } || -> || Σ { n : Natural_Number(i) } { P ( epsilon(i)(j) P n ) } || である。
他のウィキ
外部リンク
- Hexirp/googology - ブログ記事の下書き兼バックアップのリポジトリ。他にもいろいろあるよ。
バシク行列システム (BMS) 関係。
- Bachicu Matrix Calculator - バシク行列システムの計算および標準形の判定など。
- kyodaisuu/basmat - GitHub にホストされているソースコード。
- Hydra Viewer - 汎用ヒドラ表示サイト。HTTPなので注意。
- koteitan/hydraviewer - GitHub にホストされているソースコード。
- BMS Upper-branch ignoring Hydra Viewer - バシク行列システムをヒドラとして表示する。
- Naruyoko/BMSHydraViewer - GitHub にホストされているソースコード。