2006-09-29

・パターン式中で、同じパターン変数を使えない
・quoteの扱いが微妙

;Gaucheで
>(use util.match)
>(match '(1 1 1 1) ( (t t t t) #t ) )
*** ERROR: duplicate variable in pattern (t t t t)
>(match '((lambda (x) x) 1) (((lam (var) exp) arg) #t))
#t
>(match '((lambda (x) x) 1) ( (('lambda (var) body) arg) #t ))
#t
>(match '((lambda (x) x) 1) ( (('lam (var) body) arg) #t ))
*** ERROR: : no matching clause for ((lambda (x) x) 1)
>(match '('x) ( ('a) #t ))
*** ERROR: : no matching clause for ('x)
>(match '('x) ( (quot a) #t ))
*** ERROR: : no matching clause for ('x)
>(match '(quote x) ( (quot a) #t ))
#t
>(match '(quote x) ( ('quote a) #t ))
#t
> (define (orz x)
   (match x
    ( (? list? e) (map orz e) )
    ( e (x->integer e) )))
>(orz (list 2 "3" 'hoge))
(2 3 0)

単一化の方が強力なんだけど、じゃあ、パターンマッチングで不十分な時っていつよ？ってなると、私には分からない

例えば、ラムダ計算へのマッピングを与えるようなのが、表示的意味論。直接reductionを定義してしまうようなのが、操作的意味論。ラムダ計算の表示的意味論は、ラムダ計算へマッピングしても意味がないので、領域理論とかいうのでやるらしい。あと、公理的意味論というのがあるらしいので、調べていたら、
An axiomatic definition of the programming language PASCAL
というのを見つけた。読んでみたいのだけど、古すぎて(1973年!)、オンラインでは読めないorz

何気に、こんなものが。
A Formal Semantics for the C Programming Language
200ページ以上あるので、読んでないけど、1.4節によれば、Ada , Algol60 ,Pascal , Smalltalk-80に対して表示的意味論を与える試みがあって、EiffelやStandard MLに対して、操作的意味論を与える試みがあったそうな。公理的意味論は、Pascalくらい(´・ω・｀)ショボーン

Action Semanticsという謎の意味論は、Ada , Cobol , C++ , Modula-2 , Oberon , Occam , Prolog　, Smalltalkに対して使われたそうな。すげえ！Oberonとか初めて聞いたよ。

Cの操作的意味論を与えたとか書いてんな〜、このへんで
http://citeseer.ist.psu.edu/norrish97abstract.html
HOL上で実装したとか書いてあるけど、すると、例えば、Gaucheが実際にR5RSのformal semanticsを満たしてることを証明できるかもしれないんだな。もっとも、仕様上では未定義だけど、大抵の処理系でうまくいくとか、あるいはgccでのみうまくいくとか、そんな裏技が使われてるかもしれないので、一筋縄ではいかないかもしれないけど

#よく考えたら、Gaucheは本格的すぎるので、最初はTinySchemeみたいな小さい処理系でやるか、もういっそ自分でminimalなscheme処理系書くとかした方がいいのか。それから、何気に、Haskellのformal semanticsというのが見当たらない

プログラミング言語は掃いて捨てるほどあるので、各言語に、意味論与えていけば、論文のネタに一生困らないかもしれない(それはない)。Formal Semantics for Perl , Formal Semantics for Ruby , Formal Semantics for BrainF*ck , ...

パターンマッチの練習

Semantics動物園