Demostrando la igualdad de las corrientes

que tiene un tipo de datosDemostrando la igualdad de las corrientes

data N a = N a [N a]

de rosales y la instancia Aplicativo

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

y la necesidad de demostrar las leyes aplicativos para ello. Sin embargo, pure crea árboles infinitamente profundos e infinitamente ramificados. Así, por ejemplo, para demostrar la ley homomorfismo

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

pensé que demuestra la igualdad

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

por la aproximación (más o menos) lema funcionaría. Sin embargo, mis intentos conducen a "círculos viciosos" en el paso inductivo. En particular, la reducción de

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

(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?

Fuente

2011-03-03 danportin

¿Por qué quieres para probarlo sin necesidad de utilizar coinduction? Así como la inducción es el método de prueba natural para datos como listas/árboles finitos, la coinducción es el método de prueba natural para codata, como las corrientes o sus "árboles infinitamente profundos e infinitamente ramificados". –

En particular, porque la prueba funciona en el nivel de "sintaxis del programa". Una prueba de bisimilaridad no lo hace. – danportin

esto parece un buen candidato para el sitio cstheory stackexchange, especialmente si lo declaró en términos ligeramente más generales/formales. – sclv

El siguiente es un esbozo 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 repeat x que razonar acerca de un flujo (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)

Fuente

2011-03-07 16:43:20 sclv

¿Por qué es necesario coinduction? Solo induct.

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

también se puede escribir (hay que probar la izquierda y la igualdad derecha)

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

el cual le permite a uno fuera de plazo a la vez. Eso te da tu inducción.

Fuente

2011-03-10 18:40:42 jbolden1517

Creo que te estás perdiendo el punto.En realidad obtienes 'N f (repeat $ pure f) <*> N a (repite $ pure a) = N (fa) (zipWith (<*>) (repite $ pure f) (repite $ pure a))' que conduce directamente al la igualdad que Danportin quiere probar en primer lugar ... – sclv

Usaría la propiedad universal de despliegues (ya que la repetición y una cremallera adecuadamente desenrollada se desarrollan ambas). Hay una discusión relacionada on my blog. Pero también le pueden interesar los artículos de Ralf Hinze sobre los puntos de fijación únicos ICFP2008 (y el posterior documento de JFP).

(sólo la comprobación: todas sus rosales son infinitamente amplia e infinitamente profunda supongo que las leyes no llevará a cabo de otra manera?).

Fuente

2011-05-18 16:11:44

Demostrando la igualdad de las corrientes

Respuesta

Cuestiones relacionadas