什么是地图[f]

Question

假设我有一个排序 T 并且我声明了一个由 T 索引的数组，它的映射是什么类型的？

例如

(declare-datatypes ()
  ((T ....))) ; some index, may be finite or infinite (as in Int)
(declare-const a (Array T Int))
(declare-const b (Array Int Int))
(define-fun foo ((x Int)) Int)
(define-fun bar ((y Int)) Bool)

什么是 foo 上的映射？和 b 上的那种映射 foo？有没有办法弄乱索引类型并从由 T 索引的数组中获取由另一种排序索引的数组，例如诠释？

Answer 1

通常的排序匹配规则适用。也就是说，对于数组上的map 函数f : A -> B，该数组必须具有其范围类型A，它会将其转换为B，并保留其域的类型。

关于您的示例：无论您的T 是什么，如果您映射foo，您只需将Array T Int 作为最终排序，如果您映射bar，则将Array T Bool 作为结果。以下脚本类型检查没有任何问题：

(declare-datatypes ((T 0)) ((i Int)))
(declare-const a (Array T Int))
(declare-const b (Array Int Int))
(declare-fun foo (Int) Int)
(declare-fun bar (Int) Bool)

(define-fun e1 () (Array T  Int)   ((_ map foo) a))
(define-fun e2 () (Array T  Bool)  ((_ map bar) a))
(define-fun e3 () (Array Int Int)  ((_ map foo) b))
(define-fun e4 () (Array Int Bool) ((_ map bar) b))

请注意，您不能通过将函数映射到数组来更改域的类型（我认为这是 index 的意思）。它只会改变范围类型。