Что это за карта [f] - PullRequest
Новая
       7

Что это за карта [f]

0 голосов
/ 27 октября 2018

Предположим, у меня есть Sort 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на?И что-то вроде отображения foo на b?Есть ли способ испортить тип индексов и получить из массива, индексированного T, массив, индексированный другим видом, скажем, например, Int?

1 Ответ

0 голосов
/ 27 октября 2018

Применяются обычные правила соответствия сортировки. То есть для map функции f : A -> B в массиве массив должен иметь тип диапазона A, и он будет преобразован в B, сохраняя тип его домена.

Относительно вашего примера: независимо от того, какой у вас T, вы просто будете иметь Array T Int в качестве окончательной сортировки, если вы отобразите foo, и Array T Bool в качестве результата, если вы отобразите bar. Следующие скрипты проверяют тип без проблем: 

(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, я полагаю), отображая функцию в массиве. Изменяет только тип диапазона.

...