«Строго позитивный» в Агде - PullRequest
Новая
       38

«Строго позитивный» в Агде

28 голосов
/ 06 апреля 2010

Я пытаюсь закодировать некоторую денотационную семантику в Agda на основе программы, которую я написал на Haskell. 

data Value = FunVal (Value -> Value)
           | PriVal Int
           | ConVal Id [Value]
           | Error  String

В Agda прямой перевод будет: 

data Value : Set where
    FunVal : (Value -> Value) -> Value
    PriVal : ℕ -> Value
    ConVal : String -> List Value -> Value
    Error  : String -> Value

но я получаю сообщение об ошибке, связанное с FunVal, поскольку;

Значение не является строго положительным, поскольку оно встречается слева от стрелки в типе конструктора FunVal в определении Value.

Что это значит?Могу ли я закодировать это в Agda?Я поступаю неправильно?

Спасибо.

1 Ответ

34 голосов
/ 06 апреля 2010

HOAS не работает в Агде, из-за этого: 

apply : Value -> Value -> Value
apply (FunVal f) x = f x
apply _ x = Error "Applying non-function"

w : Value
w = FunVal (\x -> apply x x)

Теперь обратите внимание, что оценка apply w w возвращает вам apply w w снова. Термин apply w w не имеет нормальной формы, что в Агде запрещено. Используя эту идею и тип: 

data P : Set where
    MkP : (P -> Set) -> P

Мы можем вывести противоречие.

Один из путей выхода из этих парадоксов состоит только в том, чтобы разрешить строго положительные рекурсивные типы, что выбирают Agda и Coq. Это означает, что если вы объявите: 

data X : Set where
    MkX : F X -> X

То, что F должен быть строго положительным функтором, это означает, что X никогда не может появляться слева от любой стрелки. Таким образом, эти типы строго положительны в X: 

X * X
Nat -> X
X * (Nat -> X)

Но это не так: 

X -> Bool
(X -> Nat) -> Nat  -- this one is "positive", but not strictly
(X * Nat) -> X

Короче говоря, нет, вы не можете представлять свой тип данных в Agda. Вы можете использовать кодировку де Брюйна, чтобы получить тип термина, с которым вы можете работать, но обычно функция оценки требует своего рода «тайм-аут» (обычно называемый «топливом»), например максимальное количество шагов для оценки, потому что Agda требует, чтобы все функции были полными. Вот пример из-за @gallais, который использует для этого тип коиндуктивной пристрастности.

...