分散合意アルゴリズム Raft を TLA+ で検証する

分散合意アルゴリズム Raft を形式仕様記述言語の TLA+ を用いて検証する手順を紹介します。

A Proof for Log Matching Property of Raft

分散合意アルゴリズム Raft の Log Matching Property について可能な限り形式的な証明をしました。

ナンプレ(数独)は難しさを定義するのが難しい

ナンプレ(数独)は難しさを定義するのが難しい。ナンプレサイトの作成を通して苦労したところを解説します。作成した問題は puzzle.dev で毎日無料で遊べます。

大学数学の個別指導を始めます

はじめに 圏論に最短で入門する - 俺の Colimit を越えてゆけ の中で以下のように書きました。 数学にもともと興味があって数学科に進学した学生でも、大学以降で学ぶ数学についていけなくて挫折してしまう人は多いようです。私の考えでは、 大学受験までの…

Steve Awodey の Category Theory を読む : Chapter 10

Steve Awodey の Category Theory を読む シリーズトップ 10.2 Monads and adjoints Example 10.5 10.3 Algebras for a monad Example 10.7 10.4 Comonads and coalgebras 10.5 Algebras for endofunctors Lemma 10.10 Corollary 10.13 参考書籍 10.2 Monads…

Steve Awodey の Category Theory を読む : Chapter 9

Steve Awodey の Category Theory を読む シリーズトップ 9.1 Preliminary definition Example 9.3 9.2 Hom-set definition 9.4 Order adjoints Example 9.12 9.5 Quantifiers as adjoints 9.6 RAPL Proposition 9.16 9.7 Locally cartesian closed categori…

Steve Awodey の Category Theory を読む : Chapter 8

Steve Awodey の Category Theory を読む シリーズトップ 8.3 The Yoneda lemma 8.4 Applications of the Yoneda lemma Proposition 8.6 8.5 Limits in categories of diagrams Proposition 8.7 8.6 Colimits in categories of diagrams Proposition 8.10 8.…

圏論の入門書籍・入門資料まとめ

はじめに 圏論が数学のみならず幅広い自然科学の分野で利用されるに従って、これから専門的に圏論を学習したいという人がますます増えてくると予想されます。 また Haskell 等の関数型言語を勉強する中で、圏論について専門的に勉強するまではいかないけどど…

Steve Awodey の Category Theory を読む : Chapter 7

Steve Awodey の Category Theory を読む シリーズトップ 7.5 Examples of natural transformations Exercise 9 7.6 Exponentials of categories Proposition 7.13 7.8 Monoidal categories Exercise 18 7.9 Equivalence of categories Proposition 7.26 7.1…

Errata list for An Introduction to Algebraic Topology 4th edition.

はじめに Errata list page 53 line 5 page 74 line -3 page 77 line -7 page 114 line 6 page 118 line -4 page 157 line 14 page 159 line -12 page 183 line 6 page 189 line -6 page 191 line -6 page 213 line -13 page 266 line -18 page 276 line 14 …

Steve Awodey の Category Theory を読む : Chapter 6

Steve Awodey の Category Theory を読む シリーズトップ 6.2 Cartesian closed categories Example 6.5 is an CPO is -continuous is -continuous if is so Example 6.6 6.3 Heyting Algebras Definition 6.10 6.7 Variable sets Exercise 15(a) Exercise 1…

Steve Awodey の Category Theory を読む : Chapter 5

Steve Awodey の Category Theory を読む シリーズトップ 5.2 Pullbacks Proposition 5.5 Exercise 3 5.3 Properties of pullbacks Two pullbacks lemma Proposition 5.10 Example 5.13 5.4 Limits Proposition 5.14 5.6 Colimits Direct limits of groups …

Steve Awodey の Category Theory を読む : Chapter 4

Steve Awodey の Category Theory を読む シリーズトップ 4.1 Groups in a category Corollary 4.6 4.2 The category of groups is an equivalence relation Corollary 4.11 Cokernels are special coequalizers 4.3 Groups as categories composition of th…

二項関係から生成される同値関係に関する形式的な証明

はじめに 二項関係から生成される関係 同値類 同値類と同値関係の性質 はじめに 数学の勉強をしていると、関係 を次の等式を含むような最小の同値関係とする、という定義がよく出てきます。 しかし、この定義は関係 の具体的な構成を与えていないので、この…

Steve Awodey の Category Theory を読む : Chapter 3

Steve Awodey の Category Theory を読む シリーズトップ 3.2 Coproducts Example 3.5 Example 3.6 Example 3.9 Example 3.10 Proposition 3.11 3.4 Coequalizers Example 3.20 参考書籍 3.2 Coproducts Example 3.5 を の UMP より を満たすただ一つの arro…

Steve Awodey の Category Theory を読む : Chapter 2

Steve Awodey の Category Theory を読む シリーズトップ 2.1 Epis and monos Example 2.4 a function is epic iff surjective in any epi into a projective object splits any retract of a projective object is projective 2.3 Generalized elements ult…

Steve Awodey の Category Theory を読む : Chapter 1

Steve Awodey の Category Theory を読む シリーズトップ はじめに 1.2 Functions of sets 1.4 Examples of categories 圏 Definition 1.2 poset category が poset であること Functor は monotone function monotone function は Functor an example from …

CoqのLtacでmap関数を実装する

Coq

はじめに length関数を実装する Gallina 風の実装 Ltac から Gallina へ Gallina の項を Ltac 呼び出しの結果として受け取る 気持ち悪い点 map関数(Ltac引数)を実装する map関数(Gallina引数)を実装する 最後に 参考書籍 はじめに Ltac は、Coq において証明…

Steve Awodey の Category Theory を読む

はじめに 前回の記事では、圏論を学習する上では数学の基礎から学習する必要があると述べました。 一方で、そんなに時間をかけていられない、かけられないといった理由から数学の素養が十分に身についていない状態で Category Theory (Oxford Logic Guides) …

圏論に最短で入門する

はじめに 対象読者 数学以前 数学の基礎 ホモロジー代数 圏論 もっと手取り早く圏論の勉強を始めたい人へ おわりに 紹介した書籍 はじめに 私が圏論という分野を知るきっかけは、おそらくこの文章を読んでいるほとんどの人と同様に Haskell の勉強をしたこと…

R加群の direct limit(順極限、直極限、帰納極限)に関する基本的な命題の証明

はじめに 私はホモロジー代数を以下の書籍で学びました。 絶賛絶版中で入手は困難ですが、現状でも日本語でホモロジー代数を勉強しようと思うと、この本一択になるのではないかと思います。 証明は自分で追える程度に十分に形式的に書かれていて、誤植なども…