Na primeira parte do artigo sobre a linguagem Arend, examinamos os tipos indutivos mais simples, funções recursivas, classes e conjuntos.
2. Classificando listas no Arend
2.1 Listas ordenadas no Arend
Definimos o tipo de lista ordenada como um par que consiste em uma lista e uma prova de sua ordem. Como já dissemos, em Arend, pares dependentes são definidos usando a palavra-chave
\Sigma . Fornecemos a definição do tipo
Sorted por meio de comparação com a amostra, inspirada na definição do
artigo já mencionado
sobre listas ordenadas. \func SortedList (O : LinearOrder.Dec) => \Sigma (l : List O) (Sorted l) \data Sorted {A : LinearOrder.Dec} (xs : List A) \elim xs | nil => nilSorted | :-: x nil => singletonSorted | :-: x1 (:-: x2 xs) => consSorted ((x1 = x2) || (x1 < x2)) (Sorted (x2 :-: xs))
Nota: Arend conseguiu inferir automaticamente que o tipo
Sorted está contido no universo
\Prop . Isso aconteceu porque todos os três padrões na definição
Sorted são mutuamente exclusivos e o construtor
consSorted possui dois parâmetros, ambos pertencentes a
\Prop .
Vamos provar alguma propriedade óbvia do predicado
Sorted , digamos que o final de uma lista ordenada seja ela própria uma lista ordenada (essa propriedade será útil para nós no futuro).
\func tail-sorted {O : LinearOrder.Dec} (x : O) (xs : List O) (A : Sorted (x :-: xs)) : Sorted xs \elim xs, A | nil, _ => nilSorted | :-: _ _, consSorted _ xs-sorted => xs-sorted
Na
tail-sorted usamos a correspondência de padrões na lista
xs e o predicado
Sorted ao mesmo tempo; além disso, usamos o
caractere de salto “_”, que pode ser substituído por variáveis não utilizadas.
Alguém pode perguntar se é possível em Arend provar a propriedade de listas ordenadas, mencionadas na seção 1.3 como um exemplo de um fato que não pode ser provado na Agda sem anotações de imaterialidade. Lembre-se de que essa propriedade afirma que, para provar a igualdade de listas ordenadas definidas por meio de pares dependentes, basta verificar a igualdade dos primeiros componentes dos pares.
Argumenta-se que em Arend essa propriedade é facilmente obtida como conseqüência da construção
inProp mencionada acima e da propriedade de extensionalidade para pares
SigmaExt dependentes.
\func sorted-equality {A : LinearOrder.Dec} (l1 l2 : SortedList A) (P : l1.1 = l2.1) : l1 = l2 => SigmaPropExt Sorted l1 l2 P
A propriedade
SigmaPropExt provada no módulo
Paths da biblioteca padrão, e muitos outros fatos do segundo capítulo
do livro HoTT , incluindo a
propriedade de extensionalidade funcional , também são provados lá.
O operador
.n usado no Arend para acessar o projetor do tipo sigma com o número n (no nosso caso, o tipo sigma é
SortedList A , e a expressão
l1.1 significa que o primeiro componente desse tipo é uma expressão do tipo
List A ).
2.2 Implementação da propriedade “be permutation”
Agora vamos tentar implementar a função de classificação de lista no Arend. Naturalmente, queremos ter não uma implementação simples do algoritmo de classificação, mas uma implementação junto com uma prova de algumas propriedades.
Claramente, esse algoritmo deve ter pelo menos 2 propriedades:
1. O resultado do algoritmo deve ser uma lista ordenada.
2. A lista resultante deve ser uma permutação da lista original.
Primeiro, vamos tentar implementar a propriedade "ser permutação" das listas no Arend. Para fazer isso, adaptamos a definição retirada
daqui para Arend.
\truncated \data InsertSpec {A : \Set} (xs : List A) (a : A) (ys : List A) : \Prop \elim xs, ys | xs, :-: y ys => insertedHere (a = y) (xs = ys) | :-: x xs, :-: y ys => insertedThere (x = y) (InsertSpec xs a ys) \truncated \data Perm {A : \Set} (xs ys : List A) : \Prop | permInsert (xs' ys' : List A) (a : A) (Perm xs' ys') (InsertSpec xs' a xs) (InsertSpec ys' a ys) | permTrivial (xs = ys)
O predicado
InsertSpec introduzido por nós tem o seguinte significado intuitivo:
InsertSpec xs a ys significa exatamente que a lista
ys é o resultado da inserção do elemento a dentro da lista
xs (em qualquer posição). Assim,
InsertSpec pode ser tomado como uma especificação da função de inserção.
Claramente, o tipo de dados
Perm realmente define o relacionamento "ser permutação": o construtor
permInsert exatamente que
xs e
ys são mutuamente permutáveis se
xs e
ys são obtidos inserindo o mesmo elemento a em algumas listas
xs' e
ys' comprimentos mais curtos, que já são permutações um do outro.
Para nossa definição da propriedade "ser permutação", é fácil verificar a propriedade simetria.
\func Perm-symmetric {A : \Set} {xs ys : List A} (P : Perm xs ys) : Perm ys xs \elim P | permTrivial xs=ys => permTrivial (inv xs=ys) | permInsert perm-xs'-ys' xs-spec ys-spec => permInsert (Perm-symmetric perm-xs'-ys') ys-spec xs-spec
A propriedade transitividade também é satisfeita para
Perm , mas sua verificação é muito mais complicada. Como essa propriedade não desempenha nenhum papel na implementação de nosso algoritmo de classificação, deixamos isso para o leitor como um exercício.
\func Perm-transitive {A : \Set} (xs ys zs : List A) (P1 : Perm xs ys) (P2 : Perm ys zs) : Perm xs zs => {?}
2.3 Mudança nos níveis de homotopia quando comparada com a amostra
Agora vamos tentar implementar uma função que insere um elemento em uma lista ordenada para que a lista resultante permaneça ordenada. Vamos começar com a seguinte implementação ingênua.
\func insert {O : LinearOrder.Dec} (xs : List O) (y : O) : List O \elim xs | nil => y :-: nil | :-: x xs' => \case LinearOrder.trichotomy xy \with { | byLeft x=y => x :-: insert xs' y | byRight (byLeft x<y) => x :-: insert xs' y | byRight (byRight y<x) => y :-: x :-: xs' }
A construção
\case permite a correspondência com uma amostra de uma expressão arbitrária (
\elim pode ser usado apenas no nível mais alto de uma definição de função e apenas para seus parâmetros). Se você solicitar à Arend para verificar o tipo de
insert , a seguinte mensagem de erro será exibida.
[ERROR] Data type '||' is truncated to the universe \Prop which does not fit in the universe of the eliminator type: List OE In: | byLeft x-leq-y => x :-: insert xs' y While processing: insert
O problema é que, na classe
LinearOrder.Dec definição de
trichotomy fornecida usando o operador
|| , que, por sua vez, é determinado usando truncamento proposicional. Como já mencionado, para tipos pertencentes ao universo
\Prop , a correspondência com um padrão em Arend é permitida apenas se o tipo da expressão resultante for uma asserção (para a função acima, o resultado é do tipo
List OE e esse tipo é um conjunto).
Existe alguma maneira de contornar esse problema? A maneira mais fácil de resolver isso é alterar a definição da propriedade da tricotomia. Considere a seguinte definição de tricotomia, usando o tipo não truncado
Or vez do truncado
|| :
\func set-trichotomy {A : StrictPoset} (xy : A) => ((x = y) `Or` (x < y)) `Or` (y < x)
Esta definição
trichotomy em algo da definição original da
trichotomy através de
|| ? Por que usamos um tipo propositalmente truncado se isso apenas complica nossa vida e nos impede de usar a correspondência de padrões?
Vamos tentar responder à primeira pergunta para começar: para pedidos estritos do
StrictPoset diferença entre
trichotomy e
trichotomy set-trichotomy não é de todo. Observe que o tipo de
set-trichotomy é uma afirmação. Esse fato decorre do fato de que todas as três alternativas na definição de tricotomia são mutuamente exclusivas devido a axiomas de ordem, e cada um dos três tipos
x = y, x < y, y < x é em si uma afirmação (
x = y é uma afirmação, portanto como na definição da classe
BaseSet exigimos que a mídia
E um conjunto!).
\func set-trichotomy-isProp {A : StrictPoset} (xy : A) (l1 l2 : set-trichotomy xy): l1 = l2 \elim l1, l2 | inl (inl l1), inl (inl l2) => pmap (\lam z => inl (inl z)) (Path.inProp l1 l2) | inl (inr l1), inl (inr l2) => pmap (\lam z => inl (inr z)) (Path.inProp l1 l2) | inr l1, inr l2 => pmap inr (Path.inProp l1 l2) | inl (inl l1), inl (inr l2) => absurd (lt-eq-false l1 l2) | inl (inr l1), inl (inl l2) => absurd (lt-eq-false l2 l1) | inl (inl l1), inr l2 => absurd (lt-eq-false (inv l1) l2) | inr l1, inl (inl l2) => absurd (lt-eq-false (inv l2) l1) | inl (inr l1), inr l2 => absurd (lt-lt-false l1 l2) | inr l1, inl (inr l2) => absurd (lt-lt-false l2 l1) \where { \func lt-eq-false {A : StrictPoset} {xy : A} (l1 : x = y) (l2 : x < y) : Empty => A.<-irreflexive x (transport (x <) (inv l1) l2) \func lt-lt-false {A : StrictPoset} {xy : A} (l1 : x < y) (l2 : y < x) : Empty => A.<-irreflexive x (A.<-transitive _ _ _ l1 l2) }
Na lista acima,
absurd é a designação para o princípio ex falso quodlibet, definido no módulo
Logic . Como o tipo
Empty não possui construtores na definição (consulte a seção 1.2), não é necessário analisar os casos na definição de
absurd :
\func absurd {A : \Type} (x : Empty) : A
Como sabemos agora que
set-trichotomy é uma afirmação, podemos derivar a propriedade
set-trichotomy propriedade usual da
trichotomy em ordens decidíveis. Para fazer isso, podemos usar a construção
\return \level , que informa ao timer Arend que, neste ponto, combinar com o padrão é uma operação permitida (nesse caso, temos que mostrar a prova de que o resultado da função
set-trichotomy-property é uma instrução).
\func set-trichotomy-property {A : LinearOrder.Dec} (xy : A) : set-trichotomy xy => \case A.trichotomy xy \return \level (set-trichotomy xy) (set-trichotomy-isProp xy) \with { | byLeft x=y => inl (inl x=y) | byRight (byLeft x<y) => inl (inr x<y) | byRight (byRight y<x) => inr (y<x) }
Vamos agora tentar responder à segunda pergunta, a saber, por que é preferível usar construções não comuns, mas propositalmente truncadas, ao formular as propriedades de objetos matemáticos. Considere para isso um fragmento da definição de ordens lineares não lineares (definições completas de
Lattice e
TotalOrder podem ser encontradas no módulo
LinearOrder ):
\class TotalOrder \extends Lattice { | totality (xy : E) : x <= y || y <= x }
Vamos tentar imaginar agora como o significado da classe
TotalOrder mudaria se
TotalOrder a definição do campo da totalidade através da construção
Or não truncada.
\class BadTotalOrder \extends Lattice { | badTotality (xy : E) : (x <= y) `Or` (y <= x) }
Nesse caso, o tipo
(x <= y) `Or` (y <= x) não
(x <= y) `Or` (y <= x) mais uma declaração, porque no caso de valores iguais de
y ambas as alternativas na definição de
badTotality podem ser implementadas, e a escolha do ramo esquerdo ou direito na prova de
badTotality absolutamente arbitrária e permanece a critério do usuário - não há razão para preferir um construtor
Or a outro.
Agora está claro qual é a diferença entre
TotalOrder e
BadTotalOrder . Dois conjuntos ordenados
O1 O2 :
TotalOrder são sempre iguais quando é possível provar a igualdade dos conjuntos
O1.E, O2.E e as ordens
O1.<, O2.< Dados sobre eles (esta é a propriedade desejada). Por outro lado, para
O1 O2 :
BadTotalOrder é
BadTotalOrder provar a igualdade de
O1 e
O2 somente quando, além de todos os elementos
x de
E igualdade
O1.badTotality xx e
O2.badTotality xx .
Assim, verifica-se que a classe
BadTotalOrder intuitivamente precisa ser considerada não como um "conjunto ordenado linearmente", mas como um "conjunto ordenado linearmente junto com a escolha para cada elemento
x campo
E ramo esquerdo ou direito
Or na implementação de
badTotality xx ".
2.4 Algoritmo de classificação
Agora, implementamos o algoritmo de classificação. Vamos tentar corrigir a implementação ingênua da função de
insert da seção anterior usando a propriedade comprovada
set-trichotomy-property (neste caso, devido ao arranjo mais bem-sucedido de colchetes na definição de
set-trichotomy de
set-trichotomy , reduzimos o número de casos considerados).
\func insert {O : LinearOrder.Dec} (xs : List O) (y : O) : List O \elim xs | nil => y :-: nil | :-: x xs' => \case set-trichotomy-property xy \with { | inr y<x => y :-: x :-: xs' | inl x<=y => x :-: insert xs' y }
Agora vamos tentar implementar um análogo dessa definição para listas ordenadas. Usaremos a construção especial
\let … \in , que nos permite adicionar novas variáveis locais ao contexto.
\func insert {O : LinearOrder.Dec} (xs : SortedList O) (y : O) : SortedList O \elim xs | (nil, _) => (y :-: nil, singletonSorted) | (:-: x xs', xs-sorted) => \case set-trichotomy-property xy \with { | inr y<x => (y :-: x :-: xs', consSorted (byRight y<x) xs-sorted) | inl x<=y => \let (result, result-sorted) => insert (xs', tail-sorted x xs' xs-sorted) y \in (x :-: result, {?})
Deixamos na prova um fragmento incompleto (indicado pela expressão
{?} ) No local em que você deseja mostrar que a lista
x :-: result ordenada. Embora no contexto haja evidências da ordem da lista de
result , resta verificar se
x não excede o valor do primeiro elemento da lista de
result , o que não é tão fácil de seguir a partir das premissas do contexto (para ver todas as premissas no destino atual - é assim que chamamos ramo atual dos cálculos - é necessário solicitar a verificação do tipo na função de
insert ).
Acontece que a
insert muito mais fácil de implementar se provarmos a ordem da lista resultante em paralelo com a prova da especificação da
insert . Altere a assinatura do
insert e escreva a prova desta especificação nos casos mais simples:
\func insert {O : LinearOrder.Dec} (xs : SortedList O) (y : O) : \Sigma (ys : SortedList O) (InsertSpec xs.1 y ys.1) \elim xs | (nil, _) => ((y :-: nil, singletonSorted), insertedHere idp idp) | (:-: x xs', xs-sorted) => \case set-trichotomy-property xy \with { | inr y<x => ((y :-: x :-: xs', consSorted (byRight y<x) xs-sorted), insertedHere idp idp) | inl x<=y => \let ((result, result-sorted), result-spec) => insert (xs', tail-sorted x xs' xs-sorted) y \in ((x :-: result, {?}), insertedThere idp result-spec)
Para um único fragmento deixado sem prova, o Arend produzirá o seguinte valor de contexto:
Expected type: Sorted (x :-: (insert (\this, tail-sorted x \this \this) \this).1.1) Context: result-sorted : Sorted (insert (\this, tail-sorted \this \this \this) \this).1.1 xs-sorted : Sorted (x :-: xs') x : O x<=y : Or (x = y) (O.< xy) O : Dec result : List O y : O xs' : List O result-spec : InsertSpec xs' y (insert (xs', tail-sorted \this xs' \this) y).1.1
Para concluir a prova, teremos que usar
toda a potência do operador
\case : usaremos a correspondência de padrões com 5 variáveis diferentes e, como os tipos de algumas variáveis podem depender dos valores de outras variáveis, usaremos a correspondência de padrões dependentes.
A construção dos dois pontos indica explicitamente como o tipo de algumas variáveis comparadas depende dos valores de outras variáveis (portanto, no tipo de variáveis
xs-sorted, result-spec result-sorted em cada um dos
\case vez de
xs' e
result corresponderá às amostras correspondentes).
A construção
\return associa as variáveis usadas para combinar o padrão com o tipo de resultado esperado. Em outras palavras, no destino atual, em cada uma das cláusulas
\case , a amostra correspondente será substituída pela variável de
result . Sem essa construção, essa substituição não seria realizada e o objetivo de todas as cláusulas
\case coincidiria com o destino no lugar da própria
\case expression.
\func insert {O : LinearOrder.Dec} (xs : SortedList O) (y : O) : \Sigma (ys : SortedList O) (InsertSpec xs.1 y ys.1) \elim xs | (nil, _) => ((y :-: nil, singletonSorted), insertedHere idp idp) | (:-: x xs', xs-sorted) => \case set-trichotomy-property xy \with { | inr y<x => ((y :-: x :-: xs', consSorted (byRight y<x) xs-sorted), insertedHere idp idp) | inl x<=y => \let ((result, result-sorted), result-spec) => insert (xs', tail-sorted x xs' xs-sorted) y \in ((x :-: result, \case result \as result, xs' \as xs', xs-sorted : Sorted (x :-: xs'), result-spec : InsertSpec xs' y result, result-sorted : Sorted result \return Sorted (x :-: result) \with { | nil, _, _, _, _ => singletonSorted | :-: r rs, _, _, insertedHere y=r _, result-sorted => consSorted (transport (\lam z => (x = z) || (x < z)) y=r (Or-to-|| x<=y)) result-sorted | :-: r rs, :-: x' _, consSorted x<=x' _, insertedThere x2=r _, result-sorted => consSorted (transport (\lam z => (x = z) || (x < z)) x2=r x<=x') result-sorted }), insertedThere idp result-spec)
No bloco de código acima, os primeiros argumentos complexos do construtor
consSorted nos dois últimos parágrafos da comparação de padrões merecem comentários adicionais. Para entender o que essas duas expressões significam, as substituímos pela expressão
{?} E pedimos ao cronômetro Arend que determine os alvos em ambas as posições.
Você pode ver que, ali e ali, o destino atual é o tipo
(x = r) || O.< xr (x = r) || O.< xr . Além disso, no contexto do primeiro objetivo, existem premissas
x<=y : Or (x = y) (O.< xy) y=r : y = r
e no contexto das segundas instalações
x<=x' : (x = x') || O.< xx' x2=r : x' = r.
Intuitivamente claro: para provar o primeiro objetivo, basta substituir a variável
r pela instrução correta
Or (x = y) (O.< xy) e depois mudar para o tipo propositalmente truncado
|| usando a função
Or-to-|| definida na Seção 1.3 . Para provar o segundo objetivo, basta substituir em
(x = x') || O.< x x' (x = x') || O.< x x' vez da variável
x' variável
r .
Para formalizar a operação de substituição de expressão descrita, existe uma função de
transport especial na biblioteca Arend padrão. Considere a assinatura dela:
\func transport {A : \Type} (B : A -> \Type) {aa' : A} (p : a = a') (b : B a) : B a'
No nosso caso, em vez da variável
A precisamos substituir o tipo
OE (pode ser omitido explicitamente se os outros argumentos de
transport forem especificados) e, em vez de
B , a expressão
\lam (z : O) => (x = z) || (x < z) \lam (z : O) => (x = z) || (x < z) .
A implementação do algoritmo de classificação de inserção junto com a especificação não causa mais dificuldades particulares: para classificar a lista
x :-: xs' , primeiro classificamos o
insertSort da lista
xs' usando uma chamada recursiva para
insertSort e, em seguida, inserimos o elemento
x nessa lista, preservando a ordem de ajudar a acessar a função de
insert já implementada.
\func insertSort {O : LinearOrder.Dec} (xs : List O) : \Sigma (result : SortedList O) (Perm xs result.1) \elim xs | nil => ((nil, nilSorted), permTrivial idp) | :-: x xs' => \let | (ys, perm-xs'-ys) => insertSort xs' | (zs, zs-spec) => insert ys x \in (zs, permInsert perm-xs'-ys (insertedHere idp idp) zs-spec)
Cumprimos o objetivo inicial e implementamos a classificação das listas no Arend. Todo o código Arend fornecido neste parágrafo pode ser baixado em um arquivo a
partir daqui .
Pode-se perguntar como seria necessário alterar a implementação da função
insert se, em vez das ordens
LinearOrder.Dec estritas,
LinearOrder.Dec ordens
LinearOrder.Dec não estritas? Como lembramos, na definição da função de totalidade, o uso da operação truncada
|| foi bastante significativo, ou seja, essa definição não é equivalente a uma definição em que, em vez de
|| usado por
Or .
A resposta a esta pergunta é a seguinte: ainda é possível construir um análogo de
insert para
TotalOrder , no entanto, para isso, teríamos que provar que o tipo da função de
insert é uma declaração (isso nos permitiria na definição de
insert corresponder à amostra de acordo com a declaração de
totality xy ).
Em outras palavras, teríamos que provar que existe apenas uma lista ordenada até a igualdade, que é o resultado da inserção do elemento
y na lista ordenada
xs . É fácil perceber que esse é um fato verdadeiro, mas sua prova formal não é mais tão trivial. Deixamos a verificação desse fato como um exercício para o leitor interessado.
3. Observações finais
Nesta introdução, nos familiarizamos com as principais construções da linguagem Arend e também aprendemos como usar o mecanismo de classe. Conseguimos implementar o algoritmo mais simples, juntamente com a prova de sua especificação. Assim, mostramos que o Arend é bastante adequado para resolver problemas "cotidianos", como, por exemplo, verificação de programas.
Mencionamos longe de todos os recursos do Arend. Por exemplo, dissemos quase nada sobre
tipos com condições que permitem “colar” vários construtores de tipos com alguns valores de parâmetros especiais para esses construtores. Por exemplo, uma implementação do tipo inteiro no Arend é fornecida usando tipos com condições da seguinte maneira:
\data Int | pos Nat | neg Nat \with { zero => pos zero }
Essa definição diz que números inteiros consistem em duas cópias do tipo de números naturais, nos quais são identificados zeros "positivos" e "negativos". Essa definição é muito mais conveniente do que a definição da biblioteca Coq padrão, onde a "cópia negativa" dos números naturais deve ser "deslocada em um" para que essas cópias não se cruzem (é muito mais conveniente quando a notação
neg 1 significa o número -1, não -2) .
Não dissemos nada sobre o algoritmo para derivar níveis predicativos e homotópicos nas classes e suas instâncias. Também dificilmente mencionamos o tipo de intervalo
I , embora ele desempenhe um papel fundamental na teoria de tipos com intervalos, que são a base lógica de Arend. Para entender como esse tipo é importante, basta mencionar que, no tipo Arend, a igualdade é definida pelo conceito de intervalo. , , , (.. ).
:
,
HoTT JetBrains Research.