下方向が証明図の方向になるように書き直しました。前回の例で考えると が成り立てば良いので とすれば良いということになります。 を満たす を考えます。「 を 項から 項に切り詰めたもの」は となります。 からなる射影系の射影的極限を証明図の極限と考え…

に対応する で決まる証明図の逆方向の写像を とします。 を と定義します。これは証明図の逆方向の写像となります。 を と定義します。これは証明図の方向の写像となります。 を を満たすものとします。 として を の元 に変換する(切り詰める)ことを考えま…

証明図を遡る説明のとき、成功の場合を含めるのか含めないのか明言していませんでしたが、実質は証明が成功でも失敗でもないときの極限となっていました。証明図の極限を考えることが目的だったのですが、証明図が書けないときの極限になっているというので…

証明図の逆方向の極限 シークエント計算 LK の と の証明図のパターンを下から上にたどると、変数のところは推論が成立するような項で置き換えられれば良いということがわかります。すべての項について調べれば良いのですが証明図には一つの項しか書けないの…

以前説明したものの繰り返しになるのですが、もう少し詳しく説明したいと思います。その前に以前シークエント計算の説明をしたときに変数の説明が抜けていたようなので、これも以前の繰り返しになりますが説明したいと思います。 論理プログラミング まず論…

論理プログラミングが成功となるのは一つの積に対して成功すれば良いので、以前の説明は合っていたようです。もう少し詳しく説明しないといけないようです。

前回変数を含まない項を変数を含まない写像で証明図の方向の逆の方向へ写すということを考えましたが、この写像は変数を含む場合は一つの写像で良いのですが、変数を含まない場合は項(積の項)ごとに別々の写像が必要であるため、前回の説明は間違っていたよ…

論理プログラミングのプログラムが成功したとき、変数は変数を含まない項に置き換えられるのが普通です。したがって成功したときの場合を考えると、変数の代わりにすべての変数を含まない項について調べれば良いということになります。 を「シークエント」全…

を集合(本来は「シークエント」全体の集合)、 で自由生成された代数系(本来は分配束)全体の集合を とおきます(Wikipediaによると代数的構造を持つ集合は代数系と呼びます)。 は本来は分配束なのですが、可換冪等半環、可換半環、可換環の場合も考えていきま…

対角関手 (Wikipediaを参照) 対角関手の定義 圏 と に関して対角関手 は以下のようなものとなります。 圏 の対象 に対して は の対象となります。これは以下のような関手 となります。 の対象に対しては の対象 を対応させる。 の射に対しては の恒等射 を対…

論理プログラミングの「極限」は逆像として表すことができることがわかりましたが、逆像は「引き戻し」として表すことができるようです。「引き戻し」は「極限」で表すことができるのでここから考えていきます。環の理論を使ってクライアント側の関数プログ…

論理プログラミングとシークエント計算の関係について以前書いていましたが、まとめてみます。論理プログラミングで述語式の列(ゴール節) を実行するには、、、…、 をすべて(Prologの場合は順に)実行することになります。これは証明図で書くと以下のようにな…

集合 の1個以上有限個の元からなる集合の全体を とおきます。 は和集合を演算とすることにより集合 によって自由生成された自由冪等可換半群と考えることができます。集合 によって自由生成された自由半群 (演算を のように書くことにします)とし、 によって…

半環について考える前に、半群についてもう少し考えてみます。集合 によって自由生成された自由半群 は の元からなる1個以上有限個の文字列の全体として定義することができます。集合 によって自由生成された自由モノイド は の元からなる0個以上有限個の文…

普遍射の定義 (Wikipediaによる) と を圏、 を関手、 を の対象とするとき、 から への普遍射 とは、以下を満たす の対象 と のことを言います： の対象 と に対して が一意的に存在して を満たす。 可換図式で書くと以下のようになりますが斜めの線が書けな…