functional programming - programing - Ayudar al comprobador de terminación de Agda

coq language programming

Question

Supongamos que definimos una función

f : N /to N
f 0 = 0
f (s n) = f (n/2) -- this / operator is implemented as floored division.

Agda pintará f en salmón porque no puede saber si n / 2 es menor que n. No sé cómo decirle nada al verificador de terminación de Agda. Veo que en la biblioteca estándar tienen una división de pisos por 2 y una prueba de que n / 2 <n. Sin embargo, todavía no veo cómo obtener el comprobador de terminación para darme cuenta de que se ha realizado una recursión en un subproblema más pequeño.

Answer 1

Después de aceptar la respuesta de Vitus, descubrí una forma diferente de lograr el objetivo de probar que una función termina en Agda, es decir, usar "tipos de tamaño". Estoy proporcionando mi respuesta aquí porque parece aceptable, y también para la crítica de los puntos débiles de esta respuesta.

Se describen los tipos de tamaños: http://arxiv.org/pdf/1012.4896.pdf

Se implementan en Agda, no solo MiniAgda; Consulte aquí: http://www2.tcs.ifi.lmu.de/~abel/talkAIM2008Sendai.pdf .

La idea es aumentar el tipo de datos con un tamaño que permita al tipógrafo comprobar la terminación más fácilmente. El tamaño se define en la biblioteca estándar.

open import Size

Definimos números naturales de tamaño:

data Nat : {i : Size} /to Set where
zero : {i : Size} /to Nat {/up i}
succ : {i : Size} /to Nat {i} /to Nat {/up i}

A continuación, definimos predecesor y resta (monus):

pred : {i : Size} → Nat {i} → Nat {i}
pred .{↑ i} (zero {i}) = zero {i}
pred .{↑ i} (succ {i} n) = n
sub : {i : Size} → Nat {i} → Nat {∞} → Nat {i}
sub .{↑ i} (zero {i}) n = zero {i}
sub .{↑ i} (succ {i} m) zero = succ {i} m
sub .{↑ i} (succ {i} m) (succ n) = sub {i} m n

Ahora, podemos definir la división a través del algoritmo de Euclides:

div : {i : Size} → Nat {i} → Nat → Nat {i}
div .{↑ i} (zero {i}) n = zero {i}
div .{↑ i} (succ {i} m) n = succ {i} (div {i} (sub {i} m n) n)
data ⊥ : Set where
record ⊤ : Set where
notZero : Nat → Set
notZero zero = ⊥
notZero _ = ⊤

Damos división para denominadores distintos de cero. Si el denominador es distinto de cero, entonces es de la forma, b + 1. Luego hacemos divPos a (b + 1) = div ab Ya que div ab devuelve el techo (a / (b + 1)).

divPos : {i : Size} → Nat {i} → (m : Nat) → (notZero m) → Nat {i}
divPos a (succ b) p = div a b
divPos a zero ()

Como auxiliar:

div2 : {i : Size} → Nat {i} → Nat {i}
div2 n = divPos n (succ (succ zero)) (record {})

Ahora podemos definir un método de dividir y conquistar para calcular el n-ésimo número de Fibonacci.

fibd : {i : Size} → Nat {i} → Nat
fibd zero = zero
fibd (succ zero) = succ zero
fibd (succ (succ zero)) = succ zero
fibd (succ n) with even (succ n)
fibd .{↑ i} (succ {i} n) | true =
let
-- When m=n+1, the input, is even, we set k = m/2
-- Note, ceil(m/2) = ceil(n/2)
k = div2 {i} n
fib[k-1] = fibd {i} (pred {i} k)
fib[k] = fibd {i} k
fib[k+1] = fib[k-1] + fib[k]
in
(fib[k+1] * fib[k]) + (fib[k] * fib[k-1])
fibd .{↑ i} (succ {i} n) | false =
let
-- When m=n+1, the input, is odd, we set k = n/2 = (m-1)/2.
k = div2 {i} n
fib[k-1] = fibd {i} (pred {i} k)
fib[k] = fibd {i} k
fib[k+1] = fib[k-1] + fib[k]
in
(fib[k+1] * fib[k+1]) + (fib[k] * fib[k])

Answer 2

El verificador de terminación de Agda solo verifica la recursión estructural (es decir, las llamadas que ocurren en argumentos estructuralmente más pequeños) y no hay manera de establecer que cierta relación (como _<_ ) implica que uno de los argumentos es estructuralmente más pequeño.

Digresión: problema similar ocurre con el comprobador de positividad. Considere el tipo de datos estándar de punto de referencia:

data μ_ (F : Set → Set) : Set where
fix : F (μ F) → μ F

Agda rechaza esto porque F puede no ser positivo en su primer argumento. Pero no podemos restringir μ para que solo tome funciones de tipo positivo, o mostrar que alguna función de tipo en particular es positiva.

¿Cómo mostramos normalmente que una función recursiva termina? Para los números naturales, este es el hecho de que si la llamada recursiva ocurre en un número estrictamente más pequeño, eventualmente tenemos que llegar a cero y la recursión se detiene; Para las listas lo mismo vale para su longitud; para conjuntos podríamos usar la relación de subconjunto estricto; y así. Observe que "número estrictamente más pequeño" no funciona para los enteros.

La propiedad que todas estas relaciones comparten se llama fundamento. Hablando de manera informal, una relación está bien fundada si no tiene ninguna cadena descendente infinita. Por ejemplo, < en los números naturales está bien fundamentado, porque para cualquier número n :

n > n - 1 > ... > 2 > 1 > 0

Es decir, la longitud de dicha cadena está limitada por n + 1 .

≤ en números naturales, sin embargo, no está bien fundado:

n ≥ n ≥ ... ≥ n ≥ ...

Y tampoco es < en enteros:

n > n - 1 > ... > 1 > 0 > -1 > ...

¿Nos ayuda esto? Resulta que podemos codificar lo que significa que una relación esté bien fundada en Agda y luego usarla para implementar su función.

Para simplificar, voy a hornear la relación _<_ en el tipo de datos. En primer lugar, debemos definir qué significa que un número sea accesible: n es accesible si todos m , de forma que m < n también son accesibles. Por supuesto, esto se detiene en n = 0 , porque no hay m modo que m < 0 y esta afirmación se mantiene de forma trivial.

data Acc (n : ℕ) : Set where
acc : (∀ m → m < n → Acc m) → Acc n

Ahora, si podemos demostrar que todos los números naturales son accesibles, entonces demostramos que < está bien fundado. ¿Por qué es así? Debe haber un número finito de constructores acc (es decir, no hay una cadena descendente infinita) porque Agda no nos deja escribir una recursión infinita. Ahora, puede parecer como si simplemente hubiéramos empujado el problema un paso más allá, ¡pero escribir la prueba de fundamento es en realidad estructuralmente recursivo!

Entonces, con eso en mente, aquí está la definición de < estar bien fundamentado:

WF : Set
WF = ∀ n → Acc n

Y la prueba de fundamento:

<-wf : WF
<-wf n = acc (go n)
where
go : ∀ n m → m < n → Acc m
go zero m ()
go (suc n) zero _ = acc λ _ ()
go (suc n) (suc m) (s≤s m<n) = acc λ o o<sm → go n o (trans o<sm m<n)

Fíjate que go es estructuralmente recursivo. trans puede ser importado así:

open import Data.Nat
open import Relation.Binary
open DecTotalOrder decTotalOrder
using (trans)

A continuación, necesitamos una prueba de que ⌊ n /2⌋ ≤ n :

/2-less : ∀ n → ⌊ n /2⌋ ≤ n
/2-less zero = z≤n
/2-less (suc zero) = z≤n
/2-less (suc (suc n)) = s≤s (trans (/2-less n) (right _))
where
right : ∀ n → n ≤ suc n
right zero = z≤n
right (suc n) = s≤s (right n)

Y finalmente, podemos escribir tu función f . Observe cómo de repente se vuelve estructuralmente recursivo gracias a Acc : las llamadas recursivas ocurren en argumentos con un constructor acc despegado.

f : ℕ → ℕ
f n = go _ (<-wf n)
where
go : ∀ n → Acc n → ℕ
go zero _ = 0
go (suc n) (acc a) = go ⌊ n /2⌋ (a _ (s≤s (/2-less _)))

Ahora, tener que trabajar directamente con Acc no es muy bueno. Y ahí es donde entra la respuesta de Dominique. Todas estas cosas que he escrito aquí ya se han hecho en la biblioteca estándar. Es más general (el tipo de datos Acc realidad está parametrizado sobre la relación) y le permite usar <-rec sin tener que preocuparse por Acc .

Mirando más de cerca, en realidad estamos bastante cerca de la solución genérica. Veamos qué obtenemos cuando parametrizamos la relación. Por simplicidad no estoy tratando con el polimorfismo del universo.

Una relación en A es solo una función que toma dos A s y devuelve Set (podríamos llamarlo predicado binario):

Rel : Set → Set₁
Rel A = A → A → Set

Podemos generalizar fácilmente Acc cambiando el codificado _<_ : ℕ → ℕ → Set una relación arbitraria sobre algún tipo A :

data Acc {A} (_<_ : Rel A) (x : A) : Set where
acc : (∀ y → y < x → Acc _<_ y) → Acc _<_ x

La definición de fundamento cambia en consecuencia:

WellFounded : ∀ {A} → Rel A → Set
WellFounded _<_ = ∀ x → Acc _<_ x

Ahora, dado que Acc es un tipo de datos inductivos como cualquier otro, deberíamos poder escribir su eliminador. Para los tipos inductivos, este es un pliegue (al igual que foldr es eliminador para listas): le decimos al eliminador qué hacer con cada caso de constructor y el eliminador aplica esto a toda la estructura.

En este caso, lo haremos bien con la variante simple:

foldAccSimple : ∀ {A} {_<_ : Rel A} {R : Set} →
(∀ x → (∀ y → y < x → R) → R) →
∀ z → Acc _<_ z → R
foldAccSimple {R = R} acc′ = go
where
go : ∀ z → Acc _ z → R
go z (acc a) = acc′ z λ y y<z → go y (a y y<z)

Si sabemos que _<_ está bien fundamentado, podemos omitir completamente el argumento Acc _<_ z _z, así que vamos a escribir un contenedor pequeño y conveniente:

recSimple : ∀ {A} {_<_ : Rel A} → WellFounded _<_ → {R : Set} →
(∀ x → (∀ y → y < x → R) → R) →
A → R
recSimple wf acc′ z = foldAccSimple acc′ z (wf z)

Y finalmente:

<-wf : WellFounded _<_
<-wf = {- same definition -}
<-rec = recSimple <-wf
f : ℕ → ℕ
f = <-rec go
where
go : ∀ n → (∀ m → m < n → ℕ) → ℕ
go zero _ = 0
go (suc n) r = r ⌊ n /2⌋ (s≤s (/2-less _))

Y de hecho, ¡esto se ve (y funciona) casi como el de la biblioteca estándar!

Aquí está la versión totalmente dependiente en caso de que se lo pregunte:

foldAcc : ∀ {A} {_<_ : Rel A} (P : A → Set) →
(∀ x → (∀ y → y < x → P y) → P x) →
∀ z → Acc _<_ z → P z
foldAcc P acc′ = go
where
go : ∀ z → Acc _ z → P z
go _ (acc a) = acc′ _ λ _ y<z → go _ (a _ y<z)
rec : ∀ {A} {_<_ : Rel A} → WellFounded _<_ →
(P : A → Set) → (∀ x → (∀ y → y < x → P y) → P x) →
∀ z → P z
rec wf P acc′ z = foldAcc P acc′ _ (wf z)

Answer 3

Hace unas semanas apareció una pregunta similar en la lista de correo de Agda y el consenso pareció ser inyectar el elemento Data.Bin en Data.Bin y luego utilizar la recursión estructural en esta representación que es adecuada para el trabajo en cuestión.

Puede encontrar el hilo completo aquí: http://comments.gmane.org/gmane.comp.lang.agda/5690

Answer 4

Me gustaría ofrecer una respuesta ligeramente diferente a las que se dieron anteriormente. En particular, quiero sugerir que en lugar de tratar de convencer de alguna manera al comprobador de terminación de que realmente, no, esta recursión está perfectamente bien, en lugar de eso, deberíamos intentar reificar la fundabilidad para que la recursión sea manifiestamente buena en virtud de siendo estructural.

La idea aquí es que el problema viene de no poder ver que n / 2 es de alguna manera una "parte" de n . La recursión estructural quiere dividir una cosa en sus partes inmediatas, pero la forma en que n / 2 es una "parte" de n es que dejamos caer todas las demás suc . Pero no es obvio desde el principio cuántos tirar, tenemos que mirar alrededor y tratar de alinear las cosas. Lo que sería bueno si tuviéramos algún tipo que tuviera constructores para "múltiples" suc s.

Para hacer que el problema sea un poco más interesante, intentemos definir la función que se comporta como

f : ℕ → ℕ
f 0 = 0
f (suc n) = 1 + (f (n / 2))

Es decir, debería ser el caso de que

f n = ⌈ log₂ (n + 1) ⌉

Ahora, naturalmente, la definición anterior no funcionará, por las mismas razones que tu f no funcionará. Pero pretendamos que lo hizo, y exploremos el "camino", por así decirlo, que el argumento tomaría los números naturales. Supongamos que nos fijamos en n = 8 :

f 8 = 1 + f 4 = 1 + 1 + f 2 = 1 + 1 + 1 + f 1 = 1 + 1 + 1 + 1 + f 0 = 1 + 1 + 1 + 1 + 0 = 4

entonces el "camino" es 8 -> 4 -> 2 -> 1 -> 0 . ¿Qué hay de, digamos, 11?

f 11 = 1 + f 5 = 1 + 1 + f 2 = ... = 4

entonces el "camino" es 11 -> 5 -> 2 -> 1 -> 0 .

Bien, naturalmente, lo que está sucediendo aquí es que en cada paso o bien estamos dividiendo por 2, o restando uno y dividiendo por 2. Cada número natural mayor que 0 puede descomponerse de manera única de esta manera. Si es par, divide por dos y continúa, si es impar, resta uno y divide por dos y continúa.

Así que ahora podemos ver exactamente cómo debería ser nuestro tipo de datos. Necesitamos un tipo que tenga un constructor que signifique "dos veces la cantidad de suc " y otro que signifique "dos veces más suc más uno", así como, por supuesto, un constructor que signifique "cero suc s":

data Decomp : ℕ → Set where
zero : Decomp zero
2*_ : ∀ {n} → Decomp n → Decomp (n * 2)
2*_+1 : ∀ {n} → Decomp n → Decomp (suc (n * 2))

Ahora podemos definir la función que descompone un número natural en la Decomp que le corresponde:

decomp : (n : ℕ) → Decomp n
decomp zero = zero
decomp (suc n) = decomp n +1

Ayuda a definir +1 para Decomp s:

_+1 : {n : ℕ} → Decomp n → Decomp (suc n)
zero +1 = 2* zero +1
(2* d) +1 = 2* d +1
(2* d +1) +1 = 2* (d +1)

Dado un Decomp , podemos aplanarlo en un número natural que ignora las distinciones entre 2*_ y 2*_+1 :

flatten : {n : ℕ} → Decomp n → ℕ
flatten zero = zero
flatten (2* p) = suc (flatten p)
flatten (2* p +1 = suc (flatten p)

Y ahora es trivial definir f :

f : ℕ → ℕ
f n = flatten (decomp n)

Felizmente pasa el comprobador de terminación sin problemas, porque en realidad nunca recurrimos a la problemática n / 2 . En su lugar, convertimos el número a un formato que representa directamente su ruta a través del espacio numérico de una manera estructuralmente recursiva.

Editar Se me ocurrió hace solo un momento que Decomp es una representación de números binarios little-endian. 2*_ es "agregar 0 al final / cambio a la izquierda 1 bit" y 2*_+1 es "agregar 1 al final / cambio a la izquierda 1 bit y agregar uno". Así que el código anterior es realmente acerca de mostrar que los números binarios son estructuralmente recursivos y divididos por 2, ¡lo que deberían ser! Eso lo hace mucho más fácil de entender, creo, pero no quiero cambiar lo que ya escribí, así que podríamos hacer un cambio de nombre aquí: Decomp ~> Binary , 2*_ ~> _,zero , 2*_+1 ~> _,one , natToBin ~> natToBin , flatten ~> countBits .

Answer 5

No puede hacer esto directamente: el verificador de terminación de Agda solo considera que la recursión está bien en los argumentos que son sintácticamente más pequeños. Sin embargo, la biblioteca estándar de Agda proporciona algunos módulos para probar la terminación utilizando un orden bien fundado entre los argumentos de las funciones. El orden estándar en números naturales es tal orden y se puede utilizar aquí.

Usando el código en Inducción. *, Puede escribir su función de la siguiente manera:

open import Data.Nat
open import Induction.WellFounded
open import Induction.Nat
s≤′s : ∀ {n m} → n ≤′ m → suc n ≤′ suc m
s≤′s ≤′-refl = ≤′-refl
s≤′s (≤′-step lt) = ≤′-step (s≤′s lt)
proof : ∀ n → ⌊ n /2⌋ ≤′ n
proof 0 = ≤′-refl
proof 1 = ≤′-step (proof zero)
proof (suc (suc n)) = ≤′-step (s≤′s (proof n))
f : ℕ → ℕ
f = <-rec (λ _ → ℕ) helper
where
helper : (n : ℕ) → (∀ y → y <′ n → ℕ) → ℕ
helper 0 rec = 0
helper (suc n) rec = rec ⌊ n /2⌋ (s≤′s (proof n))

Encontré un artículo con alguna explicación here . Pero puede haber mejores referencias por ahí.

Answer 6

Se puede evitar usar una recursión bien fundada. Digamos que desea una función, que aplica ⌊_/2⌋ a un número, hasta que llegue a 0 y recopile los resultados. Con el pragma {-# TERMINATING #-} se puede definir así:

{-# TERMINATING #-}
⌊_/2⌋s : ℕ -> List ℕ
⌊_/2⌋s 0 = []
⌊_/2⌋s n = n ∷ ⌊ ⌊ n /2⌋ /2⌋s

La segunda cláusula es equivalente a

⌊_/2⌋s n = n ∷ ⌊ n ∸ (n ∸ ⌊ n /2⌋) /2⌋s

Es posible hacer ⌊_/2⌋s estructuralmente recursivo al enmarcar esta resta:

⌊_/2⌋s : ℕ -> List ℕ
⌊_/2⌋s = go 0 where
go : ℕ -> ℕ -> List ℕ
go _ 0 = []
go 0 (suc n) = suc n ∷ go (n ∸ ⌈ n /2⌉) n
go (suc i) (suc n) = go i n

go (n ∸ ⌈ n /2⌉) n es una versión simplificada de go (suc n ∸ ⌊ suc n /2⌋ ∸ 1) n

Algunas pruebas:

test-5 : ⌊ 5 /2⌋s ≡ 5 ∷ 2 ∷ 1 ∷ []
test-5 = refl
test-25 : ⌊ 25 /2⌋s ≡ 25 ∷ 12 ∷ 6 ∷ 3 ∷ 1 ∷ []
test-25 = refl

Ahora digamos que desea una función, que aplica ⌊_/2⌋ a un número, hasta que llega a 0 , y suma los resultados. Es simplemente

⌊_/2⌋sum : ℕ -> ℕ
⌊ n /2⌋sum = go ⌊ n /2⌋s where
go : List ℕ -> ℕ
go [] = 0
go (n ∷ ns) = n + go ns

Así que simplemente podemos ejecutar nuestra recursión en una lista, que contiene valores, producidos por la función ⌊_/2⌋s .

La versión más concisa es

⌊ n /2⌋sum = foldr _+_ 0 ⌊ n /2⌋s

Y de vuelta al buen estado de ánimo.

open import Function
open import Relation.Nullary
open import Relation.Binary
open import Induction.WellFounded
open import Induction.Nat
calls : ∀ {a b ℓ} {A : Set a} {_<_ : Rel A ℓ} {guarded : A -> Set b}
-> (f : A -> A)
-> Well-founded _<_
-> (∀ {x} -> guarded x -> f x < x)
-> (∀ x -> Dec (guarded x))
-> A
-> List A
calls {A = A} {_<_} f wf smaller dec-guarded x = go (wf x) where
go : ∀ {x} -> Acc _<_ x -> List A
go {x} (acc r) with dec-guarded x
... | no _ = []
... | yes g = x ∷ go (r (f x) (smaller g))

Esta función hace lo mismo que la función ⌊_/2⌋s , es decir, produce valores para llamadas recursivas, pero para cualquier función, que cumpla ciertas condiciones.

Mira la definición de go . Si x no está guarded , entonces devuelva [] . De lo contrario, agregue x y llame a fx (podríamos escribir go {x = fx} ... ), que es estructuralmente más pequeño.

Podemos redefinir ⌊_/2⌋s en términos de calls :

⌊_/2⌋s : ℕ -> List ℕ
⌊_/2⌋s = calls {guarded = ?} ⌊_/2⌋ ? ? ?

⌊ n /2⌋s devuelve [] , solo cuando n es 0 , entonces guarded = λ n -> n > 0 .

Nuestra relación bien fundada se basa en _<′_ y se define en el módulo Induction.Nat como <-well-founded .

Entonces tenemos

⌊_/2⌋s = calls {guarded = λ n -> n > 0} ⌊_/2⌋ <-well-founded {!!} {!!}

El tipo del siguiente agujero es {x : ℕ} → x > 0 → ⌊ x /2⌋ <′ x

Podemos probar fácilmente esta proposición:

open import Data.Nat.Properties
suc-⌊/2⌋-≤′ : ∀ n -> ⌊ suc n /2⌋ ≤′ n
suc-⌊/2⌋-≤′ 0 = ≤′-refl
suc-⌊/2⌋-≤′ (suc n) = s≤′s (⌊n/2⌋≤′n n)
>0-⌊/2⌋-<′ : ∀ {n} -> n > 0 -> ⌊ n /2⌋ <′ n
>0-⌊/2⌋-<′ {suc n} (s≤s z≤n) = s≤′s (suc-⌊/2⌋-≤′ n)

El tipo del último agujero es (x : ℕ) → Dec (x > 0) , podemos llenarlo con _≤?_ 1 .

Y la definición final es

⌊_/2⌋s : ℕ -> List ℕ
⌊_/2⌋s = calls ⌊_/2⌋ <-well-founded >0-⌊/2⌋-<′ (_≤?_ 1)

Ahora puede consultar en una lista, producida por ⌊_/2⌋s , sin ningún problema de terminación.