clojure - conda, condi, conde, condu

scheme clojure-core.logic

Question

Estoy leyendo el Schemer razonado .

Tengo algo de intuición sobre cómo funciona conde .

Sin embargo, no puedo encontrar una definición formal de lo que hace conde / conda / condu / condi .

Conozco https://www.cs.indiana.edu/~webyrd/ pero parece que tiene ejemplos en lugar de definiciones.

¿Hay una definición formal de conde , conda , condi , condu alguna parte?

Answer 1

El Schemer razonado cubre conda (soft cut) y condu (elección comprometida). También encontrarás explicaciones de su comportamiento en la excelente disertación de William Byrd sobre miniKanren . 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 intercalación ya no existen. conde es condi ahora.

Answer 2

En términos de Prolog, condA es "soft cut" , *-> , y condU es "elección comprometida" - una combinación de once y un corte suave, de modo que (once(A) *-> B ; false) expresa el 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 pasan a la primera cláusula B y no se prueban las 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.

Aquí hay un intento de traducir fielmente el código del libro, sin variables lógicas y unificación, en 18 líneas de Haskell (donde la yuxtaposición es la aplicación de función al curry, y significa contras ). Vea si esto aclara las cosas:

• Combinación de secuencia secuencial (" mplus " del libro):

 (1) [] ++: ys = ys
(2) (x:xs) ++: ys = x:(xs ++: ys)

• Combinación de flujo alterno (" mplusI "):

 (3) [] ++/ ys = ys
(4) (x:xs) ++/ ys = x:(ys ++/ xs)

• Alimentación secuencial (" bind "):

 (5) [] >>: g = []
(6) (x:xs) >>: g = g x ++: (xs >>: g)

• Alimentación alterna (" bindI "):

 (7) [] >>/ g = []
(8) (x:xs) >>/ g = g x ++/ (xs >>/ g)

• " OR " combinación de objetivos (" condE "):

 (9) (f ||: g) x = f x ++: g x

• Combinación de objetivos "Alternar OR " (" condI "):

 (10) (f ||/ g) x = f x ++/ g x

• Combinación de objetivos " AND " (" all "):

 (11) (f &&: g) x = f x >>: g

• Combinación de objetivos "Alternating AND " (" allI " del libro):

 (12) (f &&/ g) x = f x >>/ g

• Metas especiales

 (13) true x = [x] -- a sigleton list with the same solution repackaged
(14) false x = [] -- an empty list, meaning the solution is rejected

Los objetivos producen flujos (posiblemente vacíos) de soluciones (posiblemente actualizadas), dada una solución (posiblemente parcial) a un problema.

Reglas de 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 &&/ ... ))

Las reglas de 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 condE final de la condE y la condI , no es necesario implementar el ifE y el ifI del libro, ya que se reducen aún más a combinaciones simples de operadores, con todos los operadores considerados como asociativos correctos :

(condE (g1 g2 ...) (h1 h2 ...) ...) =
(g1 &&: g2 &&: ... ) ||: (h1 &&: h2 &&: ...) ||: ...
(condI (g1 g2 ...) (h1 h2 ...) ...) =
(g1 &&: g2 &&: ... ) ||/ (h1 &&: h2 &&: ...) ||/ ...

Entonces no hay necesidad de ninguna "sintaxis" especial en Haskell, los operadores simples son suficientes. Se puede usar cualquier combinación, con &&/ lugar de &&: si es necesario. Pero OTOH condI también podría implementarse como una función para aceptar una colección (lista, árbol, etc.) de las metas que se deben cumplir, que usaría alguna estrategia inteligente para elegir una que sea más probable o más necesaria, etc., y no solo una simple binaria alternancia como en ||/ operator (o ifI del libro).

A continuación, dos operadores nuevos, ~~> y ||~ , pueden trabajar conjuntamente en la condA del libro, trabajando juntos. Podemos usarlos de forma natural como en por ejemplo

g1 ~~> g2 &&: ... ||~ h1 ~~> h2 &&: ... ||~ ... ||~ gelse

que intuitivamente puede leerse como " IF g1 THEN g2 AND ... OR-ELSE IF h1 THEN ... OR-ELSE gelse ".

• La combinación de objetivos " IF-THEN " es para producir un objetivo "try" que debe invocarse con un objetivo de continuación de falla:

 (15) (g ~~> h) f x = case g x of [] -> f x ; ys -> ys >>: h

• La combinación de objetivos " OR-ELSE " de un objetivo "try" y un objetivo simple simplemente llama su objetivo "try" con un segundo objetivo "on-failure", 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 " tiene menos poder de enlace que el operador ~~> " IF-THEN " y también se asocia a la derecha, y ~~> operador tiene aún menos poder de enlace que &&: y similares , la agrupación sensible del ejemplo anterior se produce automáticamente como

(g1 ~~> (g2 &&: ...)) ||~ ( (h1 ~~> (h2 &&: ...)) ||~ (... ||~ gelse)...)

El último objetivo en una cadena ||~ debe ser un objetivo simple. Eso no es una limitación en realidad, ya que la última cláusula de la forma condA es equivalente de todos modos al simple " AND " -combinación de sus objetivos (o simplemente false puede usarse).

Eso es todo. Incluso podemos tener más tipos de try-goals, representados por diferentes tipos de operadores " IF ", si queremos:

• utilice la alimentación alternativa en una cláusula de éxito (para modelar lo que se podría haber llamado condAI , si había uno en el libro):

 (17) (g ~~>/ h) f x = case g x of [] -> f x ; ys -> ys >>/ h

• utilice la secuencia de solución exitosa solo una vez para producir el efecto de corte , para modelar condU :

 (18) (g ~~>! h) f x = case g x of [] -> f x ; (y:_) -> h y

De modo que, finalmente, las reglas de condA 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 &&: ... ||~ ...

Answer 3

Por ejemplo, utilizando core.logic:

conde ejecutará cada grupo, tendrá éxito si al menos un grupo tiene éxito y devolverá todos los resultados de todos los grupos exitosos.

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án después del primer grupo exitoso (de arriba a abajo)

conda devuelve todos los resultados solo del primer grupo exitoso.

user> (run* [w q]
(conda [u#]
[(or* [(== w 1) (== w 2)])
(== q :first)]
[(== q :second)]))
([1 :first] [2 :first])

condu devuelve solo un resultado solo del primer grupo exitoso.

user> (run* [w q]
(condu [u#]
[(or* [(== w 1) (== w 2)])
(== q :first)]
[(== q :second)]))
([1 :first])

Sin embargo, no tiene idea de lo que hace.