"Estrito positivo" em AGDA

Question

Estou tentando codificar alguma semântica denotacional na AGDA com base em um programa que escrevi em Haskell.

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

Na AGDA, a tradução direta seria;

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

Mas recebo um erro relacionado ao Funval porque;

O valor não é estritamente positivo, porque ocorre à esquerda de uma seta no tipo de Funval do construtor na definição de valor.

O que isto significa? Posso codificar isso no AGDA? Estou fazendo isso da maneira errada?

Obrigado.

Answer 1

Hoas Não funciona na AGDA, por causa disso:

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

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

Agora, observe que avaliar apply w w da-te apply w w de volta. O termo apply w w Não tem forma normal, que não é não na AGDA. Usando esta ideia e o tipo:

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

Podemos derivar uma contradição.

Uma das formas desses paradoxos é apenas permitir tipos recursivos estritamente positivos, que é o que a AGDA e o CoQ escolhem. Isso significa que, se você declarar:

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

Este F deve ser um functor estritamente positivo, o que significa que X pode nunca ocorrer à esquerda de qualquer flecha. Portanto, esses tipos são estritamente positivos em X:

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

Mas estes não são:

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

Então, em suma, não, você não pode representar seu tipo de dados na AGDA. Você pode usar a codificação de Bruijn para obter um tipo de termo com o qual você pode trabalhar, mas geralmente a função de avaliação precisa de algum tipo de "tempo limite" (geralmente chamado de "combustível"), por exemplo, um número máximo de etapas para avaliar, porque o AGDA requer todas as funções para ser total. Aqui está um exemplo Devido ao @Gallais que usa um tipo de parcialidade coindutiva para conseguir isso.