-
- いいね！0
ぼんてんぴょん(Bontenpøn)
@y_bonten
こんなふうに、各種の抽象のルールには、実際に証明を書き換える際にショートカット可能な状況がきちんと対応している。ここを押さえずにルールだけふんふんと眺めても、なぁーんにも面白くない。
2019-04-22 14:30:42
ぼんてんぴょん(Bontenpøn)
@y_bonten
現代数理論理学序説、ちょっと戻るけど、定理1.2.10の証明（問題1.2.11）。抽象λ*ではMがatomだろうがapplicationだろうが、xが出現していなかったらルール1を適用する。だからと言って出現している場合だけ切り分けて帰納法を回すわけにはいかない。
2019-04-23 08:22:40
ぼんてんぴょん(Bontenpøn)
@y_bonten
M=UVにはxが出現していても、UとVの両方にxが出現するとは限らないからだ。それぞれ場合分けするしか仕方なさそうだね。
2019-04-23 08:22:41
ぼんてんぴょん(Bontenpøn)
@y_bonten
『現代数理論理学序説』p18〜p19、抽象t。もはや見たことのない結合子が出てくる。確かB'だけはCBと定義されていたな、と思ったが、B'xyzが正規形を持ったはず。ところがB'の公理はB'MNRU>_1 MN(RU)になってる。後ろに４つも取るんかい。 俺の知ってるB'とちがう！ と諦めそうになったが、
2019-04-27 12:56:36
ぼんてんぴょん(Bontenpøn)
@y_bonten
CLｗの公理から、結合子に対応する公理型を復元できないものだろうか。今までやったことなかったな…と思って考えてみたら、ちゃんとできるじゃないか。B'は(δ→(β→γ))→(δ→((α→β)→(α→γ)))という公理型のようだ。これは確か問1.2.5(8)（補充問題）でコメントした、BBとか(SK)Bで書けるアレだ。
2019-04-27 12:56:36
ぼんてんぴょん(Bontenpøn)
@y_bonten
せっかくなのでK',B',C',S'の公理型を全部調べたった。α→(β→γ)のα,β,γのうちのいくつかに「δ→」を付加する公理ばかりだ。γには必ず付加するが、あとαとβに付加するかどうかで2×2の公理がある。完全にリバースエンジニアリングだな……
2019-04-27 20:11:04
ぼんてんぴょん(Bontenpøn)
@y_bonten
抽象tの定義には「Mが閉項のとき」というものが新たに登場する。この閉項は、すぐあとのp20で出てくるラムダ項の閉項ではなく、p4の「変数を含まない」という定義のほうだろうと思う。しかし、なんで閉項でないといけない（他の文字も含んではいけない）のだろう？？
2019-04-28 08:38:39
ぼんてんぴょん(Bontenpøn)
@y_bonten
例えば何度も例に上がっているλy.xyyに対して、抽象tの5.を適用してはいけない理由が何も思いつかない。これはx:α→(α→β)にS'を作用させて(α→α)→((α→α)→(α→β))に変えておき、I:α→αを2回当ててS'xII:α→βを得る書き換えに相当する。何も問題ないような気がする。
2019-04-28 08:38:40
ぼんてんぴょん(Bontenpøn)
@y_bonten
現代数理論理学序説p62例えば∀v_1[p(v_0)→∀v_2[q(v_1,v_2)]] のv_0に項を代入したいとき、その項がv_1を持っていたら、代入箇所がv_1の束縛スコープ内にあるために前処理が必要となる。v_1をほかの変数に取り換えないといけないが、この取り換え自体が代入のアルゴリズムで定義できるのが面白い。
2019-07-03 10:41:18
ぼんてんぴょん(Bontenpøn)
@y_bonten
このとき新たな衝突を事前に避けたければ、v_1をv_3などに取り換えればよい。もしもv_2に取り換えてしまうと、後でまた衝突する。全く個人的な好みだが、再帰的定義は「どんどんケツを回すことが本質」みたいな所があるので、先の論理式まで見て変数を選ぶより玉突き事故を起こすほうが美しく感じる。
2019-07-03 10:41:19
ぼんてんぴょん(Bontenpøn)
@y_bonten
α変換がガンガン行なわれることを我慢すれば、[t/x]∀yβの定義は [t/x]∀yβ≡∀z[t/x][z/y]β ただしzはtに現れずxでもない変数のうちの最初のもの。 で済むのではないだろうか。xとyが同じ変数であっても、yは別の変数zに張り替えられているので代入されない。
2019-07-04 16:40:19
ぼんてんぴょん(Bontenpøn)
@y_bonten
これでバグらないことを保証するためには、うまくいく例をいくら挙げたってダメなのだ。いろんな例で理解を深めつつ、「論理的に」なっとくしないといけない。他人のプログラミングに対していつも偉そうに言ってることが自分に跳ね返ってきた。
2019-07-04 17:30:45
ぼんてんぴょん(Bontenpøn)
@y_bonten
いろんな例を試すうちに気づいたこと：p(x)→∀x[q(x)]のようにxが自由・束縛の両方で出現してもよく、両者のxは無関係、というのはよく言われることだが、その全体に∀xをつけて∀x[p(x)→∀x[q(x)]]としても構わない。
2019-07-04 20:32:17
ぼんてんぴょん(Bontenpøn)
@y_bonten
現代数理論理学序説、間が空いてしまったので最初から読み直した。引っ掛かりを覚えた箇所をメモ。p4「S,K以外の定数を含まない閉項を結合子といいます」；この時点では定数はS,Kしか導入されていないので、結合子でない閉項が存在しない。
2019-07-08 05:35:10
ぼんてんぴょん(Bontenpøn)
@y_bonten
あとでI,B,Cなどが導入されるが、本質的には略記なので、これらが含まれるから結合子でないということにはならないだろう。P,Aが含まれたらどうなるのかは書いてない。
2019-07-08 05:35:11
ぼんてんぴょん(Bontenpøn)
@y_bonten
p5、メタ式と式の関係を式n+3と数n+3との関係に喩えている箇所；「式」が両方に登場して痛恨だが、n+3のほうを「メタ数」と「数」とでも言い換えると少しは理解しやすい。それでもなお、次頁の註のような微妙な違いがあるが、「メタ式／式」のほうも「メタ記号列／記号列」とか言い換えればいいか。
2019-07-08 05:35:11
ぼんてんぴょん(Bontenpøn)
@y_bonten
今更だが、メタ変数やI,B,Cなどの結合子の略記については、代入したり書き下したりする際に本来は最外括弧が付いていることを忘れてはならない。例えばW≡SS(KI)≡SS(K(SKK))である。結合子の略記は頭に置かれることが多いせいで括弧が省略されるために認識が遅れてしまった。
2019-07-08 05:35:11
ぼんてんぴょん(Bontenpøn)
@y_bonten
さんざん悩んだまま結論を書いていなかった|>_1と|>の違い； ・M|>_1w Nは、公理S,Kのインスタンスに尾頭を有限回（ゼロ回でもよい）つければM|>_1 Nが得られる、という意味。 ・M\>_w Nは有限個（ゼロ個でもよい）の|>_1でMとNを繋ぐことができる、という意味。
2019-07-08 05:51:53
ぼんてんぴょん(Bontenpøn)
@y_bonten
w-正規形はこれ以上|>_1で変形を繋ぐことができない終着点であり、Mを>_1で変形していってNが得られて（M|>_w N）しかもNが正規形のとき「NはMの正規形」という。つまりNはMを変形し尽くした形。
2019-07-08 05:51:54
ぼんてんぴょん(Bontenpøn)
@y_bonten
ここで当初から「どんな順番で変形を行っても、結局同じ正規形に行き着くのか？」という疑問を持っていたが、定理1.1.7Church-Rosserの定理（証明は扱わない）により、正規形が一意であることは言える。同じ項からスタートして「これ以上変形できない」ものが複数あったら定理に矛盾する。
2019-07-08 05:51:54
ぼんてんぴょん(Bontenpøn)
@y_bonten
ただし、「正規形が必ず存在する」ことを言うのは難しいと思う（何か見落としているかも）。「変形は必ず項を短くする」という保証があるなら良いが、そうでもないらしいので、ループしていつまでも停まらない可能性は否定できない。
2019-07-08 05:51:54