Interleaving Search in HVM1 (dup_labels branch)

search.hvm

// Prelude stuff
(String.concat String.nil         ys) = ys
(String.concat (String.cons x xs) ys) = (String.cons x (String.concat xs ys))

// Search Stuff
(List.head List.nil) = (Err "Head Taken on empty list")
(List.head (List.cons x _)) = x

(List.take 0 xs)               = List.nil
(List.take n List.nil)         = List.nil
(List.take n (List.cons x xs)) = (List.cons x (List.take (- n 1) xs))

(List.concat (List.nil)       ys) = ys
(List.concat (List.cons x xs) ys) = (List.cons x (List.concat xs ys))

(List.interleave (List.nil) ys) = ys
(List.interleave (List.cons x xs) ys) = (List.cons x (List.interleave ys xs))

// Minikanren style interleaving search, using dups as a proxy for thunks
(SearchI x) = (SearchI.ret (SearchI.aux x))
  (SearchI.aux None) = List.nil
  (SearchI.aux (Some x)) = (List.cons (Some x) List.nil)
  (SearchI.aux (HVM.SUP k x y)) = (List.cons None (List.interleave (SearchI.aux x) (SearchI.aux y)))

  (SearchI.seg None) = List.nil
  (SearchI.seg (Some x)) = (List.cons x List.nil)

  (SearchI.ret List.nil) = List.nil
  (SearchI.ret (List.cons x xs)) = (List.concat (SearchI.seg x) (SearchI.ret xs))

// Prolog style depth-first search
(SearchD None) = List.nil
(SearchD (Some x)) = (List.cons x List.nil)
(SearchD (HVM.SUP k x y)) = (List.concat (SearchD x) (SearchD y))

(Res x) = (List.head (SearchI x))
(ResN n x) = (List.take n (SearchI x))

// Bools
True = λxλy x
False = λxλy y
(Bool k) = (HVM.SUP k True False)
(Bool1 k) = λxλy (HVM.SUP k x y) // Note: Doesn't work so well; better for sup to be above binders to avoid blocking

(Or x y) = (x True y)
(Or1 x y) = λaλb (x a (y a b))
(And x y) = (x y False)
(And1 x y) = λaλb (x (y a b) b)

(Bool.show x) = (x (Some "T") (Some "F")) 
  // Note, Some tags need to be generated at the end of search trees. (Some #0{A B}) will not reduce to #0{(Some A) (Some B)}.
  // This also means (Some (x "T" "F")) doesn't work as the x will get stuck on the Some
  // X.show is essentially pulling double duty as both a smart constructor for Some and a prettyprinter.

// If we want a search tree with booleans at its leaves instead of strings, we can do this
// This is better if further computation is going to be done on the result of the search
(Bool.quasiquote x) = (x (Some True) (Some False)) 

// Quotation oriented constructors that pass through Some are useful. For example
(Pair (Some x) (Some y)) = (Some (Pair x y))
// Pairing a quoted expression will quote the pair automatically now

// Test expression with two variables
// (k & g) || k
(EXP1 k g) = (Or (And (Bool k) (Bool g)) (Bool k))

// Search the values of EXP1 against the true branch of (Bool 0)
// Main = (SearchI ((Bool 0) (Bool.show (EXP1 0 1)) None))

// This pairs the values of variable 1, allowing us to look at its values along with those of EXP1
// Main = (SearchI ((Bool 0) (Pair (Bool.show (EXP1 0 1)) (Bool.show (Bool 1))) None))

// This shows the values of both variables
// Main = (SearchI ((Bool 0) (Pair (Bool.show (EXP1 0 1)) (Pair (Bool.show (Bool 0)) (Bool.show (Bool 1)))) None))

// An actual solver. What values for variables 0 and 1 remain under the restriction that EXP1 is true?
// Will return [(Pair "T" "T"), (Pair "T" "F")], the two pairs of values that satisfy the formula.
// Main = (SearchI ((EXP1 0 1) (Pair (Bool.show (Bool 0)) (Bool.show (Bool 1))) None))

// Natural Numbers (Scott encoding)
Nat.zero = λzλs z
(Nat.succ x) = λzλs (s x)

(Nats k) = (HVM.SUP k Nat.zero (Nat.succ (Nats k)))

(Nat.show x) = (x (Some "Z") λa (Nat.show.aux (Nat.show a)))
  (Nat.show.aux (Some x)) = (Some (String.concat "S" x))


// Nat.show test
// Main = (Nat.show (Nat.succ (Nat.succ Nat.zero)))

// Searching through the unconstraint space of nats
// Returns the first 10 natural numbers
// Main = (ResN 10 (Nat.show (Nats 0)))

(Nat.add x y) = (x λy y λxpλy (Nat.succ (Nat.add xp y)) y)
(Nat.eq x y) = (x λy (y True λyp False) λxpλy (y False λyp (Nat.eq xp yp)) y)

One = (Nat.succ Nat.zero)
Two = (Nat.succ One)
Three = (Nat.succ Two)
Four = (Nat.succ Three)
Five = (Nat.succ Four)
Six = (Nat.succ Five)

// Test equality and add
//Should be 5
//Main = (Nat.add Three Two)
//Should be True
//Main = (Nat.eq Nat.zero Nat.zero)
//Should be False
//Main = (Nat.eq Nat.zero One)
//Should be False
//Main = (Nat.eq One Nat.zero)
//Should be True
//Main = (Nat.eq One One)
//Should be True
//Main = (Nat.eq (Nat.add Three Two) Five)
//Should be False
//Main = (Nat.eq (Nat.add Three Two) Six)

// List all numbers which add up to 5;
// Note how this search ends on its own without manual intervention
//Main = (SearchI (
//  ((Nat.eq (Nat.add (Nats 0) (Nats 1)) Five) (Pair (Nat.show (Nats 0)) (Nat.show (Nats 1))) None)
//  ))

// Get numbers, x, such that ∃y. 3 + x = 5 + y. This is just numbers >= 2, but this demos an interesting method
//Main = (ResN 10 ((Nat.eq (Nat.add Three (Nats 0)) (Nat.add Five (Nats 1))) (Nat.show (Nats 0)) None))

// Normalize a superposition into a search tree
(Nat.quasiquote x) = (x (Some Nat.zero) λxp (Nat.quasiquote.aux (Nat.quasiquote xp)))
  (Nat.quasiquote.aux (Some x)) = (Some (Nat.succ x))

// Common logic programming demo: Compute subtraction via addition.
(Sub x y) = (Res ((Nat.eq (Nat.add (Nats 0) y) x) (Nat.quasiquote (Nats 0)) None))
Main = (Sub Five Three) // Returns 2

I've tried using these methods to reproduce Taelin's search. I can't find anything that works as a drop-in replacement for the priority queue. Here are some different search algorithms I've tried, in addition to the two in the above file;

// Breadth first (V1)
(SearchB t) = (SearchB.st [t])
(SearchB.st List.nil) = List.nil
(SearchB.st (List.cons x xs)) = (SearchB.aux x xs)
  (SearchB.aux None xs) = (SearchB.st xs)
  (SearchB.aux (Some x) xs) = (List.cons x (SearchB.st xs))
  (SearchB.aux (HVM.SUP k x y) xs) = (SearchB.st (List.concat xs [x, y]))

// Breadth first (V2)
(SearchB x) = (SearchB.ret (SearchB.aux x))
  (SearchB.aux None) = List.nil
  (SearchB.aux (Some x)) = (List.cons (Some x) List.nil)
  (SearchB.aux (HVM.SUP k x y)) = (List.interleave (SearchB.aux x) (SearchB.aux y))

  (SearchB.seg None) = List.nil
  (SearchB.seg (Some x)) = (List.cons x List.nil)

  (SearchB.ret List.nil) = List.nil
  (SearchB.ret (List.cons x xs)) = (List.concat (SearchB.seg x) (SearchB.ret xs))

// Interleaving search (using a queue of sorts)

// State monad stuff
(State.run (State f) s) = (f s)
// return :: a -> State s a
(State.return x) = (State λs(Pair x s))
// bind :: State s a -> (a -> State s b) -> State s b
(State.bind (State f) g) = 
  (State λs(
    (Pair.match (f s) λresult λstate
      (State.run (g result) state)
    )
  ))
// get :: State s s
(State.get) = (State λs(Pair s s))
// put :: s -> State s ()
(State.put newState) = (State λ_ (Pair Unit newState))

// Peal one suspended layer
(IPeal None) = None
(IPeal (Some x)) = (Some x)
(IPeal (HVM.SUP k x y)) = (Branch x y)

// IStep :: Q -> State Term Q
(IStep None) = (State.return None)
(IStep (Susp x)) = (IStep.Suspaux (IPeal x))
  (IStep.Suspaux None) = (State.return None)
  (IStep.Suspaux (Branch x y)) = (State.return (Branch (Susp x) (Susp y)))
  (IStep.Suspaux (Some x)) = (State.bind (State.put (Some x)) λ_ (State.return None))
(IStep (Branch x y)) = 
  (State.bind (IStep x) λres 
    (State.return (IStep.Branchaux res y)))
    
  (IStep.Branchaux None y) = y
  (IStep.Branchaux (Susp x) y) = (Branch y (Susp x)) // Note: branch flips
  (IStep.Branchaux (Branch x z) y) = (Branch y (Branch x z)) // Note: branch flips

(ISearch3 x) = (ISearch.aux (Susp x))
  (ISearch.aux x) = (Pair.match (State.run (IStep x) None) λresλstate(ISearch.aux2 state res))
  (ISearch.aux2 None res) = (ISearch.finish res)
  (ISearch.aux2 (Some x) res) = (List.cons x (ISearch.finish res))
  (ISearch.finish None) = List.nil
  (ISearch.finish (Susp x)) = (ISearch.aux (Susp x))
  (ISearch.finish (Branch x y)) = (ISearch.aux (Branch x y))

None of them work in place of Collapse. By "work", I mean exit with a result fairly quickly. These all take a long time. I don't know why. As far as I can tell, the priority labels generated by ENUM increase with deeper depth, but are otherwise not important. Significantly, they don't do something like bias the program to calling Rec less often, or something like that. I just don't get how the priority queue is doing it. This can be adapted to a search which can return a list of results

(SearchP x) = (SearchP.aux x PQ.new)
  (SearchP.aux (HVM.SUP k a b) pq) = (SearchP.aux None (PQ.put k a (PQ.put k b pq)))
  (SearchP.aux (Some x) pq) = (List.cons x (SearchP.aux None pq))
  (SearchP.aux None pq) = (SearchP.None pq)
  
  (SearchP.None Empty) = List.nil
  (SearchP.None (Node k v lft rgt)) = ((PQ.get (Node k v lft rgt)) λkλxλpq(SearchP.aux x pq))

but I can't factor out the labels. I don't get it. There's something I'm missing.

In the above file I used "quasiquote" functions to normalize the search tree. This is actually bad for efficiency. It's possible, and not really that hard, to normalize the search tree right before calling the search function. Without it, some (all?) of the search functions won't always return atomic branches, but may instead return (even infinite!) superpositions under some circumstances. Doing this makes the priority queue search too slow to get a result, so it should be avoided. The priority queue doesn't fully normalize the search tree either. For example

(Collapse ((Bool 0) (Some (EXP1 0 1)) None) PQ.new)

will return

#1{λx0 λ* x0 λx1 λ* x1}

Which is consistent with the behavior of the other searches I listed. The program search example happens to have a single findable result, so the normalized search tree is mostly a bunch of Nones and the correct result. hmm...