1

在常见的 lisp 中有map，它可以让你做这样的事情：

(map (lambda (x y) (/ x y)) (list 2 4 6 8 10 12) (list 1 2 3 4 5 6))

返回(2 2 2 2 2 2)

但是现在我在 ACL2 工作，没有map. 所以在我看来，我剩下的唯一选择就是递归计算我想要的，除非有另一种更简单和/或更有效的方法。

...这正是我的问题。有没有比创建一个称为类似的递归函数更好的方法divide-two-lists？感觉就像是基于 lisp 的语言自然应该做的事情，而不是让你专门为它创建另一个函数，这就是我问的原因。

4

3 回答 3

0

您可以很容易地编写自己的地图。来自GNU Emacs 指南：

(defun mapcar* (function &rest args)
  "Apply FUNCTION to successive cars of all ARGS.
          Return the list of results."
  ;; If no list is exhausted,
  (if (not (memq nil args))
      ;; apply function to cars.
      (cons (apply function (mapcar 'car args))
            (apply 'mapcar* function
                   ;; Recurse for rest of elements.
                   (mapcar 'cdr args)))))

(mapcar* 'cons '(a b c) '(1 2 3 4))
⇒ ((a . 1) (b . 2) (c . 3))

我对 acl2 不熟悉，因此您可能必须更改某些函数（例如memq），或者以不同的方式处理apply参数&rest的工作方式，但这是代码的核心。

于 2013-09-09T05:55:32.070 回答
0

ACL2 基于一阶逻辑。在一阶逻辑中，语句如

（定义（PRA）（RA））

不允许，因为 R 既用作参数又用作函数。

从理论上讲，通过在包含高阶逻辑结构的一阶逻辑中逐字定义您自己的语言来解决这个限制是可能的。否则，你是对的，你最好的选择是在每次你想使用 map 函数时定义像除两个列表这样的东西。

这很乏味，但这就是 ACL2 的使用方式。

于 2013-09-15T22:34:21.957 回答
0

这并不完全适合您的问题，但它是相关的，所以我提到它以防它帮助其他正在查看您的问题的人。

考虑一下“std/util/defprojection”一书，它提供了一个宏，可让您在列表中映射函数。

于 2014-07-21T04:14:00.933 回答