-
- いいね！0
ぼんてんぴょん(Bontenpøn)
@y_bonten
しかし「無駄にMPを消費している」とか言ってると本当にゲーミングマインドに没入してくるな #数理論理学やってます
2019-04-11 15:11:29
ぼんてんぴょん(Bontenpøn)
@y_bonten
SKKとかS(KS)Kとかを見ても、そこまでに使った公理の履歴は辿れるが、メタ文字にどんな式を入れたのかまでは分からない。けれども、SKKならSKKという証明が成立している以上、入れるものはこんな形をしていないといけない、という制約が生じる。これが証明のリファクタリングのパターンを与えてくれる
2019-04-11 15:18:18
ぼんてんぴょん(Bontenpøn)
@y_bonten
『現代数理論理学序説』の解答例等でM>N ├ QMR>QNRを当然のように使ってたけど、「>1」なら問題ないが「>」はぜんぜん明らかではないんじゃないか。
2019-04-12 12:19:51
ぼんてんぴょん(Bontenpøn)
@y_bonten
これも許容規則だな。M>Nが得られているなら、Mから0個以上の>1でNまで繋がっていて、N>Nから後ろ向きに(τ)を順次適用しているはず。適用前の個々の式に尾頭をつけて(τ)を適用し直せばOK。
2019-04-12 16:53:57
ぼんてんぴょん(Bontenpøn)
@y_bonten
これだけのことを考えないと解答例の式変形が正当化できないの、いくらなんでもスパルタ過ぎないか。ゼミの院生さんたちはクリアしてるんだな。こわ。
2019-04-12 16:57:48
ぼんてんぴょん(Bontenpøn)
@y_bonten
そうか、これも Bx≡S(KS)Kx->KSx(Kx)->S(Kx)という簡約に相当するわけだな。くっ、俺が喜んで証明を簡略化する作業を尻目に、コンビネータはすべて先回りして結果を知ってやがる……
2019-04-15 22:16:19
ぼんてんぴょん(Bontenpøn)
@y_bonten
こっちも負けてない。主部のCL項だけを頼りに、述部の論理式を再現できる能力を身に着けてしまった。超楽しいパズルになっている。
2019-04-15 22:19:42
ぼんてんぴょん(Bontenpøn)
@y_bonten
現代数理論理学序説、演繹定理。具体例として、x:α→(α→β)とy:αを仮定とし、MP2回でxyy:βを得る証明がある。これを演繹定理で書き換え、仮定αを解消してα→βの証明を構成してみる。基本的な考え方は、上から順番に証明図中のすべての論理式の頭にα→をつけたものを順次証明してゆく、というもの。
2019-04-17 20:51:51
ぼんてんぴょん(Bontenpøn)
@y_bonten
まず、x:α→(α→β)は解消しなくてよいのでKで水増ししてKx:α→(α→(α→β))。いっぽう、解消したい仮定αに対しては、Iで（無仮定のもと）I:α→αを得る。これと、さきほどのKをSで振り分けたS(Kx):(α→α)→(α→(α→β))とでMPすれば、S(Kx):α→(α→β)を得る。
2019-04-17 20:51:51
ぼんてんぴょん(Bontenpøn)
@y_bonten
もとに戻ってしまって無駄に見えるが（実際に無駄なんだが）、これはもとの証明のxy:α→βの頭に「α→」をつけたものにほかならない。さらにSで振り分けてIとともにMPすれはα→βを得る。
2019-04-17 20:51:52
ぼんてんぴょん(Bontenpøn)
@y_bonten
具体的な手順とλの再帰的定義を見返すと、きわめてコンパクトに構成手順を与えてくれていることが分かる。そして、公理Sはもはや演繹定理のためにあるような公理だという感慨も覚える。
2019-04-17 20:51:52
ぼんてんぴょん(Bontenpøn)
@y_bonten
さて、せっかく演繹定理で構成し直した証明の末尾に、解消した仮定を作用させて再びMPしてやれば、もとの証明と同じ結論が得られる。つまり演繹定理は仮定の解消にも使えるけれども、解消しなくてもいいから「最後にまとめて一度ずつ使いたい」というニーズに応えてくれる。
2019-04-18 13:25:11
ぼんてんぴょん(Bontenpøn)
@y_bonten
問題1.2.9はまさにそういう話であって、カラクリが分かっていたら計算しなくても結果がxyy（もとの証明の結論）になることは分からないといけなかったのだ。今なら分かる！そしてそれを一般化したのが定理1.2.10だ。
2019-04-18 13:28:55
ぼんてんぴょん(Bontenpøn)
@y_bonten
yは最後まで手をつけず、まずxまでで変形し尽くしてから計算すると見通しがいい。 S(S(KS)(S(S(KS)(S(KK)I))(KI)))(KI)x ->S(KS)(S(S(KS)(S(KK)I))(KI))x(KIx) ->KSx(S(S(KS)(S(KK)I))(KI)x)I ->S(S(KS)(S(KK)I)x(KIx))I ->S(KSx(S(KK)Ix)I)I ->S(S(KKx(Ix))I)I ->S(S(Kx)I)I これはλ*y.xyyそのもの。
2019-04-20 11:24:44
ぼんてんぴょん(Bontenpøn)
@y_bonten
改めて S(S(Kx)I)Iy ->S(Kx)Iy(Iy) ->Kxy(Iy)y ->xyyとなる。 これで(λ*xy.M)xy->(λ*y.M)y->Mの具体例を順々に見ることができた。λを再帰的定義で展開していく過程と、後ろにxやyをつけて簡約していく過程が完璧に対応している。
2019-04-20 11:24:44
ぼんてんぴょん(Bontenpøn)
@y_bonten
こういうのを誰かに教える機会があったとして、自分の悟ったことをいくら声高に強調しても、相手が同じように泥臭く手を動かして対象にfamiliarになってくれないと何も共有できないのがもどかしいところ。
2019-04-20 11:26:40
ぼんてんぴょん(Bontenpøn)
@y_bonten
数理論理学序説、抽象η（エータ）。ちょっと今まで演繹定理の理解で大事なことが抜けていた。もとの証明の論理式の頭に「解消したい仮定→」を付けたものを再帰的に構成していく、と言ってきたが、なんの制約も無いなら最後の結論にKで水増しすりゃあいい話。
2019-04-22 14:01:12
ぼんてんぴょん(Bontenpøn)
@y_bonten
しかしそれでは一般には主部に仮定の論理式の主部が含まれたまま残ってしまう。だから苦労して遡っていくわけだ。しかしどんどん遡って、主部にもはや仮定の主部が含まれなくなったら（つまりその仮定のもとを離れたら）、もうそれ以上頑張る必要はなく、Kで水増しすればいい。それが抽象λ*のルール1。
2019-04-22 14:03:52
ぼんてんぴょん(Bontenpøn)
@y_bonten
だから、xyyのyを解消する例で、もとの証明にα→βがすでにあるのにわざわざ作り直すのは、α→βの主部xyにyが含まれているから無駄ではないのである。いっぽう、x:α→(α→β)があるのに、わざわざα→βの頭にα→を水増しするのは、こっちは正真正銘の無駄。
2019-04-22 14:08:18
ぼんてんぴょん(Bontenpøn)
@y_bonten
xとyからMPできるということは、xがすでに「y→●」という形をしているということ。そのxがyに依存せずに得られているのなら、面倒なことをしなくてもxをそのまま降ろして来れば済む話。そういうショートカットを与えてくれるのが、抽象ηのルール3だ。
2019-04-22 14:10:46
ぼんてんぴょん(Bontenpøn)
@y_bonten
抽象iのルール4は、xがUに登場しなければ、ルール4がなくてもルール6と1によってS(KU)となる運命にある。S(KU)もBUも同じことだから（サラっと書いたが要確認）、先にまとめてやっちゃえ、ということか。
2019-04-22 14:18:01
ぼんてんぴょん(Bontenpøn)
@y_bonten
抽象iの5はなんだろうな。Cはα→(β→γ)のαとβの順番を入れ替えてくれるんだったな。UとVでMPできるということはUは「V→●」の形で、それに「x→」を水増ししてCしたらV→(x→●)になると。するとV（xに依存しない）をそのまま持ってきてMPすればx→●が得られる。
2019-04-22 14:28:07
ぼんてんぴょん(Bontenpøn)
@y_bonten
誤植でVの右に閉じ括弧が余分についているが、優先順位は(C(λ^i y.U))Vでいいんだな。理解していないと直せない誤植で、我々は試されている！
2019-04-22 14:29:35