haskell-ja > Archives > 2015/07/24

2015/07/24 00:22:48 UTCnobsun
#
*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 の動作を確かめたいだけなんだけどなぁ
2015/07/24 00:53:13 UTCnobsun
#
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 はちゃんと機能しているらしい
2015/07/24 03:13:25 UTC[1..100]>>=pen
#
近づいたので再掲。7月25日(土)第22回「Haskellもくもく会」 #hasmoku http://haskellmokumoku.connpass.com/event/17228/
2015/07/24 05:38:08 UTCikegami__
#
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) が勝手にやります、これでどうでしょうか
#
おおげさかもしれませんが Agda の ring solver のようにルールを書いた後に refl 一発という方法もありそうです http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.UsingTheRingSolver
2015/07/24 07:07:00 UTCikegami__
#
導出システム Nat を Z3 ソルバでやってみました(どんどん Haskell とは関係ないな) https://twitter.com/ikegami__/status/624474793857781760
#
Nat の plus だけしかやってませんけど
2015/07/24 09:48:09 UTCnobsun
#
>ikegami__さん 「そのままはりつければよい出力」というのは,五十嵐淳さんの『プログラミング言語の基礎概念』のための演習システムのテキストエリアへの入力としてそのままつかえる構文を満した文字列表現という意味です.http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/CoPL/index.cgi
2015/07/24 09:49:13 UTCikegami__
#
あーなるほど
#
ちなみに Z3 ソルバでできるというのは間違いでしたテヘペロ
#
ぼくがCoPLをAgdaで遊んでたときは手で翻訳していました(ださい)
2015/07/24 09:59:31 UTCcutsea110
#
> Agdaだと,件の演習システムにそのままはりつければよい出力を得るのはどうやればいいの?
#
なんですが、証明はやって、その証明オブジェクトをあの形式に書き出すようにしました。
2015/07/24 10:01:02 UTCikegami__
#
機械にやらせるなら二つの方法が考えられます : CoPL 専用 pretty printer を Agda で書く : Agda の内部表現を好きな言語で pretty print する
#
notogawa さんは後者について知ってそう
2015/07/24 10:03:35 UTCcutsea110
#
prettyにはしてないけど、コピペで貼り付ければいいだけの出力はできるようにしてる。
2015/07/24 10:21:36 UTCnobsun
#
おお.そのあたりのコードがみたいなぁ.
2015/07/24 10:26:33 UTCnobsun
#
いま考えているのは,たとえば,Plus n1 n2 n3 をShowはできるので,"n1 plus n2 is n3" という文字列から Plus n1 n2 n3 が構成できれば,つまり,Plus n1 n2 n3をReadのインスタンスにできれば,型レベルでも自動導出ができることになるなぁと.
2015/07/24 10:46:03 UTCcutsea110@twitter
#
githubに上げてるけど、なんてことない感じになってます。
2015/07/24 10:51:38 UTCnobsun
#
おお参考にさせてもらいやす.
#
なるほどでやんす.
#
reader はないの?(そっちもあればパクらせてもらいたいなぁ)
2015/07/24 17:39:47 UTCcutsea110@twitter
#
Readerってサイトに書き込む書式対応のってことですよね。ないです。
あとImplicit aegによるアドホック多相が最新Agdaで使えなくなったのでそもそもshowもイマイチですよねー。
2015/07/24 17:50:58 UTCcutsea110@twitter
#
s/aeg/arg
2015/07/24 22:09:39 UTCnobsun
#
GHCの型システムで,CoPLの定理2.3「任意のペアノ自然数n1,n2に対して,あるペアノ自然数n3が存在して,n1 plus n2 is n3 である」のような存在表明を表現するのってどうすればいいのかなぁ.
#
Nat' n1 -> Nat' n2 -> Plus n1 n2 n3 -> Nat' n3
#
と表現したのですが...
2015/07/24 22:41:24 UTCnobsun
#
(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の証明の方針みたいなものです.あってますかねぇ.