サクサク読めて、アプリ限定の機能も多数!
トップへ戻る
買ってよかったもの
www.orecoli.com
はじめに 分散合意アルゴリズム Raft とは 分散合意アルゴリズムとは Raft の特徴 Raft が満たす性質 Election Safety Leader Append-Only Log Matching Leader Completeness State Machine Safety TLA+ とは TLA+ による Raft の形式的仕様 TLA+ による Raft の検証方法 TLA+ Toolbox のインストール 新規 Spec の作成 Model の作成と実行 補足: コマンドラインでの検証 Raft の拡張について Leadership Transfer Membership Change Log Compaction Client Interaction おわりに Raft 理解度を調べるクイズ 参考資料 Raft に関する資料 TLA+ に関する資料 はじめに この
背景 Log Matching Property の証明 データ構造と述語の定義 AppendEntries 関数の性質 leader の log に関する性質 Log Matching Property の証明 参考資料 背景 分散合意アルゴリズム Raft は kubernetes のクラスターの構成情報を保存する etcd の内部で使われておりお世話になっている方も多いアルゴリズムだと思います。 この記事では Raft の満たす重要な性質である Log Matching Property について証明します。 元々、『Raft を TLA+ で検証する』というタイトルの記事を書こうと考えて Raft の考案者 Diego Ongaro の博士論文を読み始めました(その記事は後日公開予定です)。 アルゴリズムは論文の 3 章に書かれているのですが、そこで Raft が常に成り立つことを
はじめに 仮置きは最強のテクニックだけど邪道です 世界一難しいナンプレの問題の作成に失敗 ナンプレを解くための 13 個のテクニック ナンプレの難しさを定義する まだ発展・改良の余地はあるか? おわりに 補足: 技術的な話 サイトを支える技術 Sat Solver を利用した問題の自動生成 Sat Solver の使用場所 Sat Solver とは ナンプレのルールを連言標準形で表現する ナンプレの問題を Sat Solver で解く 答えが 1 つしかないことを Sat Solver で確認する 連言標準形への変換 Sat Solver の応用例 対称性を用いた問題の複製 はじめに 私は先日、最新技術にキャッチアップするためにレベル別ナンプレ(数独) – 無料問題集 | パズル製作研究所(以下 puzzle.dev)というナンプレのサイトを構築しました。サイトでは自動生成した大量の問題
はじめに 圏論に最短で入門する - 俺の Colimit を越えてゆけ の中で以下のように書きました。 数学にもともと興味があって数学科に進学した学生でも、大学以降で学ぶ数学についていけなくて挫折してしまう人は多いようです。私の考えでは、 大学受験までの計算主体の数学から、大学以降の証明主体の数学への移行を明確に意識させること 移行のためのトレーニングを積ませること を学生が認識できる形で教育機会として大学が提供できていないことが原因なのではないかと考えています。 このブログを初めて以来、何人かの学生の方から数学の学習について相談を受けています。彼らと話をしているとどうも証明主体の数学の勉強を進める上での基礎が十分ではないように感じます。結果、数学の勉強の進め方、勉強の仕方に問題を抱えているように感じました。 私も数学の勉強を始めた当初は同じ問題を抱えていました。当時私が感じていた問題は次
はじめに 圏論が数学のみならず幅広い自然科学の分野で利用されるに従って、これから専門的に圏論を学習したいという人がますます増えてくると予想されます。 また Haskell 等の関数型言語を勉強する中で、圏論について専門的に勉強するまではいかないけどどのような学問なのか知っておきたい、という人もいるでしょう。 以前は圏論について知ろうと思うと初見殺しとして有名な 圏論の基礎 や英語の専門書しか利用できなかったのですが、最近では圏論について日本語で読める書籍が揃ってきました。 また、教科書的なものに限らず読み物的な書籍も幾つか出版されています。 現状でも圏論について書かれた書籍はたくさんあると思います。また、ネット上にもたくさんの圏論に関する解説ブログや資料があります。それらを全て読んで紹介することは不可能なので、ここでは以下のような基準 (必ずしも厳密ではない) を設けた上で、私の独断で入門
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 the congruence category is well-defined is a congruence Theorem 4.13 4.4 Finitely presented categories smallest congruence 参考書籍 4.1 Groups in a category Corollary 4.6 任意の が a
はじめに 二項関係から生成される関係 同値類 同値類と同値関係の性質 はじめに 数学の勉強をしていると、関係 を次の等式を含むような最小の同値関係とする、という定義がよく出てきます。 しかし、この定義は関係 の具体的な構成を与えていないので、この同値関係に関する証明をしようとすると途端に行き詰まってしまいます(例えば、商空間を定義域とするような関数が well-defined であることを証明する場合など)。 この記事では、二項関係から生成される同値関係を構成的に定義し、それが本当に最小の同値関係になっていることを証明します。 また同値類を定義し、同値類と同値関係に関して成り立つ基本的な事柄に関して補足します。 二項関係から生成される関係 を任意の集合 上の二項関係であるとします。このとき、新しい 上の二項関係 を次のように定義します。 \begin{align*} \forall x,y
はじめに 私はホモロジー代数を以下の書籍で学びました。 絶賛絶版中で入手は困難ですが、現状でも日本語でホモロジー代数を勉強しようと思うと、この本一択になるのではないかと思います。 証明は自分で追える程度に十分に形式的に書かれていて、誤植などもほとんどなかったように記憶しています。 ホモロジー代数 (岩波基礎数学選書) 作者: 河田敬義出版社/メーカー: 岩波書店発売日: 1990/11/08メディア: 単行本 クリック: 4回この商品を含むブログを見る この本の第1章で direct limit ( と表す) という概念が出てきます。 そこで direct limit に関して成り立つ基本的な事実として、 任意の の元 に対して、或る十分大きな と が存在して、 が成り立つ 任意の の元 に対して、 となることと、十分に大きいある が存在して、 となることは同値である ということが、証明無
このページを最初にブックマークしてみませんか?
『俺の Colimit を越えてゆけ』の新着エントリーを見る
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く