«Не строго положительное явление ...» - PullRequest
Новая
       5

«Не строго положительное явление ...»

0 голосов
/ 02 февраля 2019

Я пытаюсь определить следующий тип 

Inductive t : Type -> Type :=
  | I : t nat
  | F : forall A, (t nat -> t A) -> t A.

и получаю следующую ошибку: 

Non strictly positive occurrence of "t" in "forall A : Type, (t nat -> t A) -> t A".
  • Что означает эта ошибка?
  • Есть ли способ «исправить» определение, чтобы сделать его действительным?
  • Где я могу узнать больше об этом?

Спасибо!

1 Ответ

0 голосов
/ 02 февраля 2019

Вы можете найти общие сообщения об ошибках в справочном руководстве Coq: https://coq.inria.fr/distrib/current/refman/language/gallina-specification-language.html?highlight=positive#coq:exn.non-strictly-positive-occurrence-of-ident-in-type

По сути, если конструктор содержит функции (такие как t nat -> t A), они не могут упоминать индуктивный тип, определяемый как частьаргумента (t nat). 

        vvvvvvvvvvvvvv argument
F : ... (t nat -> t A)               -> t A
                  ^ OK ("positive occurence")
         ^ Not OK ("negative occurence")

Этот раздел в Сертифицированном программировании с зависимыми типами (CPDT) объясняет проблему с помощью упрощенного примера: http://adam.chlipala.net/cpdt/html/Cpdt.InductiveTypes.html#lab30

Если бы вы могли определитьтип 

Inductive term : Set :=
| App : term -> term -> term
| Abs : (term -> term) -> term.

тогда вы можете определить функцию 

Definition uhoh (t : term) : term :=
  match t with
    | Abs f => f t
    | _ => t
  end.

и uhoh (Abs uhoh) будет расходиться.

...