随伴関手の説明をする前に自由群などについて説明をしておきます。 半群・モノイド・群の定義 集合 と結合律を満たす二項演算(積と呼びます) の組 半群と言います。単位元を持つ半群をモノイドと呼びます。モノイドが任意の元に対して逆元を持つとき群と呼び…

「環上の代数」、「環上の加群」に対応する半環のときの用語がないので、これらを「半環上のフラクタル代数」、「半環上のフラクタル加群」と呼ぶことにします。 「半環上のフラクタル代数」の「微分」を考えてそれに対する「極限」を考えます。 論理計算の…

論理プログラミングの説明でプログラムの実行を逆にたどると証明になるという説明をしようとしましたが、説明はなかなか難しいです。随伴関手の考え方で説明できるかもしれないと思いますので、説明できれば説明してみたいと思います。

関数プログラミングで無限に行われる入出力を書くときにどこに書くのかというだいたいの説明はできたのですが、厳密な説明ではないところが多いのでちゃんと説明できているのかはまだよくわかりません。この点をはっきりさせるために関数プログラミングでも…

PLP の項 が という形のとき という PLP の節があって、この節で変換されるものとします。 同様に PLP の項 が という形のとき という PLP の節があって、この節で変換されるものとします。 PLP の項 が という形のとき としたいのですが に が現れても良い…

関数プログラミングと論理プログラミングを対応させることによって、入出力が無限に実行されるプログラムをどのように書けば良いのかを考えていきます。関数プログラミングで無限に続く入出力を書く方法を考える必要はあるのですが、それを記述する言葉がな…

PLPとPrologの違いについて説明していきます。Prologのプログラムは論理式として見ることもできるのですが、実行する順序が決まっていて、プログラムとして実行することができるようになっています。これを説明するためPrologの単一化(unification)について…

逆に という形の列(各 は という形の論理式)を証明する証明図(*)が存在するとします。 という論理式を とおきます。 を 個並べた列を と書くことにします。 「シークエント計算」についてはほとんど説明していないし、詳しく知っているわけでもないので以下…

のときに成り立つとして のときに成り立つことを証明していきます。 のときに証明図を書くことができると仮定します。 のときの PLP の正規化された論理式 は という形になります。上についた は変数を何回か置き換えたものであることを表しています。 は の…

PLP のプログラムが成功するとき、論理式として見ると証明図を書くことができることを帰納法で証明していきます。 となる に関する帰納法で証明します。 から始めます。PLP のプログラムは1個の述語式から始めると定義したので、 のときは書くことができませ…

ここでは は単に項 と が一致するとき true 、そうではないとき false となるものとします。 を述語式で表す方法については後で述べる予定です。Prolog の単一化についても後で述べる予定です。 プログラムが成功するときは、論理式として見ると証明図を書く…

PLP のデータとなる項を定義します。 記号の有限集合 があってその元を定数と呼びます。定数は項となります。 記号の可算集合 があってその元を変数と呼びます。変数は項となります。 記号の有限集合 があってその元を関数と呼びます。関数 に対して という…

以下(からまでの議論)を見てみます。 を証明するには 、、、、…のすべてを証明するか、または 、、、、…のすべてを証明するか、または 、、、、…のすべてを証明するか、または… 、、、、…のすべてを証明すれば十分ということがわかります。 ここで は述語式 …

PLP のプログラムは形としてはPrologのプログラムで、実行順序のないものとします(以下で少しずつどういうことか説明していきます)。PLPのプログラムは論理的には という論理式と考えることができます。ここで は という形の式とします。 は述語、各 は項ま…

PLP の述語 集合 (述語の項を表す)とブール代数 (PLPの結果の成功または失敗を表す)に対して を(項の)述語と呼びます。 これを拡張して可算集合 (変数を表す)に対して としたものも述語と呼びます。 有限個の述語の集合を とおきます。 の各元 に対して とい…

半環の定義 集合 に2つの二項演算、加法 と乗法 が定義されていて、加法に関しては可換なモノイド、乗法に関してはモノイドで、乗法が加法に対して分配法則を満たすとき、 は半環であると言います。乗法が可換であるとき は可換であると言います。加法が冪等…

Prologのプログラムでは否定を扱うことができないため、Prologのデータは分配的な束と考えることができます。これは可換な冪等半環で加法に関しても乗法に関しても分配的なものと考えることができます。 ここでは PLP のデータをまず半環として数学的に定義…

実行順序を考えない論理プログラミングを PLP と書くことにします。(ピュア論理プログラミングの意味。以前の記事で CLP (並行論理プログラミングの意味)と書いていましたがわかりにくいので変更) この PLP を代数的に、半環を使って定義します。半環を使う…

はてなブログに移行してから何も書いていないようなので何か書いてみようと思っています。 Optimistic Mathematicsのサイトで書いていた数学とコンピューティングに関する記事を更新するために考えたことなどを書いてみたいと思います。Prologを実行できるよ…