エレファント・コンピューティング調査報告

極限に関する順序を論理プログラミングの手法を使って指定することを目指すブロクです。

関数プログラミングと無限論理多項式(2)

今回は3の平方根を1桁ずつ計算するC#の例をJavaScriptで書き直したものを考えます。 JavaScript の例 以下のコードのクラス Numbers の関数 GetNextDecimalDigit() で1桁分の処理を行っています。LongDecimal は小数点以下の任意の桁数を計算することができ…

関数プログラミングと無限論理多項式(1)

この記事では、サーバーで無限に実行されるプログラムとブラウザーで実行されるプログラムを組み合わせたものを記述する方法について考えていきます。まずC#のイテレーターで考えてみます。今後はHaskellなどのプログラミング言語とも比較していきたいと思い…

現状報告(4)

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

現状報告(3)

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

現状報告(2)

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

現状報告(1)

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

ABC予想と無限論理多項式(1)

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

中間報告(8)

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

エレファントな群とリー代数(16)

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

エレファントな群とリー代数(15)

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

エレファントな群とリー代数(14)

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

エレファントな群とリー代数(13)

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

エレファントな群とリー代数(12)

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

エレファントな群とリー代数(11)

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

中間報告(7)

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

エレファントな群とリー代数(10)

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

エレファントな群とリー代数(9)

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

エレファントな群とリー代数(8)

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

エレファントな群とリー代数(7)

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

エレファントな群とリー代数(6)

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

エレファントな群とリー代数(5)

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

エレファントな群とリー代数(4)

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

エレファントな群とリー代数(3)

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

エレファントな群とリー代数(2)

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

エレファントな群とリー代数(1)

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

代数的構造による圏論(12)

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

代数的構造による圏論(11)

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

代数的構造による圏論(10)

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

代数的構造による圏論(9)

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

中間報告(6)

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