#いい加減自分らが一体なにがしたいのかまとまったんすか。正当性検証からもどんどんはずれているんすけど。
#いつまでたっても話が噛み合わん。
#rahAloe さん : ここでは参加者が興味をもっている対象（おもに Haskell に関係ある）について議論する場所で、必ずしも一つだけのトピックについてのみ会話するのではなく、ときにはトピックが複数入り交じります
#今の話題は、僕が理解している限りは、「プログラミング言語の基礎概念」の Nat 推論の自動導出をどう書くかということです
#rahAloe さんがわからないことについて、ここでより深く質問することは自由ですし、むしろ僕は歓迎いたします
#つまり、現在の話題「自動導出」以外の話題を並行して行うことも可能だということです
#まったりといきましょう
##これのswap-plusなんですが
##このswap-plus自体はcase splitは指定したけどそれ以外は全て自動証明に任せたものです.
#なのですが良く理解できないので教えてください
#swap-plus自体は直感的には n1+(n2+n3)=n2+(n1+n3)を証明しようとしています
#場合分けとしては 1. n2 が Z の時, 2. n2は S ? で n1 が Z の時, 3. n1 n2 ともにZではない時
#に対応していると思いますが,3番目のケースが何を意味しているのかが良く分からない
#これどう読み取ればいいんでしょう?
#この規則自体はn1やn2がZでなかったとしても、n6を構成できて、相応の証明を提示できるものと思って始めたのですが
#矛盾からの証明になっていて、これが一体どういうことを意味してるの？というところで立ち止まってる
#例えば具体的に言えば n1=1, n2=2, n3=3 の場合なんかがこの3番目のケースにあたると思うのですが、
#その場合この証明は何を意味しますかね?
#swap-plus : ∀ {n₁ n₂ n₃ n₄ n₅} → n₂ plus n₃ is n₄ → n₁ plus n₄ is n₅ →
∃ λ n₆ → n₁ plus n₃ is n₆ → n₂ plus n₆ is n₅#確認ですが，この型シグネチャーの意味は「任意の n₁ n₂ n₃ n₄ n₅ について，n₂ plus n₃ is n₄ および n₁ plus n₄ is n₅ が成り立てば，ある n₆ が存在して， n₁ plus n₃ is n₆ ならば n₂ plus n₆ is n₅ である」でいいですか？
#です
#だとすると，3つめの場合は，n₆ を Z としたとき，n₁ plus n₃ is n₆ → n₂ plus n₆ is n₅ は矛盾するということですよね．
#うむ
#ただn6は任意のではなく存在なのでZで矛盾するからと言って、それがどうした？と思いません？
#Zが入っているn6の構成のところは、見つかれば埋めてくれますが、見つからなければ solution not foundであきらめてくれるので
#その場合はこちらで教えてやるかしないとダメなのだと思っています
#それがAgdaさんが自動で引っぱりだしてきたもんだから、何がどうなってそうなってる？と思ってるところ
#solution not found じゃないのかという疑問ですか？
#いえ、そうではなく
#いろいろだなー
#なにが疑問？
#そもそもこのケースでn6構成できないの？
#いや構成したじゃん．Z
#それ矛盾してますし
#矛盾してても，n₁ plus n₃ is n₆ → n₂ plus n₆ is n₅ だよね
#いや、ちょっとまって
#はい．
#まずn6はforallではないわけだから
#どんなn6でも成り立つわけじゃない
#ということはそら成り立たないケースもってくればそうなりますよね
#そういう場合を取り上げて矛盾からの真を出して証明になるものなのですか？
#それありだったら何でも証明できそうな気がする
#∃ 系なもの全般で
#矛盾のない n₁ plus n₃ is n₆ → n₂ plus n₆ is n₅ を得たいとは言われてないよ．< Agda の言い分
#たぶん．
#えーっと
#n1=1,n2=2,n3=3だったとします
#はい．
#n6は4として具体的に構成できますよね
#矛盾を持ち出さなくても
#n1=2,n2=2,n3=2の場合も構成できますね
#その場合，4 を構成すれば，矛盾のない表明になるということですよね．
#そうそう
#0を構成したから，矛盾になったんだよね．
#というか、n6は別にforallじゃないんだから当然でしょ＞
#そういうダメなものを出しても、だからなに？では？
#だから，n6 を構成するのに，後の表明を使ってないんですよ．
#closure-propertyでしたっけ、閉じている」
#あ、誤爆
#あとの表明とは？
#n6 を含む表明
#？
#後の表明というのは ∃ λ n₆ → n₁ plus n₃ is n₆ → n₂ plus n₆ is n₅ ？
#これが Z , (λ ())では?
#n6 = Zとしている
#n6を構成するのに後の表明を使ってないという意味をもっと詳しく
#n1=1,n2=2,n3=3 と n₂ plus n₃ is n₄ と n₁ plus n₄ is n₅ から n6 は構成できないですよね．
#いや、存在なのでそれから構成できなくても良くて、見つけてもいいんですよね？
#0 を見つけました．
#じゃあ
#閉じているというのありますよね
#任意のn1とn2にたいして
#n1 plus n2 is n3となるn3が存在する
#はい．
#こいつもn1とn2がともにZでない場合、n3=Zを見つけて矛盾するから証明おっけー＞
#そうなりますか？
#それはどのような型ですか？
#closure-plusがそうです
#closure-plus : ∀ {n₁ n₂} → ∃ λ n₃ → n₁ plus n₂ is n₃
#ああ．たぶん，証明を自動生成させればそうなると思いますが．．．
#んー、これはそう簡単に自動証明できなくて
#仕方なく結構書きました
#ですし
#ならないかも，
#そもそも直感的には、そういうのが証明でOKなら存在系は間違っているものでも何でも証明できてしまいません？
#述語になってないから，矛盾述語はでてこないかも．
#間違ってないからですよ．
#述語とは？
#〜ならば××
#じゃあですね
#はい．
#swap-plus : ∀ {n₁ n₂ n₃ n₄ n₅} → n₂ plus n₃ is n₄ → n₁ plus n₄ is n₅ →
∃ λ n₆ → n₁ plus n₁ is n₆ → n₂ plus n₆ is n₅#これどうです？
#後の部分を少し書き換えました
#任意のn1,n2,n3についてn1+(n2+n3)=n2+(n1+n1)となる
#まぁ任意なのでそらダメだろと思いますが
#さっきのnobsunの理屈であれば
#n1とn2がともにZでないばあいn1 plus n1 is n6はn6がZのとき矛盾するから真になって、このヘンテコ規則が証明できてしまいませんか？
#どんな規則
#swap-plus : ∀ {n₁ n₂ n₃ n₄ n₅} → n₂ plus n₃ is n₄ → n₁ plus n₄ is n₅ →
∃ λ n₆ → n₁ plus n₁ is n₆ → n₂ plus n₆ is n₅#あれ？同じだ
#swap-plus2 : ∀ {n₁ n₂ n₃ n₄ n₅} → n₂ plus n₃ is n₄ → n₁ plus n₄ is n₅ →
∃ λ n₆ → n₁ plus n₁ is n₆ → n₂ plus n₆ is n₅
swap-plus2 {n₅ = n₅} P-Zero p₂ = n₅ , (λ x → P-Zero)
swap-plus2 {n₃ = n₃} (P-Succ p₁) P-Zero = n₃ , (λ x₁ → P-Succ p₁)
swap-plus2 (P-Succ p₁) (P-Succ p₂) = Z , (λ ())#これ意味的には 「任意のn1,n2,n3についてn1+(n2+n3)==n2+(n1+n1)」ではないの？
#ますます分からなくなってきた
#この場合swap-plus2 (P-Succ p₁) (P-Succ p₂)で得られるのは n6 と n₁ plus n₁ is n₆ → n₂ plus n₆ is n₅ 型の述語．という理解でよい？
#↑単なる確認です．
#右辺のことですよね？
#はい．
#n6とλ n₆ → n₁ plus n₁ is n₆ → n₂ plus n₆ is n₅な感じ？
#あ
#いえ、nobsunのであってる
#n6とn₁ plus n₁ is n₆ → n₂ plus n₆ is n₅のProductです
#λ()の型はn₁ plus n₁ is n₆ → n₂ plus n₆ is n₅で，正しいですか？
#その部分です
#正しいと思うのですが．
#まず、
#これ意味的には 「任意のn1,n2,n3についてn1+(n2+n3)==n2+(n1+n1)」ではないの？
#Yes?No?
#NO
#ちがうの？
#その意味にしたければ多分，
#swap-plus : ∀ {n₁ n₂ n₃ n₄ n₅} → n₂ plus n₃ is n₄ → n₁ plus n₄ is n₅ →
∃ λ n₆ → (n₁ plus n₁ is n₆ , n₂ plus n₆ is n₅)
とすべきかなぁと思います．#ということは
#associativity-plusも間違ってる?
#つかuniqueness-plusなんかもアウト？
#それ連言てことですよね？
#そうです．
#定理2.2は
#uniqueness-plus : ∀ {n₁ n₂ n₃ n₄} → n₁ plus n₂ is n₃ → n₁ plus n₂ is n₄ → n₃ ≡ n₄
#ではなく
#uniqueness-plus : ∀ {n₁ n₂ n₃ n₄} → ∑ (n₁ plus n₂ is n₃) (n₁ plus n₂ is n₄) → n₃ ≡ n₄
#こう？
#uniqueness-plus はそのままでいいと思うけど． (Σわかない)
#_,_は値の構成でΣ A (A -> B)が型なので
#そう書いただけです
#カリー化すれば同じことだよね．
#なにとなにが？
#n₁ plus n₂ is n₃ → n₁ plus n₂ is n₄ → n₃ ≡ n₄
#と
#(n₁ plus n₂ is n₃ ， n₁ plus n₂ is n₄) → n₃ ≡ n₄
#そうおもったけど、→が右結合だから違うのかもしれないと思いはじめてる
#(n₁ plus n₂ is n₃ ， n₁ plus n₂ is n₄ → n₃ ≡ n₄)となるが故に
#右結合だからそうならない．
#(n₁ plus n₂ is n₃ ， n₁ plus n₂ is n₄) → n₃ ≡ n₄とは違うということかと
#n₁ plus n₂ is n₃ → n₁ plus n₂ is n₄ → n₃ ≡ n₄
#は
#n₁ plus n₂ is n₃ → (n₁ plus n₂ is n₄ → n₃ ≡ n₄)
#でしょ？
#そうだよ．
#A -> BというのをA , Bと同じだといっているのではないの？
#カリー化は (a,b) -> c を a -> (b -> c)にすることだよ
#あう
#です
#では
#swap-plusはもしかして
#swap-plus : ∀ {n₁ n₂ n₃ n₄ n₅} → ∑ (n₂ plus n₃ is n₄) (n₁ plus n₄ is n₅) →
∃ λ n₆ → ∑ (n₁ plus n₃ is n₆, n₂ plus n₆ is n₅)#あーしまった
#swap-plus : ∀ {n₁ n₂ n₃ n₄ n₅} → ∑ (n₂ plus n₃ is n₄) (n₁ plus n₄ is n₅) →
∃ λ n₆ → ∑ (n₁ plus n₃ is n₆) (n₂ plus n₆ is n₅)#こうだ
#これでもOK
#Σを連言につかうの？Agdaでは？
#uniqueness-plusはその後にn==mがあるから→のままでもいいってことね？
#そうでぇす．
#というか今_,_になっているやつはこれが型です
#_,_はデータ構成子
#ああなるほど．
#Πを使うのかとおもた．
#swap-plusの場合はそれで最後になっているから意味が違ってきちゃうのか
#n1+n3=n6かつn2+n6=n5となるn6がある
#です．
#最初のだと
#n6があって、n1+n3=n6ならn2+n6=n5だから
#ああああ
#型が間違っている
#です．
#uniqueness-plusについてはuniqueness-plus : ∀ {n₁ n₂ n₃ n₄} → ∑ (n₁ plus n₂ is n₃) (n₁ plus n₂ is n₄) → n₃ ≡ n₄
でもいいはず#associativity-*もなんか矛盾が出まくりでおかしいなーと思ってたけど、これも完全に間違っている
#てことですね。。。
#ようやく分かりました。
#多分これが問題で定理2.9も証明ができなくなってるんだ。
#ありがとうございました
#あー
#ん？
#なにか？
#「あー」？
#ああ、いや
#単なる溜息です
#orzみたいな
#よかった．^.^
#uniqueness-plusをまずは連言で書き直した
#やんなくてもいいけど
#連言として書いた方が自分では分かりやすそう
#というか勘違いしない
#この調子ですすめてみます
#確かに連言で書いたほうがわかりやすいね．
#Σじゃなくて×の方で
#なんかこの辺どっちでもよさげだ
#ちょっと教えて，
#はい
#Σってどう定義されてるの？記号の印象としては連言はΠの印象があるんだけど，Πは全然違う意味で使ってるのかな．
#agda2-mode使えます?
#いま使える状態にない．ghc-7.10.1 で cabal-install すればいい？
#record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
constructor _,_
field
proj₁ : A
proj₂ : B proj₁#もし使えれば ESC-.で定義にjumpできるんで、と思っただけです
#こんな定義になってますね
#これ選言に見えるけど
#ああちがう．
#これProductだから多分いいような
#module Data.Product where
#そうですね．
#AとBが対称じゃないのか．
#ああまさにプロダクト，積か．
#依存するので対称じゃないんですよね
#どうもその辺りでLevelもあがるしイマイチ込みいってくると混乱する
#ので、あまり使い慣れなくて
#チュートリアル追う時は自分で作った方が簡単になる気がする
#反転しても同型だよね．
#反転というのは入れかえてもってこと？
#uniqueness-timesも修正
#これは元々正しかったからほぼそのまま書き換えられたけど
#Σ{a b} {A : B -> Set a} {B : Set b}
#どうだろう、これ書けないような
#Agdaって記述の上での前後関係あるじゃないですか
#前のものに後ろのものが依存する
#こちらHaskellのMetaTheory.hsもたぶん修正しないといけない気がする．
#ああなるほど
#でも確認してよかtた
#全然間違ってたし
#躓いてたから諦めなければ早晩発覚はするんでしょうが
#存在をGHCの型システムで表明する方法がわからない．
#なんかアイデアある？
#いや、どっかで見た気はするけど
#konnさんかなぁ
#うーん、ちょっと手元にはそれらしいの残ってないです
#(∃x.P(x)) -> Q ⇔ ∀x.(P(x) -> Q) とかいうのはあるんだけど．
##たしかにforall使うことになるんじゃなかったっけ
#それたぶん．(∃x.P(x)) -> Q ⇔ ∀x.(P(x) -> Q) の説明だとおもう．
#UHCでは書けそうだなぁ
##aoeさんか
##これだったか
#ようやっとassociativity-plus証明できたけどなんかもうちょっと整理できないものか？ってくらい複雑
#ようやく定理2.9に戻ってこれた
#swap-plus証明でけたー
#ようやっと今日本届いたのでとりあえず定理2.9まで示しましたがこれで追い付けた？
#すでに抜かれた
#2.9まだです
#もなか
##assoc-plusシンプルに解けてますね
#plus-assocか
#times-closure途中でplus-closureをwithしていますけど
#これどう考えたらそれやろうと思います?
#C-cC-,でいくら眺めてみてもそれ思い付かないんですが
#こっちのCaseではゴールが ∃ λ n₃ → S n₁ times n₂ is n₃ なので
#S n₁ times n₂ is n₃ のカタチだけ見れば n₁ * n₂ = hoge と n₂ + hoge = n₃ があればT-SUCCで終わるだろうと
#そういう流れで前者がひとつめのwithで後者がふたつめのwith
#だったかと
#最近ようやくwithを使う感覚が掴めつつあったんですが
#まだ完全に分かっていなくて
#使えたり使えなかったりするし、そもそもC-cC-,で見えてないと全然思い付かないっす
#特にこっちでのn1-n4を暗黙にしているからかもしれませんが
#変数が自動生成のままなんでたぶん実際やってたときはあんまり考えてなくて直感的に流したかもしれません，が後付けでも理由付けるとこんなんです．
#plus-closureに渡す引数も全然見えてこないからヒントもらってもなかなか出来なそうです
#なるほど
#自分が丁寧に考えてるとことそうでないところは大体わかりやすくて変数名を丁寧に付け換えてるとこは考えてますね．
#まぁ見栄えのためだけに後で付け換えてるとこはあったりもしますが
#ただ換えてないとこはサラッと流してしまったとこなのはほぼ確定です．
#再帰パターンになるだろうし、withで評価させてみるかーみたいな軽い感じですかね
#timesの方はtimesとplusで構成されてるんだから両方あててやればどうだ？と
#closure-timesは合ててたけど
#当ててたけど
#plusには及ばなかった
#どちらかというと再帰というより，existsをどう見つけるかというほうにカンを向けている気がします．
#良いexistsなんちゃら(タプルの左側)を発見・構成する程，その後(タプルの右側)がラクなので．
#ふーむ
#あぁ、そうか
#existsを見つけたいために出来るだけ引数間の関係やら具体的な情報を引き出したいというのがあってのwithだと思えばいいのかな
#わっかりにくい表現だしかし
#なんか出来たな
#引数は暗黙にしてたからではなくて、オレがちゃんと見てなかったからだな
#n2 proj1で呼べばいいのは判断の関係を見ればわかる
#あとclosureとidentityは暗黙にしないほうがいいですよ
#引数
#それはなぜでしょう？
#いや、実はいつも暗黙にしてから暗黙にしないほうが分かりやすいかなーって思うことは多いんですけど
#たぶんですが，そのほうが使い易い
#というのは
#他のやつはそれ以降で暗黙部分もちゃんと判明するけど，closureとidentityはそれがわからないまま結果の型になるからです
#てことは
#実際に証明しているときには証明が終わったときに暗黙部分がはっきりするかどうかは定かではないわけだから
#通常は暗黙の引数にして始めたりはしない？
#最初は明示しておいて進めることが多い？
#いえ，たとえばcommとかassocは暗黙部分もわかるので無いほうがラクです．
#解く前の話ですか
#命題の型の結果の型という
#ではなく，使う時の話です
#証明したものを？
#はい
#まだよくわかってないのですが
#identityの場合は
#(n : Nat) -> Z plus n is nとするべきだと
#{n} -> Z plus n is nとすると？
#使う時にnを渡したくなるからってことです？
#「渡したくなるシーンが多いから」ですかね
#identity nとして使いたいということでいいです？
#渡さなくても良いシーンもある
#型が既に決まっている位置に当てはめるように使う場合は渡さなくてもよい
#ああ、commやassocは_plus_is_や_times_is_を渡した時に自動的に判明するからってことですね
#そうでなく，その結果が欲しいだけの場合は明示的に渡すことになる
#そうです
#じゃあ一般的には foo -> bar となっててfooが暗黙の引数に依存している場合には使う時にfooを渡すことになるから自動的に暗黙の引数も判明するから暗黙にしておいてもよさげだが
#fooでしかないような場合には暗黙の引数にしちゃうと渡したくなることが多いので暗黙にせずfooが依存している引数は明示した方が良いよと
#ああ、その辺整理して考えたことなかったです
#後から暗黙じゃない方が便利だったかもと思うことは良くあったのですが、全部やるか？とかその辺はあんまり基準を持ってなかったですね
#ザックリと「後の引数の型で判明するなら暗黙，そうでない(たとえば結果の型にしか現れない)とかなら暗黙にしない」くらい
#理解しました
#ありがとうございます
#にしておくと，後でわざわざ{n}みたいに渡すシーンも，逆にムダに引数をいっぱい渡すシーンも，少なくなるでしょう．
#早速それで修正することにします
#単刀直入に言えば、2chの実装
・管理している人の中にHaskellかSchemeの人いるよね。かなり前から。
#知りませんでした．ただ，その書き方だと「確定じゃないけど」ってことかと思うんですが，参考までにそういうのって どこ情報 or 何から判断して のものなんですか？
#read.cgi, bbs.cgi は Perl で書かれた時期がありましたね、次世代は一部を JavaScript で書き直す計画があります。管理者が誰かはしりませんが「HaskellかSchemeの人」って定義はなんですか
#Haskell や Scheme に興味を持っている or プログラミング能力を持つ、ということならありえそう
#「～の人」は「～使い」くらいに解釈してました
#ぼくはしりません
haskell-ja > Archives > 2015/07/25