Estoy leyendo the Reasoned Schemer.conda, condi, conde, conducto
Tengo un poco de intuición sobre cómo funciona conde.
Sin embargo, no puedo encontrar una definición formal de lo conde/conda/condu/condi lo hacen.
Conozco https://www.cs.indiana.edu/~webyrd/ pero parece que tiene más ejemplos que definiciones.
¿Existe una definición formal de conde, conda, condi, condu somewhere?
En términos de Prolog, condA es "corte suave", *->, y condU es "elección comprometida" – una combinación de once y un corte suave, de modo que (once(A) *-> B ; false) expresa la corte en (A, !, B):
A *-> B ; C %% soft cut, condA
once(A) *-> B ; C %% committed choice, condU
En condA, si el objetivo A tiene éxito, todas las soluciones se pasan a la primera cláusula B y no se proponen cláusulas alternativas C. once/1 permite que su objetivo de argumento tenga éxito solo una vez (conserva solo una solución, si corresponde).
condE es una disyunción simple, y condI es una disyunción que alterna entre las soluciones de sus constituyentes.
Así es un intento de traducir fielmente el código del libro, las variables fuera lógicos y unificación w /, en 18 líneas de Haskell (donde yuxtaposición es aplicación de función al curry, y : significa contras).Ver si esto aclara las cosas:
mplus "del libro):(1) [] ++: ys = ys
(2) (x:xs) ++: ys = x:(xs ++: ys)
mplusI"):(3) [] ++/ ys = ys
(4) (x:xs) ++/ ys = x:(ys ++/ xs)
bind "):(5) [] >>: g = []
(6) (x:xs) >>: g = g x ++: (xs >>: g)
bindI"):(7) [] >>/ g = []
(8) (x:xs) >>/ g = g x ++/ (xs >>/ g)
OR" objetivo combinación ("condE "):(9) (f ||: g) x = f x ++: g x
OR" combinación objetivo (" condI"):(10) (f ||/ g) x = f x ++/ g x
AND" combinación objetivo ("all "):(11) (f &&: g) x = f x >>: g
AND" combinación objetivo (" allI" del libro):(12) (f &&/ g) x = f x >>/ g
(13) true x = [x] -- a sigleton list with the same solution repackaged
(14) false x = [] -- an empty list, meaning the solution is rejected
Metas producir corrientes (posiblemente vacío) de soluciones (posiblemente actualizados), dada una solución (posiblemente parcial) a un problema.
reglas Re-escritura para all son:
(all) = true
(all g1) = g1
(all g1 g2 g3 ...) = (\x -> g1 x >>: (all g2 g3 ...))
=== g1 &&: (g2 &&: (g3 &&: ...))
(allI g1 g2 g3 ...) = (\x -> g1 x >>/ (allI g2 g3 ...))
=== g1 &&/ (g2 &&/ (g3 &&/ ...))
reglas Re-escritura para condX son:
(condX) = false
(condX (else g1 g2 ...)) = (all g1 g2 ...) === g1 &&: (g2 &&: (...))
(condX (g1 g2 ...)) = (all g1 g2 ...) === g1 &&: (g2 &&: (...))
(condX (g1 g2 ...) (h1 h2 ...) ...) =
(ifX g1 (all g2 ...) (ifX h1 (all h2 ...) (...)))
Para llegar a la final condE y condI la traducción, t aquí no hay necesidad de poner en práctica ifE y ifI, ya que reducen además a combinaciones de operadores simples, con todos los operadores que se consideran asociativo por la derecha del libro:
(condE (g1 g2 ...) (h1 h2 ...) ...) =
(g1 &&: g2 &&: ...) ||: (h1 &&: h2 &&: ...) ||: ...
(condI (g1 g2 ...) (h1 h2 ...) ...) =
(g1 &&: g2 &&: ...) ||/ (h1 &&: h2 &&: ...) ||/ ...
lo que no hay necesidad de ningún "sintaxis" especial en Haskell, los operadores simples son suficientes. Se puede usar cualquier combinación, con &&/ en lugar de &&: si es necesario. Pero OTOH condI también podría implementarse como una función para aceptar una recopilación (lista, árbol, etc.) de los objetivos que se deben cumplir, que usaría alguna estrategia inteligente para elegir uno más probable o más necesario, etc., y no solo alternancia binaria simple como en el operador ||/ (o ifI del libro).
A continuación, de condA puede ser modelado por dos nuevos operadores, ~~> y ||~, trabajando juntos el libro. Podemos usarlos de forma natural como en, por ejemplo,
g1 ~~> g2 &&: ... ||~ h1 ~~> h2 &&: ... ||~ ... ||~ gelse
que se puede leer intuitivamente como "IF g1 THEN g2 AND ... OR-ELSE IF h1 THEN ... OR-ELSE gelse".
IF-THEN" combinación objetivo es producir una meta "probar" que debe ser llamado con un gol de falta de continuación:(15) (g ~~> h) f x = case g x of [] -> f x ; ys -> ys >>: h
OR-ELSE" combinación objetivo de un "tratar "Objetivo y un objetivo simple simplemente llama a su objetivo de" prueba "con un segundo objetivo de falla, por lo que no es más que una sintaxis de conveniencia para la agrupación automática de operandos:(16) (g ||~ f) x = g f x
Si el operador ||~ "OR-ELSE" se le da poder menos vinculante que el operador ~~> "IF-THEN" e hizo asociativo por la derecha también, y ~~> operador ha poder aún menos vinculante que &&: y similares agrupación, sensata de los anteriores ejemplo se produce automáticamente como
(g1 ~~> (g2 &&: ...)) ||~ ((h1 ~~> (h2 &&: ...)) ||~ (... ||~ gelse)...)
último gol en una cadena ||~ debe por lo tanto ser un objetivo simple.Eso no es una limitación en realidad, ya que la última cláusula del formulario condA es equivalente de todos modos al simple "AND" -combinación de sus objetivos (o simplemente false se puede usar igual de bien).
Eso es todo. Incluso podemos tener más tipos de Try-objetivos, representados por diferentes tipos de "IF" operadores, si queremos:
condAI , si había uno en el libro):(17) (g ~~>/ h) f x = case g x of [] -> f x ; ys -> ys >>/ h
condU:(18) (g ~~>! h) f x = case g x of [] -> f x ; (y:_) -> h y
Así que, finalmente, las reglas de reescritura para condA y condU del libro son simplemente:
(condA (g1 g2 ...) (h1 h2 ...) ...) =
g1 ~~> g2 &&: ... ||~ h1 ~~> h2 &&: ... ||~ ...
(condU (g1 g2 ...) (h1 h2 ...) ...) =
g1 ~~>! g2 &&: ... ||~ h1 ~~>! h2 &&: ... ||~ ...
El Schemer razonado cubre conda (corte suave) y condu (elección comprometida). También encontrará explicaciones de su comportamiento en el excelente dissertation on miniKanren de William Byrd. Has etiquetado esta publicación como sobre core.logic. Para ser claros, core.logic se basa en una versión más reciente de miniKanren que la presentada en The Reasoned Schemer. miniKanren siempre intercala los objetivos disyuntivos - condi y las variantes de entrelazado ya no existen. condeescondi ahora.
Por ejemplo, el uso de core.logic:
conde se ejecutará cada grupo, tener éxito si al menos un grupo tiene éxito, y el retorno todos los resultados de todos los grupos de éxito.
user> (run* [w q]
(conde [u#]
[(or* [(== w 1) (== w 2)])
(== q :first)]
[(== q :second)]))
([_0 :second] [1 :first] [2 :first])
conda y Condu: ambos se detendrá después de la primera exitoso grupo (de arriba abajo)
conda retornos todos los resultados de sólo el primer grupo de éxito.
user> (run* [w q]
(conda [u#]
[(or* [(== w 1) (== w 2)])
(== q :first)]
[(== q :second)]))
([1 :first] [2 :first])
Condu sólo devuelve un resultado de sólo el primer grupo de éxito.
user> (run* [w q]
(condu [u#]
[(or* [(== w 1) (== w 2)])
(== q :first)]
[(== q :second)]))
([1 :first])
Ni idea de lo condi hace sin embargo.
No es una definición formal pero podría ayudar – paulocuneo
como dnolen escribe en su respuesta aquí, conde of core.logic es condi del libro. Conde del libro procesa sus sub-objetivos en orden, secuencialmente. si el primer subgrupo sucesivo producía un flujo infinito de respuestas, no aparecerían otras soluciones de subgoles exitosas en el flujo de soluciones combinadas. Condi del libro remedió eso intercalando las corrientes. –
¡increíble! ahora sé. no capturó la parte de secuencia/intercalado cuando. revisitando core.logic src a partir de ahora – paulocuneo
5 uparrows on stack overflow no es digno de esta respuesta. Espero que lo conviertas en una publicación de blog o algo así. – user1383359
Como seguimiento: ¿es COND? == O?¿y todo? == Y? ? – user1383359
@ user1383359 más o menos. CONDe es OR de Prolog (disyunción), y ALL - AND de AND (conjunción) de Prolog. CONDi, ALLi, son una variación de las soluciones de subobjetivos que combinan orden, tratando de incorporar la prevención del comportamiento no productivo en el sistema de antemano. –