list - name - Demostrando igualdad de arroyos

name keywords

Question

Tengo un tipo de datos

data N a = N a [N a]

De rosales y instancia aplicativa.

instance Applicative N where
 pure a = N a (repeat (pure a))
 (N f xs) <*> (N a ys) = N (f a) (zipWith (<*>) xs ys)

y necesidad de probar las leyes aplicativas para ello. Sin embargo, lo puro crea árboles infinitamente profundos e infinitamente ramificados. Así, por ejemplo, al probar la ley del homomorfismo.

pure f <*> pure a = pure (f a)

Pensé que demostrando la igualdad.

zipWith (<*>) (repeat (pure f)) (repeat (pure a)) = repeat (pure (f a))

por la aproximación (o toma) lemma funcionaría. Sin embargo, mis intentos llevan a "círculos viciosos" en el paso inductivo. En particular, reduciendo

approx (n + 1) (zipWith (<*>) (repeat (pure f)) (repeat (pure a))

da

(pure f <*> pure a) : approx n (repeat (pure (f a)))

donde aprox es la función de aproximación. ¿Cómo puedo probar la igualdad sin una prueba coinductiva explícita?

Answer 1

¿Por qué necesitas coinducción? Sólo induct.

pure f <*> pure a = pure (f a)

También se puede escribir (es necesario probar la igualdad de izquierda y derecha)

N f [(pure f)] <*> N a [(pure a)] = N (f a) [(pure (f a))]

lo que le permite desactivar un término a la vez. Eso te da tu inducción.

Answer 2

El siguiente es un bosquejo de algo que creo que funciona y se mantiene en el nivel de la sintaxis programática y el razonamiento ecuacional.

La intuición básica es que es mucho más fácil razonar sobre la repeat x que sobre una transmisión (y, lo que es peor, una lista) en general.

uncons (repeat x) = (x, repeat x)

zipWithAp xss yss = 
    let (x,xs) = uncons xss
        (y,ys) = uncons yss
    in (x <*> y) : zipWithAp xs ys

-- provide arguments to zipWithAp
zipWithAp (repeat x) (repeat y) = 
    let (x'',xs) = uncons (repeat x)
        (y'',ys) = uncons (repeat y)
    in (x'' <*> y'') : zipWithAp xs ys

-- substitute definition of uncons...
zipWithAp (repeat x) (repeat y) = 
    let (x,repeat x) = uncons (repeat x)
        (y,repeat y) = uncons (repeat y)
    in (x <*> y) : zipWithAp (repeat x) (repeat y)

-- remove now extraneous let clause
zipWithAp (repeat x) (repeat y) = (x <*> y) : zipWithAp (repeat x) (repeat y)

-- unfold identity by one step
zipWithAp (repeat x) (repeat y) = (x <*> y) : (x <*> y) : zipWithAp (repeat x) (repeat y)

-- (co-)inductive step
zipWithAp (repeat x) (repeat y) = repeat (x <*> y)

Answer 3

Yo usaría la propiedad universal de los despliegues (ya que se repiten y se despliegan adecuadamente). Hay una discusión relacionada en mi blog . Pero es posible que también le gusten los artículos de Ralf Hinze sobre puntos de ICFP2008 únicos ICFP2008 (y el documento de JFP posterior).

(Solo verificando: ¿todos tus rosales son infinitamente anchos e infinitamente profundos? Supongo que las leyes no se sostendrán de otra manera).