Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Saturday, 06-Feb-2021 22:59:39 JST きゅーけー

   全ての関数が全域で変な値がどの分岐に入るかを一応考えないといけないのは少し難しい気がしてる。再帰関数の場合は変な値は基底部の方に入れるようにする。変な値を受け入れていいのかという問題自体は Guard で解決可能なのでそこを気にする必要はないんだけど、納得するのがむずかしい問題かもしれない。

   • 杉田匠 (tacumi@misskey.io)'s status on Saturday, 06-Feb-2021 23:18:05 JST 杉田匠

     in reply to

     @tojoqk@mastodon.tojo.tokyo https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/COMMON-LISP____FLETfletで局所関数も作れたりするので変な値とやらはそこに隠すのもいいかも

     きゅーけー repeated this.
   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Saturday, 06-Feb-2021 23:18:05 JST きゅーけー

     in reply to

     • 杉田匠

     @tacumi ここで話している変な値は関数が本来受け入れたくない値のことでした。たとえば、階乗を計算をする関数を実装する場合に自然数のみを引数に取りたいと思っても ACL2 では全ての関数が全域でないといけないので、どんな値を渡しても計算が停止しなんらかの値を返さなければなりません。この例の場合では zp という関数を使って条件分岐すると、自然数以外の値を全て 0 として処理してくれて、 0 の場合が基底部になるのでこれが正解(zerop で分岐すると話が難しくなる)なんですが、これに納得するのが難しいだろうなという趣旨でした。基本的には上記の zp のような異常な値を特定の値であるとみなす述語を使うことで解決します。

     http://www.mathcs.duq.edu/simon/acl2/ZERO-TEST-IDIOMS.html

     (誤解されると非常にまずいので毎回書いているのですが、ACL2 は Guard という機能で自然数でない値が渡されないことを静的に検証することが可能です。ただ、Guard を使っていても、自然数でない値を引数にとってもなんらかの値を返すように関数を書かないといけないんです)