En la primera parte del artículo sobre el lenguaje Arend, examinamos los tipos inductivos más simples, funciones recursivas, clases y conjuntos.
2. Ordenar listas en Arend
2.1 Listas ordenadas en Arend
Definimos el tipo de listas ordenadas como un par que consiste en una lista y prueba de su orden. Como ya dijimos, en Arend, los pares dependientes se definen usando la palabra clave
\Sigma . Damos la definición del tipo
ordenado a través de la comparación con la muestra, inspirada en la definición del
artículo ya 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 pudo inferir automáticamente que el tipo
Sorted está contenido en el universo
\Prop . Esto sucedió porque los tres patrones en la definición
Sorted son mutuamente excluyentes, y el constructor
consSorted tiene dos parámetros, los cuales pertenecen a
\Prop .
Probemos alguna propiedad obvia del predicado ordenado, digamos que la cola de una lista ordenada es en sí misma una lista ordenada (esta propiedad nos será útil en el 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
En la
tail-sorted utilizamos la coincidencia de patrones en la lista
xs y el predicado
tail-sorted al mismo tiempo, además, utilizamos el
carácter de omisión "_", que puede sustituirse por variables no utilizadas.
Uno puede preguntar si es posible en Arend probar la propiedad de las listas ordenadas, mencionadas en la sección 1.3 como un ejemplo de un hecho que no puede probarse en Agda sin anotaciones de inmaterialidad. Recuerde que esta propiedad afirma que para probar la igualdad de las listas ordenadas definidas a través de pares dependientes, es suficiente verificar la igualdad de los primeros componentes de los pares.
Se argumenta que en Arend esta propiedad se obtiene fácilmente como consecuencia de la construcción
inProp mencionada anteriormente y la propiedad de extensionalidad para pares
SigmaExt dependientes.
\func sorted-equality {A : LinearOrder.Dec} (l1 l2 : SortedList A) (P : l1.1 = l2.1) : l1 = l2 => SigmaPropExt Sorted l1 l2 P
La propiedad
SigmaPropExt prueba en el módulo
Paths de la biblioteca estándar, muchos otros hechos del segundo capítulo
del libro HoTT , incluida la
propiedad de extensibilidad funcional , también se prueban allí.
El operador
.n usa en Arend para acceder al proyector de tipo sigma con el número n (en nuestro caso, el tipo sigma es
SortedList A , y la expresión
l1.1 significa que el primer componente de este tipo es una expresión de tipo
List A ).
2.2 Implementación de la propiedad "be permutation"
Ahora intentemos implementar la función de clasificación de listas en Arend. Naturalmente, no queremos tener una implementación simple del algoritmo de clasificación, sino una implementación junto con una prueba de algunas propiedades.
Claramente, este algoritmo debe tener al menos 2 propiedades:
1. El resultado del algoritmo debe ser una lista ordenada.
2. La lista resultante debe ser una permutación de la lista original.
Primero, intentemos implementar la propiedad "be permutation" de las listas en Arend. Para hacer esto, adaptamos la definición tomada
de aquí 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)
El predicado
InsertSpec introducido por nosotros tiene el siguiente significado intuitivo:
InsertSpec xs a ys significa exactamente que la lista
ys es el resultado de insertar el elemento a dentro de la lista
xs (en cualquier posición). Por lo tanto,
InsertSpec se puede tomar como una especificación de la función de inserción.
Está claro que el tipo de datos
Perm realmente define la relación "ser permutación": el constructor
permInsert exactamente que
xs e
ys son mutuamente permutables si se obtienen
xs e
ys insertando el mismo elemento a en algunas listas
xs' e
ys' longitudes más cortas, que ya son permutaciones entre sí.
Para nuestra definición de la propiedad "ser permutación", es fácil verificar la propiedad de simetría.
\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
La propiedad de transitividad también se satisface para
Perm , pero su verificación es mucho más complicada. Dado que esta propiedad no juega ningún papel en la implementación de nuestro algoritmo de clasificación, lo dejamos al lector como un ejercicio.
\func Perm-transitive {A : \Set} (xs ys zs : List A) (P1 : Perm xs ys) (P2 : Perm ys zs) : Perm xs zs => {?}
2.3 Cambio en los niveles de homotopía en comparación con la muestra
Ahora intentemos implementar una función que inserte un elemento en una lista ordenada para que la lista resultante permanezca ordenada. Comencemos con la siguiente implementación ingenua.
\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' }
La construcción
\case permite la coincidencia con una muestra de una expresión arbitraria (
\elim se puede usar en el nivel más alto de una definición de función y solo para sus parámetros). Si le pide a Arend que verifique el tipo de
insert , se mostrará el siguiente mensaje de error.
[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
El problema es que en la clase
LinearOrder.Dec , la
LinearOrder.Dec define utilizando
|| , que, a su vez, se determina utilizando el truncamiento proposicional. Como ya se mencionó, para los tipos que pertenecen al universo
\Prop , la coincidencia con un patrón en Arend solo se permite si el tipo de la expresión resultante es en sí misma una aserción (para la función anterior, el resultado es de tipo
List OE , y este tipo es un conjunto).
¿Hay alguna forma de evitar este problema? La forma más fácil de resolver esto es cambiar la definición de la propiedad de la tricotomía. Considere la siguiente definición de tricotomía, utilizando el tipo no truncado
Or lugar del truncado
|| :
\func set-trichotomy {A : StrictPoset} (xy : A) => ((x = y) `Or` (x < y)) `Or` (y < x)
¿Esta definición
trichotomy en algo de la definición de
trichotomy original a través de
|| ? ¿Por qué incluso usamos un tipo truncado proposicionalmente si solo complica nuestra vida y nos impide usar la coincidencia de patrones?
Intentemos responder la primera pregunta para empezar: para órdenes estrictas de
StrictPoset diferencia entre
trichotomy y
trichotomy set-trichotomy no es en absoluto. Tenga en cuenta que el tipo
set-trichotomy es una declaración. Este hecho se deduce del hecho de que las tres alternativas en la definición de tricotomía son mutuamente excluyentes debido a los axiomas de orden, y cada uno de los tres tipos
x = y, x < y, y < x es en sí mismo una declaración (
x = y es una declaración, por lo que como en la definición de la clase
BaseSet que los medios
E un 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) }
En la lista anterior,
absurd es la designación para el principio ex falso quodlibet, que se define en el módulo
Lógico . Dado que el tipo
Empty no tiene constructores en la definición (ver sección 1.2), no es necesario pasar por los casos en la definición de
absurd :
\func absurd {A : \Type} (x : Empty) : A
Dado que ahora sabemos que
set-trichotomy es una declaración, podemos derivar la propiedad
set-trichotomy propiedad habitual de
trichotomy de órdenes decidibles. Para hacer esto, podemos usar la construcción
\return \level , que le dice al temporizador Arend que en este punto la coincidencia de patrones es una operación permitida (en este caso, tenemos que demostrar que el resultado de la función
set-trichotomy-property es una declaración).
\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) }
Tratemos ahora de responder la segunda pregunta, a saber, por qué, al formular las propiedades de los objetos matemáticos, es preferible usar construcciones no ordinarias, sino truncadas proposicionalmente. Considere para esto un fragmento de la definición de órdenes lineales no lineales (las definiciones completas de
Lattice y
TotalOrder se pueden encontrar en el módulo
LinearOrder ):
\class TotalOrder \extends Lattice { | totality (xy : E) : x <= y || y <= x }
Tratemos de imaginar ahora cómo
TotalOrder el significado de la clase
TotalOrder si
TotalOrder la definición del campo de totalidad a través de la construcción
Or truncada.
\class BadTotalOrder \extends Lattice { | badTotality (xy : E) : (x <= y) `Or` (y <= x) }
En este caso, el tipo
(x <= y) `Or` (y <= x) ya no es una declaración, porque en caso de valores iguales de
x e
y ambas alternativas en la definición de
badTotality se pueden implementar, y la elección de la rama izquierda o derecha en la prueba de
badTotality absolutamente arbitraria y queda a discreción del usuario; no hay razón para preferir uno
Or un constructor a otro.
Ahora está claro cuál es la diferencia entre
TotalOrder y
BadTotalOrder . Dos conjuntos ordenados
O1 O2 :
TotalOrder siempre son iguales cuando es posible demostrar la igualdad de los conjuntos
O1.E, O2.E y las órdenes
O1.<, O2.< Dado en ellos (esta es la propiedad deseada). Por otro lado, para
O1 O2 :
BadTotalOrder es
BadTotalOrder probar la igualdad de
O1 y
O2 solo cuando, además de todos los elementos
x de
E O1.badTotality xx E igualdad
O1.badTotality xx y
O2.badTotality xx .
Por lo tanto, resulta que la clase
BadTotalOrder intuitivamente debe considerarse no como un "conjunto ordenado linealmente", sino como un "conjunto ordenado linealmente junto con la elección para cada elemento
x campo
E rama izquierda o derecha
Or en la implementación de
badTotality xx ".
2.4 Algoritmo de clasificación
Ahora procedemos a implementar el algoritmo de clasificación. Tratemos de arreglar la implementación ingenua de la función de
insert de la sección anterior utilizando la
set-trichotomy-property probada
set-trichotomy-property (en este caso, debido a la disposición más exitosa de los corchetes en la definición de
set-trichotomy , hemos reducido el 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 }
Ahora intentemos implementar un análogo de esta definición para las listas ordenadas. Usaremos la construcción especial
\let … \in , que nos permite agregar nuevas variables locales al 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, {?})
Dejamos en la prueba un fragmento incompleto (indicado por la expresión
{?} ) En el lugar donde desea mostrar que la lista
x :-: result ordenado. Aunque en el contexto hay evidencia del orden de la lista de
result , nos queda por verificar que
x no exceda el valor del primer elemento de la lista de
result , que no es tan fácil de seguir desde las premisas en el contexto (para ver todas las premisas en el objetivo actual - esto es lo que llamamos rama actual de los cálculos: debe solicitar la verificación de tipo desde la función de
insert ).
Resulta que la
insert mucho más fácil de implementar si probamos el orden de la lista resultante en paralelo con la prueba de la especificación de
insert . Cambie la firma de
insert y escriba la prueba de esta especificación en los casos más 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 un solo fragmento que queda sin prueba, Arend generará el siguiente 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 completar la prueba, tendremos que usar
toda la potencia del operador
\case : utilizaremos la coincidencia de patrones con 5 variables diferentes, y dado que los tipos de algunas variables pueden depender de los valores de otras variables, utilizaremos la coincidencia de patrones dependientes.
La construcción de dos puntos indica explícitamente cómo el tipo de algunas variables a comparar depende del valor de otras variables (por lo tanto, en el tipo de variables
xs-sorted, result-spec y
result-sorted en cada
\case lugar de
xs' y
result coincidirá con las muestras correspondientes).
La construcción
\return asocia las variables utilizadas para hacer coincidir el patrón con el tipo de resultado esperado. En otras palabras, en el objetivo actual, en cada una de las cláusulas
\case , la muestra correspondiente se sustituirá por la variable de
result . Sin esta construcción, dicho reemplazo no se llevaría a cabo, y el objetivo de todas las cláusulas
\case coincidiría con el objetivo en lugar de la expresión
\case misma.
\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)
En el bloque de código anterior, los primeros argumentos complejos del constructor
consSorted en los últimos dos párrafos de la comparación de patrones merecen un comentario adicional. Para entender qué significan ambas expresiones, las reemplazamos con la expresión
{?} Y le pedimos al temporizador Arend que determine los objetivos en ambas posiciones.
Puede ver que tanto allí como allí el objetivo actual es el tipo
(x = r) || O.< xr (x = r) || O.< xr . Además, en el contexto del primer objetivo, hay premisas
x<=y : Or (x = y) (O.< xy) y=r : y = r
y en el contexto del segundo - premisas
x<=x' : (x = x') || O.< xx' x2=r : x' = r.
Intuitivamente claro: para probar el primer objetivo, es suficiente sustituir la variable
r en el enunciado correcto
Or (x = y) (O.< xy) , y luego cambiar al tipo truncado proposicionalmente
|| utilizando la función
Or-to-|| definida en la Sección 1.3 . Para probar el segundo objetivo, simplemente sustituya en
(x = x') || O.< x x' (x = x') || O.< x x' lugar de la variable
x' variable
r .
Para formalizar la operación de sustitución de expresión descrita, existe una función de
transport especial en la biblioteca estándar de Arend. Considere su firma:
\func transport {A : \Type} (B : A -> \Type) {aa' : A} (p : a = a') (b : B a) : B a'
En nuestro caso, el tipo
OE debe ser sustituido por la variable
A (puede omitirse explícitamente si se especifican los otros argumentos de
transport ), y la expresión
\lam (z : O) => (x = z) || (x < z) \lam (z : O) => (x = z) || (x < z) .
La implementación del algoritmo de clasificación de inserción junto con la especificación ya no causa dificultades particulares: para ordenar la lista
x :-: xs' , primero ordenamos la cola de la lista
xs' usando una llamada recursiva a
insertSort , y luego insertamos el elemento
x dentro de esta lista mientras conservamos el orden cuando Ayuda a acceder a la función de
insert ya 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)
Cumplimos el objetivo inicial e implementamos la clasificación de las listas en Arend. Todo el código Arend que se proporciona en este párrafo se puede descargar en un archivo
desde aquí .
Uno podría preguntarse cómo tendría que cambiar la implementación de la función de
insert si en lugar de las órdenes estrictas
LinearOrder.Dec utilizamos las órdenes no estrictas
TotalOrder ? Como recordamos, en la definición de la función de totalidad, el uso de la operación truncada
|| fue bastante significativo, es decir, esta definición no es equivalente a una definición en la que en lugar de
|| utilizado por
Or .
La respuesta a esta pregunta es la siguiente: todavía es posible construir un análogo de
insert para
TotalOrder , sin embargo, para esto tendríamos que demostrar que el tipo de la función de
insert es una declaración (esto nos permitiría en la definición de
insert hacer una comparación con la muestra de acuerdo con la declaración de
totality xy ).
En otras palabras, tendríamos que demostrar que solo hay una lista ordenada hasta la igualdad, que es el resultado de insertar el elemento
y en la lista ordenada
xs . Es fácil ver que este es un hecho cierto, pero su prueba formal ya no es tan trivial. Dejamos la verificación de este hecho como un ejercicio para el lector interesado.
3. Observaciones finales
En esta introducción, nos familiarizamos con las construcciones principales del lenguaje Arend, y también aprendimos cómo usar el mecanismo de clase. Logramos implementar el algoritmo más simple junto con la prueba de su especificación. Por lo tanto, hemos demostrado que Arend es bastante adecuado para resolver problemas "cotidianos", como, por ejemplo, la verificación de programas.
Hemos mencionado lejos de todas las características y características de Arend. Por ejemplo, no dijimos casi nada acerca de los
tipos con condiciones que le permiten "pegar" varios constructores de tipos con algunos valores de parámetros especiales para estos constructores. Por ejemplo, se proporciona una implementación del tipo entero en Arend usando tipos con las condiciones siguientes:
\data Int | pos Nat | neg Nat \with { zero => pos zero }
Esta definición dice que los enteros consisten en dos copias del tipo de números naturales, en los que se identifican ceros "positivos" y "negativos". Dicha definición es mucho más conveniente que la definición de la biblioteca estándar de Coq, donde la "copia negativa" de los números naturales debe ser "desplazada por uno" para que estas copias no se crucen (es mucho más conveniente cuando la notación
neg 1 significa el número -1, no -2) .
No dijimos nada sobre el algoritmo para derivar niveles predicativos y de homotopía en las clases y sus instancias. Tampoco mencionamos el tipo de intervalo
I , aunque juega un papel clave en la teoría de los tipos con intervalos, que son la base lógica de Arend. Para comprender lo importante que es este tipo, es suficiente mencionar que en Arend la igualdad de tipos se define a través del concepto de intervalo. , , , (.. ).
:
,
HoTT JetBrains Research.