Optimal Brute Force Search on Simply-Typed λ-Calculus Terms

optimal_brute_force_search_stlc.hvm1.c

// Types
// -----

// Type ::=
//   | (Fun inp out)     // ∀inp out
//   | (Par fst snd)     // [fst&snd]
//   | (Eit fst snd)     // [fst|snd]
//   | Uni               // ⊤

// Term ::=
//   | (Lam bod)         // λx bod
//   | (App fun arg)     // (fun arg)
//   | (Con fst snd)     // [fst,snd]
//   | (Get val bod)     // ![x,y] = val; bod
//   | (Lft val)         // -val 
//   | (Rgt val)         // +val
//   | (Mat val ifL ifR) // ?val :- ifL :+ ifR
//   | One               // 1
//   | (Var idx)         // x

(Lam bod)     = λlam λapp λcon λget λlft λrgt λmat λone λvar (lam bod)
(App fun arg) = λlam λapp λcon λget λlft λrgt λmat λone λvar (app fun arg)
(Con fst snd) = λlam λapp λcon λget λlft λrgt λmat λone λvar (con fst snd)
(Lft val)     = λlam λapp λcon λget λlft λrgt λmat λone λvar (lft val)
(Rgt val)     = λlam λapp λcon λget λlft λrgt λmat λone λvar (rgt val)
(Mat val l r) = λlam λapp λcon λget λlft λrgt λmat λone λvar (mat val l r)
(Get val bod) = λlam λapp λcon λget λlft λrgt λmat λone λvar (get val bod)
One           = λlam λapp λcon λget λlft λrgt λmat λone λvar one
(Var idx)     = λlam λapp λcon λget λlft λrgt λmat λone λvar (var idx)

// Utils
// -----

(If 0 t f) = f
(If n t f) = t

(Unwrap (Some x)) = x

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

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

(Join List.nil)         = String.nil
(Join (List.cons x xs)) = (String.concat x (Join xs))

(COL 0 i x) = x
(COL n i x) = (HVM.DUP i x λx0λx1(COL (- n 1) (+ i 1) (TRY x0 x1)))

(TRY (Some x) y) = (Some x)
(TRY None     y) = y

// Checker
// -------

// TODO

// Evaluator
// ---------

// TODO

// Equality
// --------

// TASK: convert to λ-encoded version
(Equal a b dep) =
  let a_lam = λa_bod λb
    let b_lam = λb_bod (Equal (a_bod (Var dep)) (b_bod (Var dep)) (+ dep 1))
    let b_app = λb_fun λb_arg 0
    let b_con = λb_fst λb_snd 0
    let b_get = λb_val λb_bod 0
    let b_lft = λb_val 0
    let b_rgt = λb_val 0
    let b_mat = λb_val λb_l λb_r 0
    let b_one = 0
    let b_var = λb_val 0
    (b b_lam b_app b_con b_get b_lft b_rgt b_mat b_one b_var)
  let a_app = λa_fun λa_arg λb
    let b_lam = λb_bod 0
    let b_app = λb_fun λb_arg (& (Equal a_fun b_fun dep) (Equal a_arg b_arg dep))
    let b_con = λb_fst λb_snd 0
    let b_get = λb_val λb_bod 0
    let b_lft = λb_val 0
    let b_rgt = λb_val 0
    let b_mat = λb_val λb_l λb_r 0
    let b_one = 0
    let b_var = λb_val 0
    (b b_lam b_app b_con b_get b_lft b_rgt b_mat b_one b_var)
  let a_con = λa_fst λa_snd λb
    let b_lam = λb_bod 0
    let b_app = λb_fun λb_arg 0
    let b_con = λb_fst λb_snd (& (Equal a_fst b_fst dep) (Equal a_snd b_snd dep))
    let b_get = λb_val λb_bod 0
    let b_lft = λb_val 0
    let b_rgt = λb_val 0
    let b_mat = λb_val λb_l λb_r 0
    let b_one = 0
    let b_var = λb_val 0
    (b b_lam b_app b_con b_get b_lft b_rgt b_mat b_one b_var)
  let a_get = λa_val λa_bod λb
    let b_lam = λb_bod 0
    let b_app = λb_fun λb_arg 0
    let b_con = λb_fst λb_snd 0
    let b_get = λb_val λb_bod (Equal (a_bod (Var dep) (Var (+ dep 1))) (b_bod (Var dep) (Var (+ dep 1))) (+ dep 2))
    let b_lft = λb_val 0
    let b_rgt = λb_val 0
    let b_mat = λb_val λb_l λb_r 0
    let b_one = 0
    let b_var = λb_val 0
    (b b_lam b_app b_con b_get b_lft b_rgt b_mat b_one b_var)
  let a_lft = λa_val λb
    let b_lam = λb_bod 0
    let b_app = λb_fun λb_arg 0
    let b_con = λb_fst λb_snd 0
    let b_get = λb_val λb_bod 0
    let b_lft = λb_val (Equal a_val b_val dep)
    let b_rgt = λb_val 0
    let b_mat = λb_val λb_l λb_r 0
    let b_one = 0
    let b_var = λb_val 0
    (b b_lam b_app b_con b_get b_lft b_rgt b_mat b_one b_var)
  let a_rgt = λa_val λb
    let b_lam = λb_bod 0
    let b_app = λb_fun λb_arg 0
    let b_con = λb_fst λb_snd 0
    let b_get = λb_val λb_bod 0
    let b_lft = λb_val 0
    let b_rgt = λb_val (Equal a_val b_val dep)
    let b_mat = λb_val λb_l λb_r 0
    let b_one = 0
    let b_var = λb_val 0
    (b b_lam b_app b_con b_get b_lft b_rgt b_mat b_one b_var)
  let a_mat = λa_val λa_l λa_r λb
    let b_lam = λb_bod 0
    let b_app = λb_fun λb_arg 0
    let b_con = λb_fst λb_snd 0
    let b_get = λb_val λb_bod 0
    let b_lft = λb_val 0
    let b_rgt = λb_val 0
    let b_mat = λb_val λb_l λb_r (& (Equal a_val b_val dep) (& (Equal a_l b_l (+ dep 1)) (Equal a_r b_r (+ dep 1))))
    let b_one = 0
    let b_var = λb_val 0
    (b b_lam b_app b_con b_get b_lft b_rgt b_mat b_one b_var)
  let a_one = λb
    let b_lam = λb_bod 0
    let b_app = λb_fun λb_arg 0
    let b_con = λb_fst λb_snd 0
    let b_get = λb_val λb_bod 0
    let b_lft = λb_val 0
    let b_rgt = λb_val 0
    let b_mat = λb_val λb_l λb_r 0
    let b_one = 1
    let b_var = λb_val 0
    (b b_lam b_app b_con b_get b_lft b_rgt b_mat b_one b_var)
  let a_var = λa_val λb
    let b_lam = λb_bod 0
    let b_app = λb_fun λb_arg 0
    let b_con = λb_fst λb_snd 0
    let b_get = λb_val λb_bod 0
    let b_lft = λb_val 0
    let b_rgt = λb_val 0
    let b_mat = λb_val λb_l λb_r 0
    let b_one = 0
    let b_var = λb_val (== a_val b_val)
    (b b_lam b_app b_con b_get b_lft b_rgt b_mat b_one b_var)
  (a a_lam a_app a_con a_get a_lft a_rgt a_mat a_one a_var b)

// Enumerator
// ----------

// Generates a term
(GEN lv (Fun inp out)) = (Lam λx(USE lv x inp out))
(GEN lv (Par fst snd)) = (Con (GEN lv fst) (GEN lv snd))
(GEN lv (Eit fst snd)) = (HVM.SUP lv (Lft (GEN lv fst)) (Rgt (GEN lv snd)))
(GEN lv (Box typ))     = (GEN (+ lv 1) typ)
(GEN lv Uni)           = One

// Consumes a term
(USE lv tm (Fun inp out) ret) = (USE lv (App tm (GEN lv inp)) out ret)
(USE lv tm (Par fst snd) ret) = (Get tm (GEN lv (Fun fst (Fun snd ret))))
(USE lv tm (Eit fst snd) ret) = (Mat tm (Lam λx(USE lv x fst ret)) (Lam λx(USE lv x snd ret)))
(USE lv tm (Box val)     ret) = (USE lv tm val ret)
(USE lv tm Uni           ret) = (GEN lv ret)

// Searcher
// --------

// Optimal Brute-Force Search. Proves `∃(x: type). query(x)`
(Search n type query) =
  let term = (GEN 0 type) // superposition of candidates
  (COL n 0 (If (query term) (Some term) None))

// Stringification
// ---------------

(Show.u60 n x) = (λx(If (> n 9) (Show.u60 (/ n 10) x) x) (String.cons (+ 48 (% n 10)) x))

(Show term dep) =
  let case_lam = λbod (Join ["λ" (Show (bod (Var dep)) (+ dep 1))])
  let case_app = λfun λarg (Join ["(" (Show fun dep) " " (Show arg dep) ")"])
  let case_con = λfst λsnd (Join ["[" (Show fst dep) "," (Show snd dep) "]"])
  let case_get = λval λbod (Join ["! [" (Show (Var dep) dep) "," (Show (Var (+ dep 1)) (+ dep 1)) "] = " (Show val dep) "; " (Show (bod (Var dep) (Var (+ dep 1))) (+ dep 2))])
  let case_lft = λval (Join ["-" (Show val dep)])
  let case_rgt = λval (Join ["+" (Show val dep)])
  let case_mat = λval λifL λifR (Join ["? " (Show val dep) " :- " (Show ifL (+ dep 1)) " :+ " (Show ifR (+ dep 1))])
  let case_one = (Join ["1"])
  let case_var = λval (Show.u60 val String.nil)
  (term case_lam case_app case_con case_get case_lft case_rgt case_mat case_one case_var)

// Main
// ----

// The n-bit word type
(Word 0) = Uni
(Word n) = (Eit (Box (Word (- n 1))) (Box (Word (- n 1))))

// A n-bit word with all 1's
(Ones 0) = One
(Ones n) = (Rgt (Ones (- n 1)))

// Needle = 0x15783b61d
Needle = 
  (Rgt (Lft (Rgt (Rgt (Rgt (Lft (Rgt (Rgt
  (Rgt (Rgt (Lft (Lft (Lft (Lft (Lft (Rgt
  (Rgt (Rgt (Lft (Rgt (Rgt (Lft (Rgt (Rgt
  (Lft (Lft (Lft (Lft (Rgt (Rgt (Rgt (Lft 
  One))))))))))))))))))))))))))))))))

// Searches a needle in a 2^32 space by optimal brute force
// Main : ∃(x: U32). x == 0x15783b61d
Main =
  let size   = 32
  let type   = (Word size) // u32 type
  let query  = λx(Equal x Needle 0) // query searches for the needle
  (Show (Unwrap (Search size type query)) 0)

Nice, would be perfect for fast symbolic regression :o