今度は「自動修復で PC を修復できませんでした」というのが出ました。そこに書いてあるファイルと思われるものを見ると ブートの重要なファイル d:\efi\microsoft\boot\cipolicies\active\{cdd5cb55-db68-4d71-aa38-3df2b6473a52}.cip が壊れています。 と…

Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化という本のKindle版がなかったのでKinoppyで購入。Kinoppyは初めて使いました。PCでは字が小さくて読みにくいですがiPadの大きいのを持っているのでそっちではなんとか読めます。PC…

TeXからはてなブログに変換するツールを作ろうと思って、Visual StudioでPythonが使えるようなのでやってみましたが、正規表現のやり方が普通と違う感じになってしまいました。たぶん普通のやり方でもできるとは思うのですが、Pythonはよく知らないのでわか…

Windows10のノートPCを使っていたのですが、変な音がするようになったので、新しくWindows11のノートPCを購入しました。そのPCでこのブログを書いていたら、「デバイスに問題が発生したため、再起動する必要があります。エラー情報を収集しています。自動的…

ABC予想(1) まず「ABC予想 - Wikipedia」に従って定義を述べます。自然数 に対して、 の互いに異なる素因数の積を の根基 (radical) と呼び、 と書きます。自然数の組 で、 で、 と は互いに素であるものを abc-triple と呼びます。ABC予想(1) (『日本一わか…

このブログでは、「無限の項を持つ多項式のようなもの」(「無限論理多項式」と呼ぶことにします)を使って、サーバーで無限に実行されるプログラムとブラウザーで実行されるプログラムの組み合わせを表そうとしています。この「無限論理多項式」の定義につい…

一般マグマの多項式の完備化 環の演算では書き換え規則の合成を行っているので、今までの議論で説明できるのですが、その説明では長くなるのでいったん 群の完備化の説明をしたいと思います。群の完備化ではクヌース・ベンディックス完備化アルゴリズム - Wi…

一般マグマの多項式の等式の合成(2) 続いて単位元をもつマグマの準同型についても見ていきます。 単位元をもつマグマの準同型(1) 第1段階 等式の集合 \begin{cases} \mathrm{eq}_{1}: & x & \mapsto & e x & = & x \\ \mathrm{eq}_{2}: & x & \mapsto & x e'…

一般マグマの多項式の等式の合成(1) 書き換え規則 に対して、 とします。 を等式と考えます。これを と書くことにします。書き換え規則の合成を等式の合成に書き直すことができます。書き換え規則 、 に対して書き換え規則の集合の合成 を考えると、 となり…

一般マグマの多項式の書き換え規則の合成(2) 前回の説明で間違っているところがあったので訂正します。書き換え規則 に対して、 の部分項の位置 の部分項を 、 の部分項の位置 の部分項を とします。 の部分項の位置全体の集合を 、 の部分項の位置全体の集…

一般マグマの多項式の書き換え規則の合成 「環の演算」(これはスマートフォンで使えるように以前のものを少し書き直しました)での式の合成の説明をする準備ができました。これを説明する前に、まず書き換え規則の合成について考えます。ある代数的構造を等式…

一般マグマの多項式の単一化アルゴリズム(3) 前回の議論(「wikipedia:ユニフィケーション」の「一階の項」を参照)を『計算論理に基づく推論ソフトウェア論』の議論のように2段階に分けます。なお、前回の記事でも単一化アルゴリズムの中で項を変化させる場合…

このブログは、論理プログラミングを無限に実行する場合、実行順序を指定する機能を追加することを目的としています。現在は「無限の項書き換え」のような方法で記述する方法を検討しています。 エレファントな群とリー代数 項書き換えと同様の方法で群やリ…

一般マグマの多項式の単一化アルゴリズム(2) この項目の内容は「一階の項」の理論と内容は同じものになると思われます。書き方を変えることで極限や普遍性について考えるときに多項式の考え方が使えると思うのですが、今のところどうなるかわかりません。前…

一般マグマの多項式の単一化 環(および自然数の演算)(日本語が正しく表示されない可能性がありますがいつか書き直します)の使い方を説明すると書きましたが、ここで行っている「規則の合成」を説明するには単一化(ユニフィケーション)について説明する必要が…

環の性質(2) 任意の 項演算を任意の個数もつ代数的構造に対しても「±マグマ」と同様の議論が成り立ちます。これを「一般マグマ」と呼ぶことにします。「一般マグマ」によって環の性質を証明することができます。前回の続きを書いていきます。\begin{cases} \…

±マグマ 集合 が二項演算 と単項演算 を持つとき を±マグマと呼ぶことにします。「単項・二項マグマ」と呼んでいましたが長いのでこう呼ぶことにします。ここでは、マグマに関する議論に演算を付け加えたものをまとめて説明していきます。この議論に関する一…

環の性質 「群の性質」で考えた「単項・二項マグマ」に二項演算を付け加えたものを考えます。これをここでは「単項・二項・二項マグマ」と呼ぶことにします。「単項・二項・二項マグマ」について「代入」を考えることで「群の性質」と同様に環で成り立つ関係…

群の性質(2) 今回は群の性質の続きを調べていきます。 前回の結果 「エレファントな群とリー代数(3)」では書き換え規則の集合 \begin{cases} \rho_{1} & = & ( & x & \mapsto & e x & \to & x & ) \\ \rho_{2} & = & ( & x & \mapsto & x & \to & e x & ) \\…

単位元をもつマグマの準同型(1) を単位元 をもつマグマ、 を単位元 をもつマグマ、 をマグマの準同型とします。このとき ならば が成り立ちます。これを「マグマの左単位元・右単位元」と同様の方法で証明することができます。項を に属する項と に属する項…

群の性質 本[1][2]の中で「群の完備化」として、群の定義の一部から出発して完備な書き換え規則を得る手順が書かれています。こちらの私のサイト http://www2.biglobe.ne.jp/~optimist/algebra/word_2.html でもやっているのですが、本では有限回で終了して…

モノイドの左逆元・右逆元 をモノイド( は単位元)とします。 (L) に対して、 であるような を の左逆元と呼びます。 (R) に対して、 であるような を の右逆元と呼びます。 が左逆元 と右逆元 を持つならば、 となります。 [証明] (L)より (R)より よって結…

ここでは「項書き換え」のような方法で群、モノイド、半環やリー代数に関する証明を行ってみます。「項書き換え」については[1][2]の本を持っていたのですが見当たらないので、ウェブに同様の記事があったのでそれを参考にします。本来の「項書き換え」では…

随伴(3) 随伴の三角等式による定義 随伴の定義についても本に従って見ていきます。 随伴の三角等式による定義 定義 8.1 圏 、 間の関手 、 について、自然変換 、 が存在してこれらが三角等式を満たすとき、すなわち \begin{CD} F @> 1_F >> F \\ @V Fη VV @…

随伴(2) 積関手と冪関手 自由マグマと自由モノイドの関係を使って、随伴(の一部)を説明することができると思ったのですが、まだできていないし、随伴の全体を説明することは難しいと思われるので、また「圏論の道案内 ～矢印でえがく数学の世界～」の「第8章…

随伴(1) 自由マグマ まず基本になると思われる自由マグマから始めます。 マグマ 集合 が二項演算 を持つとき をマグマと呼びます。単に と表すこともあります。 部分マグマ をマグマとします。 に対して と書くことにします。 が を満たすとき は の への制…

トポス(1) この段階で数学的帰納法を使うことによって図式を使わずに説明することができるようになったと思うのですが、簡単にはいかないのでトポスについてもう少し調べてみたいと思います。[4]、[5]、[6]、[7]の本を持っていたので少し読んでみようと思い…

このブログは、論理プログラミングに実行順序を指定する機能を追加するため、現在は主に数学的帰納法や可換モノイドについてプログラミング言語で記述する方法を調査しています。 前回の中間報告以降更新したもの 代数的構造による圏論 ← 斜めの線を使わない…

第5章まで読めばろいろできると思われるのですが、数学的帰納法について考えるには第7章まで読んだほうが良いようなのでさらに引用していきます。そこまでは少し図式を描いていきます。 第6章 冪：プログラムの本質 ①冪 定義 6.1 (冪) 積を持つ圏 の対象 に…

⑦極限，余極限の定義 続いて極限と積などの関係を見ていきます。 積・余積 圏 を対象が の二つで、射が恒等射だけの圏とします。 と書くことにします。 型の図式(圏 から圏 への関手) に対する極限( の終対象)が存在するとします。、 とおきます。「 を圏 (…