#*Language.BCoPL.Nat> Z'
Z
*Language.BCoPL.Nat> :t Z'
Z' :: Nat' 'Z
*Language.BCoPL.Nat> Z' :: Nat' 'Z
<interactive>:5:12:
Data constructor ‘Z’ cannot be used here
(Perhaps you intended to use DataKinds)
In an expression type signature: Nat' Z
In the expression: Z' :: Nat' Z
In an equation for ‘it’: it = Z' :: Nat' Z#あれぇ？
#これどういう意味だろう。
#*Language.BCoPL.Nat> read "Z" :: Nat' 'Z
<interactive>:6:18:
Data constructor ‘Z’ cannot be used here
(Perhaps you intended to use DataKinds)
In an expression type signature: Nat' Z
In the expression: read "Z" :: Nat' Z
In an equation for ‘it’: it = read "Z" :: Nat' Z#まぁそうなるわな。 read の動作を確かめたいだけなんだけどなぁ
#hoge :: Plus Z (S Z) (S Z)
#hoge = PZero (read "S(Z)")
#とスクリプトに書いておいて
#*Language.BCoPL.Nat> hoge
Z plus S(Z) is S(Z) by P-Zero { }#read はちゃんと機能しているらしい
##nobsun:「そのままはりつければよい出力を得る」の意味がわかりません…Emacs bufferに表示させるだけなら C-c C-n (Evaluate term to normal form) ですし、表示するなら「型：rules -> S(n) + S(S(n)) == S(S(S(n)))」「証明：rule をどう適用するかを書く」で、C-c C-a (Agda auto) で人間が書かなくても ? から Agda と Agsy (auto prover) が勝手にやります、これでどうでしょうか
###Nat の plus だけしかやってませんけど
#＞ikegami__さん 「そのままはりつければよい出力」というのは，五十嵐淳さんの『プログラミング言語の基礎概念』のための演習システムのテキストエリアへの入力としてそのままつかえる構文を満した文字列表現という意味です．http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/CoPL/index.cgi #あーなるほど
#ちなみに Z3 ソルバでできるというのは間違いでしたテヘペロ
#ぼくがCoPLをAgdaで遊んでたときは手で翻訳していました（ださい）
#> Agdaだと，件の演習システムにそのままはりつければよい出力を得るのはどうやればいいの？
#なんですが、証明はやって、その証明オブジェクトをあの形式に書き出すようにしました。
#機械にやらせるなら二つの方法が考えられます : CoPL 専用 pretty printer を Agda で書く : Agda の内部表現を好きな言語で pretty print する
#notogawa さんは後者について知ってそう
#prettyにはしてないけど、コピペで貼り付ければいいだけの出力はできるようにしてる。
#おお．そのあたりのコードがみたいなぁ．
#いま考えているのは，たとえば，Plus n1 n2 n3 をShowはできるので，"n1 plus n2 is n3" という文字列から Plus n1 n2 n3 が構成できれば，つまり，Plus n1 n2 n3をReadのインスタンスにできれば，型レベルでも自動導出ができることになるなぁと．
#githubに上げてるけど、なんてことない感じになってます。
#おお参考にさせてもらいやす．
#なるほどでやんす．
#reader はないの？(そっちもあればパクらせてもらいたいなぁ)
#Readerってサイトに書き込む書式対応のってことですよね。ないです。
あとImplicit aegによるアドホック多相が最新Agdaで使えなくなったのでそもそもshowもイマイチですよねー。
#s/aeg/arg
#GHCの型システムで，CoPLの定理2.3「任意のペアノ自然数n1，n2に対して，あるペアノ自然数n3が存在して，n1 plus n2 is n3 である」のような存在表明を表現するのってどうすればいいのかなぁ．
#Nat' n1 -> Nat' n2 -> Plus n1 n2 n3 -> Nat' n3
#と表現したのですが．．．
#(j+1) * (k+1)
~~~~~~~~~~~~~ TSucc
--> j*(k+1) + (k+1)
~~~~~~~ hypo
--> (k+1)*j + (k+1)
~~~~~~~ TSucc
--> (k*j + j) + (k+1)
~~~~~~~~~~~~~~~~~ p-assoc
--> k*j + (j+(k+1))
~~~ hypo
--> j*k + (j+(k+1))
~~~~~~~ p-comm
--> j*k + ((k+1)+j)
~~~~~~~~~ lemma
--> j*k + (k+(j+1))
~~~~~~~~~~~~~~~ p-assoc
--> (j*k + k) + (j+1)
~~~~~~~~~ TSucc
--> (j+1)*k + (j+1)
~~~~~~~ hypo
--> k*(j+1) + j+1
~~~~~~~~~~~~~ TSucc
--> (k+1) * (j+1)#こっちは定理2.9の証明の方針みたいなものです．あってますかねぇ．
haskell-ja > Archives > 2015/07/24