logic.lhs

= Logic Programming =

So far, substitutions have been a means to an end. Once we found the most
general unifier, we discarded any work we did along the way.

This time, the substitutions take center stage. We start with our trusty `mgu`:

\begin{code}
{-# LANGUAGE BlockArguments, DeriveFunctor, DeriveFoldable #-}
import Control.Arrow (second)
import Data.List (nub, transpose)
import Text.Megaparsec
import Text.Megaparsec.Char
type Parser = Parsec () String

data ExpF a = C String | V a | ExpF a :@ ExpF a deriving (Eq, Functor, Foldable, Show)
type VarId = String
type Exp = ExpF VarId
type Subst = [(VarId, Exp)];

apply :: Subst -> Exp -> Exp
apply sub t = case t of
  a :@ b -> apply sub a :@ apply sub b
  V v    -> maybe t id $ lookup v sub
  _      -> t

mgu :: Exp -> Exp -> Subst -> [Subst]
mgu t u sub = case (apply sub t, apply sub u) of
  (C a, C b) | a == b  -> [sub]
  (V a, V b) | a == b  -> [sub]
  (V a, x)             -> varBind a x
  (x, V a)             -> varBind a x
  (x1 :@ y1, x2 :@ y2) -> mgu x1 x2 sub >>= mgu y1 y2
  _                    -> []
  where
  varBind v t = if elem v t then [] else
    [(v, t):map (second $ apply [(v, t)]) sub]
\end{code}

In the past, we applied substitutions before calling `mgu`. Here, we pass in
substitutions and `mgu` applies them on our behalf, so we can easily try out
different substitutions on the same term.

Instead of a `Maybe Subst` we return a list of 0 or 1 substitutions.

== Who's your daddy? ==

We define a simple grammar for parsing `Exp` values:

\begin{code}
fact :: Parser Exp
fact = apps where
  apps = foldl1 (:@) <$> some
    (con <|> var <|> between (spch '(') (spch ')') apps)
  con  = C <$> sp ((:) <$> (digitChar <|> lowerChar) <*> many alphaNumChar)
  var  = V <$> sp ((:) <$> upperChar <*> many alphaNumChar)

sp   = (<* many (char ' '))
spch = sp . char

mustFact :: String -> Exp
mustFact = either undefined id . parse fact ""
\end{code}

Suppose we are told `alfred` is a parent of `aethelflaed`, and then we are
asked for a parent of `aethelflaed`. We can answer this query via unification:

\begin{code}
exampleTrivial = mgu fact q [] where
  fact = mustFact "parent alfred aethelflaed"
  q    = mustFact "parent X aethelflaed"
\end{code}

------------------------------------------------------------------------
[[("X",C "alfred")]]
------------------------------------------------------------------------

Let's build on this simple idea.

== Do you know where your children are? ==

Given multiple facts, we can find all that unify with a given query:

\begin{code}
births :: [Exp]
births = mustFact <$>
  [ "parent alfred aethelflaed"
  , "parent aethelflaed aelfwynn"
  , "parent alfred edward"
  , "parent edward aethelstan"
  , "parent edward edmund"
  , "parent edward eadred"
  , "parent edmund eadwig"
  , "parent edmund edgar"
  ]

exampleMultiple = concat [mgu p q [] | p <- births]
  where q = mustFact "parent edward X"
\end{code}

------------------------------------------------------------------------
[[("X",C "aethelstan")],[("X",C "edmund")],[("X",C "eadred")]]
------------------------------------------------------------------------

== Grand slam ==

We extend our system so a predicate depends on any number of other predicates:

\begin{code}
type Rule = [Exp]
rule :: Parser Rule
rule = (:) <$> fact <*> (option [] (sp (string ":-") *> sepBy1 fact (spch ',')))

mustRule :: String -> Rule
mustRule = either undefined id . parse rule ""

grand :: [Rule]
grand = mustRule "grandparent A B :- parent A X, parent X B" :
  ((:[]) <$> births)
\end{code}

The `births` are predicates which are unconditionally true because they have no
dependencies, while `grandparent A B` is true only if we can unfiy `parent A X`
with a true predicate and unify `parent X B` with a true predicate.

We find all solutions with a depth-first search:

\begin{code}
dfs :: [Rule] -> Exp -> Subst -> [Subst]
dfs rules q sub = concat [f t =<< mgu h q sub | (h:t) <- rules]
  where
  f xs s' = case xs of
    []     -> [s']
    (x:xt) -> f xt =<< dfs rules x s'

exampleGrand = dfs grand (mustFact "grandparent alfred Y") []
\end{code}

------------------------------------------------------------------------
[[("Y",C "aelfwynn"),("X",C "aethelflaed"),("B",V "Y"),("A",C "alfred")],
[("Y",C "aethelstan"),("X",C "edward"),("B",V "Y"),("A",C "alfred")],
[("Y",C "edmund"),("X",C "edward"),("B",V "Y"),("A",C "alfred")],
[("Y",C "eadred"),("X",C "edward"),("B",V "Y"),("A",C "alfred")]]
------------------------------------------------------------------------

== Keep it fresh ==

In our previous example, we had to carefully chose distinct variable names.
It makes more sense for variables to be scoped to the rule in which they
appear. This makes the language friendlier, and also allows recursive rules.

We'll achieve this by automatically generating fresh variables each time we
encounter a rule. But first, we break down our search for substitutions into
easily digestible pieces.

The design of our code is similar to
http://www.cs.uu.nl/research/techreps/repo/CS-2008/2008-044.pdf[the basic
parser combinators described by Swierstra], or the `readS a` type from the base
library: a function taking a string and returning the list of possible ways to
parse the beginning of the input string along with the unparsed remainder.

We define a "predicate combinator" `Pred` to be a function taking an `Env`
consisting of the substitutions required so far and a stream of integers
representing unused variables and returning all `Env` values that satisfy the
predicate.

\begin{code}
type Env = (Subst, [Int])
type Pred = Env -> [Env]

pristine :: Env
pristine = ([], [0..])
\end{code}

The only `Pred` we can build from scratch is one that attempts to unify two
given expressions:

\begin{code}
(~~) :: Exp -> Exp -> Pred
s ~~ t = \(sub, vs) -> [(s', vs) | s' <- mgu s t sub]
\end{code}

Otherwise we build a `Pred` value from existing `Pred` values or indirectly
calling `(~~)`.

\begin{code}
fresh :: (Exp -> Pred) -> Pred
fresh f = \(sub, v:vs) -> f (V $ '_':show v) (sub, vs)

(\/!) :: Pred -> Pred -> Pred
(\/!) x y e = x e <> y e

(/\!) :: Pred -> Pred -> Pred
(/\!) x y e = x e >>= y

nono :: Pred -> Pred
nono x e = if null $ x e then [e] else []
\end{code}

Our depth-first search becomes:

\begin{code}
dfs' rules q = fst <$> f q pristine where
  f q = foldr1 (\/!)
    $ foldr1 (/\!) . zipWith ($) ((q ~~):repeat f) <$> rules

exampleGrand' = dfs' grand $ mustFact "grandparent alfred Y"
\end{code}

However, we want fresh variables:

\begin{code}
varsOf :: Rule -> [VarId]
varsOf = nub . concatMap (foldr (:) [])

pretty :: Foldable t => t VarId -> Env -> Subst
pretty q (subs, _) = map (second $ apply subs)
  $ filter (\(v, _) -> elem v q) subs

prolog :: [Rule] -> Exp -> [Subst]
prolog rules q = pretty q <$> f q pristine where
  f q = foldr1 (\/!)
    [refresh [] (varsOf r) $ zip ((q ~~):repeat f) r | r <- rules]
  refresh sub vs zs = case vs of
    []     -> foldr1 (/\!) $ map (\(f, x) -> f $ apply sub x) zs
    (v:vt) -> fresh \w -> refresh ((v, w):sub) vt zs
\end{code}

We called the function `prolog` because it mimics the logical part of Prolog.
We've also taken this opportunity to clean up the output. We only print
substitutions for variables in the query, and we fully apply all substitutions.

We test a classic example:

\begin{code}
anc :: [Rule]
anc =
    mustRule "ancestor A B :- parent A B"
  : mustRule "ancestor A B :- parent A X, ancestor X B"
  : grand

exampleAnc = prolog anc $ mustFact "ancestor X eadwig"
\end{code}

------------------------------------------------------------------------
[[("X",C "edmund")],[("X",C "alfred")],[("X",C "edward")]]
------------------------------------------------------------------------

== Out of our depth ==

The following `bitty` predicate matches all bitstrings of all lengths:

\begin{code}
bitty = mustRule <$>
  [ "bitty end"
  , "bitty (0 X) :- bitty X"
  , "bitty (1 X) :- bitty X"
  ]
\end{code}

But when we look for them, we only see 0s:

\begin{code}
exampleBitty = take 5 $ prolog bitty $ mustFact "bitty X"
\end{code}

------------------------------------------------------------------------
[[("X",C "end")],
[("X",C "0" :@ C "end")],
[("X",C "0" :@ (C "0" :@ C "end"))],
[("X",C "0" :@ (C "0" :@ (C "0" :@ C "end")))],
[("X",C "0" :@ (C "0" :@ (C "0" :@ (C "0" :@ C "end"))))]]
------------------------------------------------------------------------

Here, depth-first search never tires of the first branch it explores, because
it contains infinite matches.
Surprisingly, by simply replacing `concat` with a function that interleaves two
lists, the depth-first search gains elements of a breadth-first search in the
way it it backtracks.

\begin{code}
interleave :: [a] -> [a] -> [a]
interleave [] ys = ys
interleave (x:xs) ys = x : interleave ys xs

(\/) :: Pred -> Pred -> Pred
(\/) x y e = x e `interleave` y e

(/\) :: Pred -> Pred -> Pred
(/\) x y e = foldr interleave [] $ map y (x e)

prolog' :: [Rule] -> Exp -> [Subst]
prolog' rules q = pretty q <$> f q pristine where
  f q = foldr1 (\/) $ (\r -> refresh [] (varsOf r) $ zip ((q ~~):repeat f) r) <$> rules
  refresh sub vs zs = case vs of
    []     -> foldr1 (/\) $ map (\(f, x) -> f $ apply sub x) zs
    (v:vt) -> fresh \w -> refresh ((v, w):sub) vt zs
\end{code}

Our search now reaches any given bitstring:

\begin{code}
exampleBitty' = take 5 $ prolog' bitty $ mustFact "bitty X"
\end{code}

------------------------------------------------------------------------
[[("X",C "end")],
[("X",C "1" :@ C "end")],
[("X",C "0" :@ C "end")],
[("X",C "1" :@ (C "1" :@ C "end"))],
[("X",C "0" :@ (C "1" :@ C "end"))]]
------------------------------------------------------------------------

A cute trick is to define `interleave` as:

------------------------------------------------------------------------
interleave xs ys = concat $ transpose [xs, ys]
------------------------------------------------------------------------

More generally, the function `transpose` can interleave multiple lists, which
suggests the following variation with even more emphasis on breadth over depth:

\begin{code}
disj :: [Pred] -> Pred
disj xs e = concat . transpose $ map ($ e) xs

conj :: [Pred] -> Pred
conj = foldr1 \x y e -> concat . transpose $ map y (x e)

prolog'' :: [Rule] -> Exp -> [Subst]
prolog'' rules q = pretty q <$> f q pristine where
  f q = disj $ (\r -> refresh [] (varsOf r) $ zip ((q ~~):repeat f) r) <$> rules
  refresh sub vs zs = case vs of
    []     -> conj $ map (\(f, x) -> f $ apply sub x) zs
    (v:vt) -> fresh \w -> refresh ((v, w):sub) vt zs
\end{code}

== Predicate combinators ==

Just as we mix and match parser combinators to build parsers, we can mix and
match the above functions to build logic programs. For example, the following
finds all pairs of lists that concatenate to [3, 1]:

\begin{code}
appendo :: Exp -> Exp -> Exp -> Pred
appendo x y z =
     ((x ~~ C "nil") /\ (y ~~ z))
  \/ fresh \h -> fresh \xt -> fresh \zt ->
       (x ~~ (C "cons" :@ h :@ xt))
    /\ (z ~~ (C "cons" :@ h :@ zt))
    /\ appendo xt y zt

exampleAppendo = pretty ["X", "Y"] <$>
  appendo (V "X") (V "Y") (mustFact "cons 3 (cons 1 nil)") pristine
\end{code}

------------------------------------------------------------------------
[[("Y",(C "cons" :@ C "3") :@ ((C "cons" :@ C "1") :@ C "nil")),("X",C "nil")],
[("Y",(C "cons" :@ C "1") :@ C "nil"),("X",(C "cons" :@ C "3") :@ C "nil")],
[("Y",C "nil"),("X",(C "cons" :@ C "3") :@ ((C "cons" :@ C "1") :@ C "nil"))]]
------------------------------------------------------------------------

== Prolog forever ==

To perform true breadth-first search, we define a variant of `Pred` that takes an
`Env` to a stream of lists of possible `Env` values that satisfy the predicate.
All solutions in the same list have the same cost. The nth list holds all
solutions of cost n.

\begin{code}
type PredB = Env -> [[Env]]
\end{code}

The unification predicate costs nothing:

\begin{code}
(~~~) :: Exp -> Exp -> PredB
s ~~~ t = \(sub, vs) -> [[(s', vs) | s' <- mgu s t sub]]
\end{code}

Disjunction concatenates all solutions with the same cost:

\begin{code}
mct = map concat . transpose

disB :: [PredB] -> PredB
disB xs e = mct $ ($ e) <$> xs
\end{code}

To form the conjunction of `f` and `g`, we order the solutions of `f` by
cost, then solve each one of them for `g`, adding in the cost of solving `f`
before ordering them. We add a cost of 1 to everything by prepending an empty
list of solutions, which indicates there are no solutions of cost 0.
Conceptually, we want:

------------------------------------------------------------------------
\f g e ->
   [[], mct $ zipWith (++) (inits $ repeat []) $ mct . map g <$> f e]
------------------------------------------------------------------------

This only works for finite cases, because we may wind up concatenating an
infinite list of `[]`. We know this does nothing, but the code doesn't! We
instead explicitly limit concatenation, resulting in something like a discrete
convolution applied to many lists:

\begin{code}
andB :: PredB -> PredB -> PredB
andB f g e = [] : map concat (conv [] $ mct . map g <$> f e) where
  conv acc xs = case xs of
    [] -> transpose acc
    (xsh:xst) -> hs : conv (xsh : ts) xst
    where
    (hs, ts) = unzip [(h, t) | h:t <- acc]

conB :: [PredB] -> PredB
conB = foldr1 andB
\end{code}

Generating a fresh variable remains the same, and with that, we have a
Prolog that performs breadth-first search:

\begin{code}
freshB :: (Exp -> PredB) -> PredB
freshB f = \(sub, v:vs) -> f (V $ '_':show v) (sub, vs)

prologB :: [Rule] -> Exp -> [Subst]
prologB rules q = pretty q <$> concat (f q pristine) where
  f q = disB $ (\r -> refresh [] (varsOf r) $ zip ((q ~~~):repeat f) r) <$> rules
  refresh sub vs zs = case vs of
    []     -> conB $ map (\(f, x) -> f $ apply sub x) zs
    (v:vt) -> freshB \w -> refresh ((v, w):sub) vt zs
\end{code}

Poorly written recursive rules in Prolog can get trapped in depth-first search.
Breadth-first search is more tolerant:

\begin{code}
wrong :: [Rule]
wrong =
    mustRule "ancestor A B :- parent A B"
  : mustRule "ancestor A B :- ancestor X B, parent A X"
  : grand

exampleWrong = prologB wrong $ mustFact "ancestor X eadwig"
\end{code}

The code still runs forever, but at least it finds all solutions:

------------------------------------------------------------------------
[[("X",C "edmund")],[("X",C "edward")],[("X",C "alfred")]
------------------------------------------------------------------------

Putting the output of a `Pred` in a singleton list to gives us a `PredB`.
Thus we can mix in our other functions and combine different search strategies.

== Program synthesis ==

We employ breadth-first search to find combinatory logic programs `F`
satisfying `F x y = y`.

\begin{code}
step :: Exp -> Exp -> PredB
step lhs rhs = freshB \x -> freshB \y -> freshB \z -> disB
  [ conB [lhs ~~~ (C "k" :@ x :@ y)     , rhs ~~~ x]
  , conB [lhs ~~~ (C "t" :@ x :@ y)     , rhs ~~~ (y :@ x)]
  , conB [lhs ~~~ (C "s" :@ x :@ y :@ z), rhs ~~~ (x :@ z :@ (y :@ z))]
  , conB [lhs ~~~ (C "b" :@ x :@ y :@ z), rhs ~~~ (x :@ (y :@ z))]
  , conB [lhs ~~~ (C "c" :@ x :@ y :@ z), rhs ~~~ (x :@ z :@ y)]
  , conB [lhs ~~~ (x :@ z), rhs ~~~ (y:@ z), step x y]
  ]
cl :: Exp -> Exp -> PredB
cl lhs rhs = disB
  [ step lhs rhs
  , freshB \x -> conB [step lhs x, cl x rhs]
  ]

elemConst :: String -> Exp -> Bool
elemConst s t = case t of
  C s' | s == s' -> True
  a :@ b ->  elemConst s a || elemConst s b
  _ -> False

exampleCL = filter (\[(_, t)] -> not (elemConst "y" t)) $ pretty ["F"] <$>
  concat (cl (mustFact "F x y") (mustFact "y") pristine)
\end{code}

------------------------------------------------------------------------
[[("F",C "s" :@ C "k")],
[("F",C "c" :@ C "k")],
[("F",C "k" :@ ((C "s" :@ C "k") :@ V "_9"))],
[("F",C "k" :@ ((C "c" :@ C "k") :@ V "_12"))],
[("F",(C "b" :@ (C "s" :@ C "k")) :@ V "_5")],
[("F",(C "b" :@ (C "c" :@ C "k")) :@ V "_5")],
[("F",C "s" :@ (C "c" :@ (C "s" :@ C "k")))],
[("F",C "s" :@ (C "c" :@ (C "c" :@ C "k")))],
[("F",C "c" :@ (C "c" :@ (C "s" :@ C "k")))],
[("F",C "c" :@ (C "c" :@ (C "c" :@ C "k")))],
[("F",(C "k" :@ (C "s" :@ C "k")) :@ V "_8")],
...
------------------------------------------------------------------------

== The solution to confusion is substitution ==

Long ago, I was underwhelmed by Prolog. Introductory examples suggested I could
declare facts and rules, then watch the computer magically answer my queries.
This was true, up to a point. But past this point, the programmer is forced to
peek under the hood, where it turns out a mundane depth-first search is running
the show.

We can break free of its limitations with "extra-logical" features such as
`cut`. http://minikanren.org/minikanren-and-prolog.html[Understanding side
effects even lets us perform breadth-first searches]. I admire the ingenuity,
but why not use a conventional language if I must muck with low-level details
anyway?

I'm happy that modern logic programming seems more principled.
https://en.wikipedia.org/wiki/Answer_set_programming[Answer set programming
(ASP)] really does magically answer queries after logical facts and rules are
declared. Instead of depth-first search, it uses state-of-the-art SAT-solver
techniques.

Researchers are also tidying up by investigating, for example,
https://gup.ub.gu.se/file/207634[how types can help], or
https://pdfs.semanticscholar.org/3e0a/ff0f1e287b06deb427d56a2696af8228dd61.pdf[how to apply
equational reasoning].

http://www.silvija.net/0000OxfordPublications/seres_thesis.pdf[Seres' thesis on
the algebra of logic programming] features multiple search strategies using
what we called "predicate combinators". The http://minikanren.org/[miniKanren
language family] seems similar. We took our `appendo` example from a miniKanren
demo.

https://www.youtube.com/watch?v=D7rlJWc3474[Edward Kmett's talk on Guanxi]
contains good references and applications. My initial impression is he is
combining all of the above: speedy SAT-solving techniques coupled with a set of
building blocks for rich data structures such as abstract syntax trees.

My starting point was
http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf[the paper on
microKanren], which uses a Lisp-like language. I found simplifications thanks
to Haskell's lazy evaluation, and list monad (only to discover later these
improvements were well-known). On the other hand, Lisp's homoiconicity is
certainly seductive.

The literature mentions monads frequently (there's even a
http://hackage.haskell.org/package/logict[LogicT monad transformer]) but I
shied away; I'm apprehensive about committing to particular choices for `(<|>)`
and `(>>=)`.