私はこのようなもののACL2の中で何かを行う必要があります。ACL2で再帰を使用してループする方法は？
for (i=1; i<10; i++) {
print i;
}
それはCOMMON LISPを使用していますが、私はこの作業を行うにはどのように任意のアイデアを持っていない...
我々は標準を使用することはできませんLOOP、DOのような共通のLisp構造体。ちょうど再帰。
私はいくつかのリンクを持っているが、私は理解することは非常に困難見つける：
セクションを「すべての訪問A Gentle Introduction to ACL2 Programmingのnから0までの自然数について説明しています。
(defun visit (n max ...)
(cond ((> n max) ...) ; N exceeds MAX: nothing to do.
(t . ; N less than or equal to MAX:
. n ; do something with N, and
.
(visit (+ n 1) max ...) ; visit the numbers above it.
.
.
.)))
再帰を使用するソリューション：
> (defun for-loop (from to fn)
(if (<= from to)
(progn
(funcall fn from)
(for-loop (+ from 1) to fn))))
;; Test
> (for-loop 1 10 #'(lambda (i) (format t "~a~%" i)))
1
2
3
4
5
6
7
8
9
10
NIL
ACL2（DEFUN FOR-LOOP ...）のエラー：IFは3つの引数をとるが、 コール（IF（<= FROM TO）（PROGN（FUNCALL FN FROM）（FOR-LOOP FN））） 2つの引数が与えられます。 IFの仮パラメータリストは（X Y Z）です。 ACL2システムによる印刷物。あなたがIFに3番目の引数を追加しようとすると、 – toxaus
戻り値 - ACL2 p！>（defun for-loop（fnから）へ） （if（<= from）） （progn （funcall fn（forループ（+ 1からfn）） 'nil）） ACL2のエラー（DEFUN FOR-LOOP ...）：コード内のPROGN の使用を許可していませんCommon Lispの意味がACL2の意味と異なるため、Common Lispによって実行されます。 – toxaus
（defunのfooのループ（N） （指揮（（ZP n）が「済：あなたのケースでは
あなたはあなたのコードは次のようになりますので、昇順で番号を訪問したいです「） （トン（PROG2の$（CW "〜X0" n）を （FOO-ループ（1 N）））））
（FOO-ループ10）
あなたは、終了条件をやり直すことができます1から10になる模倣への再帰。
ありがとう！その正しい方法。 – toxaus