haskell - ¿Hay alguna manera de realizar una función de tipo((a-> b)-> b)-> O ab?

logic

Question

Las proposiciones (P -> Q) -> Q y P // Q son equivalentes.

¿Hay alguna manera de presenciar esta equivalencia en Haskell?

from :: Either a b -> ((a -> b) -> b)
from x = case x of
         Left a -> /f -> f a
         Right b -> /f -> b

to :: ((a -> b) -> b) -> Either a b
to = ???

tal que

from . to = id from . to = id y to . from = id to . from = id ?

Answer 1

Las proposiciones (P -> Q) -> Q y P // Q son equivalentes.

Esto es cierto en la lógica clásica, pero no en la lógica constructiva.

En la lógica constructiva no tenemos la ley del medio excluido , es decir, no podemos comenzar a pensar con "o P es verdadero o P no es verdadero".

Clásicamente razonamos como:

• si P es verdadero (es decir, tenemos ( x :: P )), entonces devuelve Left x .
• si P es falso, entonces en Haskell hablar tendremos nx :: P -> Void Función nx :: P -> Void . Entonces absurd . nx :: P -> Q absurd . nx :: P -> Q (podemos alcanzar cualquier tipo de pico, tomamos Q ) y llamamos dado f :: (P -> Q) -> Q) con absurd . nx absurd . nx para obtener el valor de tipo Q

El problema es que no hay una función general de un tipo:

lem :: forall p. Either p (p -> Void)

Para algunos tipos concretos hay, por ejemplo, Bool está habitado para que podamos escribir

lemBool :: Either Bool (Bool -> Void)
lemBool = Left True -- arbitrary choice

pero de nuevo, en general no podemos.

Answer 2

Como otros han señalado, esto es imposible porque no tenemos la ley del medio excluido. Déjame pasar por eso un poco más explícitamente. Supongamos que tenemos

bogus :: ((a -> b) -> b) -> Either a b

y establecemos b ~ Void . Entonces tenemos

-- chi calls this `impossible2`.
double_neg_elim :: ((a -> Void) -> Void) -> a
bouble_neg_elim f = case bogus f of
             Left a -> a
             Right v -> absurd v

Ahora, demostremos la doble negación de la ley del medio excluido aplicada a una proposición específica .

nnlem :: forall a. (Either a (a -> Void) -> Void) -> Void
nnlem f = not_not_a not_a
  where
    not_a :: a -> Void
    not_a = f . Left

    not_not_a :: (a -> Void) -> Void
    not_not_a = f . Right

Y ahora

lem :: Either a (a -> Void)
lem = double_neg_elim nnlem

claramente no puede existir porque puede codificar la proposición de que cualquier configuración de máquina de Turing que elija se detendrá.

Verifiquemos que lem sea ​​suficiente:

bogus :: forall a b. ((a -> b) -> b) -> Either a b
bogus f = case lem @a of
  Left a -> Left a
  Right na -> Right $ f (absurd . na)

Answer 3

No tengo idea de si esto es válido en términos de lógica, o qué significa para su equivalencia, pero sí, es posible escribir dicha función en Haskell.

Para construir un Either ab , necesitamos un valor a o a b . No tenemos ninguna forma de construir un valor a, pero tenemos una función que devuelve un b que podríamos llamar. Para hacer eso, necesitamos proporcionar una función que convierta a a en a b , pero dado que los tipos son desconocidos, en el mejor de los casos podríamos hacer una función que devuelva una constante b . Para obtener ese valor b , no podemos construirlo de otra manera que antes, por lo que esto se convierte en un razonamiento circular, y podemos resolverlo simplemente creando un punto de fijación :

to :: ((a -> b) -> b) -> Either a b
to f = let x = f (/_ -> x) in Right x

Answer 4

No, es imposible Considere el caso especial donde Q = Void .

Either PQ es Either P Void , que es isomorfo a P

iso :: P -> Either P Void
iso = Left

iso_inv :: Either P Void -> P
iso_inv (Left p)  = p
iso_inv (Right q) = absurd q

Por lo tanto, si tuviéramos un término de función

impossible :: ((P -> Void) -> Void) -> Either P Void

también podríamos tener un término

impossible2 :: ((P -> Void) -> Void) -> P
impossible2 = iso_inv . impossible

Según la correspondencia de Curry-Howard, esto sería una tautología en la lógica intuicionista :

((P -> False) -> False) -> P

Pero lo anterior es la eliminación de la doble negación, que es bien sabido que es imposible de probar en la lógica intuicionista , de ahí una contradicción. (El hecho de que podamos probarlo en la lógica clásica no es relevante).

(Nota final: esto supone que nuestro programa Haskell finalizará. Por supuesto, usando una recursión infinita, undefined y formas similares para evitar devolver un resultado, podemos habitar cualquier tipo en Haskell).

Answer 5

No, no es posible, pero es un poco sutil. El problema es que las variables de tipo b están cuantificadas universalmente.

to :: ((a -> b) -> b) -> Either a b
to f = ...

b están universalmente cuantificados. La persona que llama elige de qué tipo son, por lo que no puede simplemente crear un valor de cualquier tipo. Esto implica que no puede simplemente crear un valor de tipo Either ab mientras ignora el argumento f . Pero usar f también es imposible. Sin saber qué son los tipos a y b , no puede crear un valor de tipo a -> b para pasar a f . Simplemente no hay suficiente información disponible cuando los tipos se cuantifican universalmente.

En cuanto a por qué el isomorfismo no funciona en Haskell, ¿estás seguro de que esas proposiciones son equivalentes en una lógica constructivista intuicionista? Haskell no implementa una lógica deductiva clásica.