subgraph_isomorphism_gpt5.hmv

// =============================
// Core encodings & primitives
// =============================

// Church lists
(Cons h t) = λc λn (c h (t c n))
Nil        = λc λn n

// Pairs
(Pair a b) = λp (p a b)
(Fst p)    = (p λa λb a)
(Snd p)    = (p λa λb b)

// Numeric if: non-zero is true
(If 0 t f) = f
(If x t f) = t

// Boolean-ish helpers on 0/1 numerics
(And a b)  = (If a (If b 1 0) 0)
(Or  a b)  = (If a 1 (If b 1 0))
(Not a)    = (If a 0 1)

// Folds and list ops (fusion-friendly, no intermediates)
(Append xs ys) = (xs λh λr (Cons h r) ys)
(Map xs f)     = (xs λh λr (Cons (f h) r) Nil)
(Filter xs p)  = (xs λh λr (If (p h) (Cons h r) r) Nil)
(Len xs)       = (xs λh λr (+ 1 r) 0)
(Any xs p)     = (xs λh λr (If (p h) 1 r) 0)
(All xs p)     = (xs λh λr (If (p h) r 0) 1)
(Contains xs x)= (xs λh λr (If (== h x) 1 r) 0)

// Assoc lists: List (Pair k v)
(AssocGetD xs k d) = (xs λpr λr (pr λk2 λv (If (== k2 k) v r)) d)
(AssocHas  xs k)   = (xs λpr λr (pr λk2 λv (If (== k2 k) 1 r)) 0)
(AssocSet  xs k v) = (xs λpr λr (pr λk2 λv2 (If (== k2 k)
                                   (Cons (Pair k v) r)
                                   (Cons (Pair k2 v2) r))) (Cons (Pair k v) Nil))

// =============================
// Graph representation
// Graph = Pair Labels Edges
//   Labels : List (Pair node label)
//   Edges  : List (Pair u v)  // store both directions for undirected
// =============================
(Labels G) = (Fst G)
(Edges  G) = (Snd G)
(Nodes  G) = (Map (Labels G) λpr (Fst pr))
(LabelOf G v) = (AssocGetD (Labels G) v  (-1))

// Neighbors and degree
(Neighbors G v) = (Map (Filter (Edges G) λe (e λa λb (== a v))) λe (e λa λb b))
(Degree    G v) = (Len (Neighbors G v))
(Adj       G u v) = (Contains (Neighbors G u) v)

// Symmetric adjacency on pattern graph
(AdjP P u v) = (Or (Adj P u v) (Adj P v u))

// =============================
// Utilities for mapping (pattern->target)
// MapPT : List (Pair p g)
// =============================
(ImgContains map g) = (map λpr λr (pr λk λv (If (== v g) 1 r)) 0)
(MapHas map p)      = (AssocHas map p)
(MapGet map p)      = (AssocGetD map p 0) // used only when (MapHas map p) holds

// =============================
// Domain: List (Pair p Candidates), Candidates : List g
// =============================

// Initial domain: candidate g must match label and have deg ≥
(InitDom P G) =
  (Map (Labels P) λpr
    (pr λp λlabP
      (Pair p
        (Filter (Nodes G) λg
          (And (== labP (LabelOf G g))
               (>= (Degree G g) (Degree P p)))))))

// Domain lookup for p
(DomLookup dom p) = (AssocGetD dom p Nil)

// Refine domain after assigning (p -> g):
//   - For each pv ≠ p that neighbors p on P, keep only xs adjacent to g on G.
(RefineDom P G dom map p g) =
  (Map dom λentry
    (entry λpv λcands
      (If (== pv p)
        (Pair pv cands)
        (If (AdjP P pv p)
          (Pair pv (Filter cands λx (Adj G x g)))
          (Pair pv cands)))))

// =============================
// Variable selection (MRV – minimum remaining values)
// Returns Pair(best_p, best_len), with best_p=-1 if none
// =============================
(SelStep assigned entry best) =
  (entry λp λcands
    (If (Contains assigned p)
      best
      (let len = (Len cands);
       (If (< len (Snd best)) (Pair p len) best))))

(SelectVar dom assigned) =
  let init = (Pair (-1) 1152921504606846976) // huge sentinel (2^60)
  (dom λentry λacc (SelStep assigned entry acc) init)

// =============================
// Labeling for forks: one label per pattern node
// We need lab = index of p in Nodes(P). Index is computed as
//     Pos nodes p := foldr: if h==p -> 0 else 1+r
// It yields position of first occurrence (0..n-1).
// =============================
(Pos nodes p) = (nodes λh λr (If (== h p) 0 (+ 1 r)) 0)

// =============================
// Fork combinator: places a superposition in function position
// to enforce APP-SUP splitting of ctx with the *same* lab.
// For lab n in 0..31. Extend if needed.
// =============================
(Fork  n f g ctx) =
  (If (== n  0) ((#0  { f g }) ctx)
  (If (== n  1) ((#1  { f g }) ctx)
  (If (== n  2) ((#2  { f g }) ctx)
  (If (== n  3) ((#3  { f g }) ctx)
  (If (== n  4) ((#4  { f g }) ctx)
  (If (== n  5) ((#5  { f g }) ctx)
  (If (== n  6) ((#6  { f g }) ctx)
  (If (== n  7) ((#7  { f g }) ctx)
  (If (== n  8) ((#8  { f g }) ctx)
  (If (== n  9) ((#9  { f g }) ctx)
  (If (== n 10) ((#10 { f g }) ctx)
  (If (== n 11) ((#11 { f g }) ctx)
  (If (== n 12) ((#12 { f g }) ctx)
  (If (== n 13) ((#13 { f g }) ctx)
  (If (== n 14) ((#14 { f g }) ctx)
  (If (== n 15) ((#15 { f g }) ctx)
  (If (== n 16) ((#16 { f g }) ctx)
  (If (== n 17) ((#17 { f g }) ctx)
  (If (== n 18) ((#18 { f g }) ctx)
  (If (== n 19) ((#19 { f g }) ctx)
  (If (== n 20) ((#20 { f g }) ctx)
  (If (== n 21) ((#21 { f g }) ctx)
  (If (== n 22) ((#22 { f g }) ctx)
  (If (== n 23) ((#23 { f g }) ctx)
  (If (== n 24) ((#24 { f g }) ctx)
  (If (== n 25) ((#25 { f g }) ctx)
  (If (== n 26) ((#26 { f g }) ctx)
  (If (== n 27) ((#27 { f g }) ctx)
  (If (== n 28) ((#28 { f g }) ctx)
  (If (== n 29) ((#29 { f g }) ctx)
  (If (== n 30) ((#30 { f g }) ctx)
  (If (== n 31) ((#31 { f g }) ctx)
                 ((#0  { f g }) ctx))))))))))))))))))))))))))))))))

// =============================
// Collapse of all labels 0..(n-1) by joining lists
// Join is church-list append; DUP splits by label k
// =============================
(Join a b) = λc λn (a c (b c n))
(Collapse 0 x) = x
(Collapse n x) = (HVM.DUP (- n 1) x λx0 λx1 (Collapse (- n 1) (Join x0 x1)))

// =============================
// Pack/Unpack a triple context (map, dom, assigned)
// =============================
(Ctx m d a) = λk (k m d a)

// =============================
// Consistency test:
//
//   1) injective: g not in image(mapping)
//   2) adjacency-preserving: for all pn neighbor of p already mapped,
//      Adj(G, g, mapping[pn]) must hold
// =============================
(Consistent P G mapping p g) =
  (And (Not (ImgContains mapping g))
       (All (Neighbors P p) λpn
         (If (MapHas mapping pn)
             (Adj G g (MapGet mapping pn))
             1)))

// =============================
// Branch over candidate images of p, all forks sharing label = Pos(nodes,p)
// Each branch receives ctx=(mapping,dom,assigned) via APP-SUP splitting.
//
// Returns: Church list of solutions (each solution is an assoc-list MapPT).
// =============================
(SupChoices P G nodes lab choices mapping dom assigned) =
  (choices
    λg λrest
      let ctx  = (Ctx mapping dom assigned);
      let left = λctx (ctx λm λd λa
                    let m2 = (Cons (Pair (lab) g) m); // note: lab == p index; map key = p itself
                    let d2 = (RefineDom P G d m2 (lab) g);
                    let a2 = (Cons (lab) a);
                    (SolveRec P G nodes d2 m2 a2));
      let right = λctx (ctx λm λd λa
                    (SupChoices P G nodes lab rest m d a));
      ((Fork lab left right) ctx)
    Nil)

// =============================
// Solver (recursive)
// =============================
(SolveRec P G nodes dom mapping assigned) =
  let sel = (SelectVar dom assigned);
  let p   = (Fst sel);
  (If (== p (-1))
      (Cons mapping Nil) // all assigned: emit one solution
      (let choices0 = (DomLookup dom p);
       let choices  = (Filter choices0 λg (Consistent P G mapping p g));
       let lab      = (Pos nodes p);
       (SupChoices P G nodes lab choices mapping dom assigned)))

// Top-level: returns a *collapsed* list of solutions
// Each solution is an assoc-list (Pair p g) for p in 0..n-1.
(FindSubiso P G) =
  let nodes = (Nodes P);
  let dom   = (InitDom P G);
  let solsS = (SolveRec P G nodes dom Nil Nil);
  (Collapse (Len nodes) solsS)

// -----------------------------
// Pretty-print helpers (optional):
// vectorize a mapping into [g0,g1,...,g(n-1)] in node order
// -----------------------------
(MapVec nodes mapping) =
  (Map nodes λp (MapGet mapping p))

(MapVecs nodes maps) =
  (Map maps λm (MapVec nodes m))

// ===================================
// Example graphs (exactly as in the earlier Python demo)
// G: 1-A -- 2-B -- 3-A
// P: 0-A -- 1-B
// Labels: A=0, B=1
// ===================================
(G_labels) =
  (Cons (Pair 1 0)
  (Cons (Pair 2 1)
  (Cons (Pair 3 0) Nil)))

(G_edges) =
  (Cons (Pair 1 2)
  (Cons (Pair 2 1)
  (Cons (Pair 2 3)
  (Cons (Pair 3 2) Nil))))

(G) = (Pair (G_labels) (G_edges))

(P_labels) =
  (Cons (Pair 0 0)
  (Cons (Pair 1 1) Nil))

(P_edges) =
  (Cons (Pair 0 1)
  (Cons (Pair 1 0) Nil))

(P) = (Pair (P_labels) (P_edges))

// A second test: ring(8, C=2) vs. path(4, C=2)
// Build helpers
// ring n: nodes 0..n-1 labelled L; edges both directions
(RingLab n L i acc_lab acc_edg) =
  (If (== i n)
    (Pair acc_lab acc_edg)
    (let lab' = (Cons (Pair i L) acc_lab);
     let a    = i;
     let b    = (% (+ i 1) n);
     let edg' = (Cons (Pair a b) (Cons (Pair b a) acc_edg));
     (RingLab n L (+ i 1) lab' edg')))
(Ring n L) =
  let lr = (RingLab n L 0 Nil Nil);
  (Pair (Fst lr) (Snd lr))

// path m: nodes 0..m-1 labelled L; edges both directions
(PathLab m L i acc_lab acc_edg) =
  (If (== i m)
    (Pair acc_lab acc_edg)
    (let lab' = (Cons (Pair i L) acc_lab);
     let edg' = (If (== i 0)
                   acc_edg
                   (let a = (- i 1); let b = i;
                        (Cons (Pair a b) (Cons (Pair b a) acc_edg))));
     (PathLab m L (+ i 1) lab' edg')))
(Path m L) =
  let pr = (PathLab m L 0 Nil Nil);
  (Pair (Fst pr) (Snd pr))

// ===================================
// Main: returns a church-list of solutions for both tests,
// each solution vectorized as [g0,g1,...]. Outer list has 2 items.
// ===================================
(Main) =
  let sols1 = (FindSubiso (P) (G));
  let vecs1 = (MapVecs (Nodes (P)) sols1);

  let G2    = (Ring 8 2);
  let P2    = (Path 4 2);
  let sols2 = (FindSubiso P2 G2);
  let vecs2 = (MapVecs (Nodes P2) sols2);

  (Cons vecs1 (Cons vecs2 Nil))