"Estrito positivo" em AGDA
-
24-09-2019 - |
Pergunta
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.
Solução
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.