問題タブ [acl2]

次のエラー メッセージが表示されるのはどういう意味ですか? GLをロードしました。

ctrl+te を使用してフォームを ACL2 シェル バッファーにコピーしようとすると、シェル バッファーに既に time$ が配置されているため、フォームを貼り付けることができないというエラーが表示されます。既に (time$ が書き込まれている ACL2 シェル バッファーに貼り付けられるように、emacs マクロを変更するにはどうすればよいですか?

acl2 を使用して、最初の引数 (リスト) を 2 番目の引数 (別のリスト) の各要素の前に再帰的に追加する関数「ins」を作成しようとしています。

戻り値

そのため、そのような関数への呼び出し

私たちに与えます

空かどうかをチェックして、単一の要素を含むarg2リストでのみ機能する非再帰関数を思いつきました。

再帰的なものを考え出そうとすると、最初の引数が 2 番目の引数のリスト内のすべての要素に追加されます。

しかし、何があっても常にゼロになり、その理由がわかりません。そのため、再帰呼び出しが正しいかどうかさえわかりません。自明ではない再帰をトレースするのに苦労しています。

リストと自然数を取り、指定されたインデックスでリスト内の項目を返す ACL2 (具体的には ACL2s) に関数を記述しようとしています。したがって、 (select (list 1 2 3) 2) は 3 を返します。

これが私のコードです：

次のエラーが表示されます。

どんな助けでも大歓迎です！

ACL2 で自然数を単項表記 ( O、(S O)、(S (S O))、...) でモデル化し、加算の可換性を証明しようとしています。これが私の試みです：

これはおそらくこれを行う最も LISPy な方法ではありません。私はパターン マッチングを使用する言語に慣れています。

私の問題は、コメントで示唆されているとおりです。証明者はループし、同じもののより深くネストされたバージョンを証明しようとします。どうすればこれを止めることができますか? マニュアルでは、ループ書き換えルールについて簡単に言及していますが、それらについて何をすべきかについては何も述べていません。

私の期待は、この証明は失敗し、それを完了するために必要な補助補題についてのヒントを与えてくれるというものでした。ループ証明からの出力を使用して、ループを停止する可能性のある補題を見つけ出すことはできますか?

ACL2 マクロ トランスフォーマーで、関数定義を最上位に持ち上げることは可能ですか?

関数を指定すると、以下のlet-mapような関数を定義できるマクロを設計しようとしています。map-doubledouble

最上位のみを気にする場合は、define-mapマクロを使用してこれを行うことができます。ただし、このマクロを別の式内にネストされたコンテキストで呼び出すことができるようにしたいと考えています。たとえば、次のようになります。

let-mapマクロで function を定義してから、本体の結果を返します。map-doubleこの場合は を呼び出し(map-double (list 1 2 3))ます。これを で定義しようとしましfletたが、私のmap-double関数は再帰的であるため、機能fletしません。

を使用しますlabelsが、ACL2 ではサポートされていません。

map-fしたがって、再帰を可能にするために、 (map-doubleこのマクロを使用している)の定義をトップレベルに上げたいと思います。これは ACL2 マクロ システムで可能ですか?

ラケットのようなシステムでは、このような機能を使用しますsyntax-local-lift-expression。では、ACL2 に類似の形式はありますか?