Inductive Synthesis: from BDD scenarios to PatLang code

A working inductive logic programming (ILP) system, built entirely in PatLang, that treats Gherkin-style BDD scenarios (Given/When/Then) as a training corpus and induces real PatLang rule clauses that satisfy them — then emits literal, compilable PatLang source for the result. This isn't a toy: it reproduces the actual routing table from the router DSL demo and the actual dependency-graph rules from the goal-oriented build demo from nothing but example scenarios, and when induction can't find an answer, it can point at exactly which example is the problem and ask a targeted question about it, rather than failing silently.

Everything below is real, working code — five library modules (self_hosting/lib/synthesis*.patlang) and eleven self-hosted test scripts, run entirely PatLang-side: self_hosting/tools/run_synthesis_selftests.patlang runs every suite as its own subprocess (pat --ir-run) and reports an aggregate pass/fail, with no Rust toolchain, cargo, or cucumber involved anywhere in exercising this system — only the base pat runtime that executes any PatLang program at all. See the Logic / Goal-Oriented section for the underlying rule_add/solve resolution engine this is all built on top of, and the BDD framework page for the Gherkin-style test runner whose vocabulary (Given/When/Then) this reuses directly.

Why BDD is the right input format for this — not just a convenient one

A Given/When/Then scenario already has exactly the shape induction needs, for free:

  • Given is the precondition — the world-state / background facts a hypothesis has to be consistent with.
  • When is the input — the concrete value being classified or acted on.
  • Then is the expected postcondition — exactly the label a learning system needs as ground truth.

That's the same (background knowledge, positive/negative examples) → rules shape every ILP system from Aleph to Metagol takes as input — BDD scenarios don't need translating into that shape, they already are it. Three consequences that make this specifically valuable, not just tidy:

  • The requirements document and the training corpus are the same artifact. A product owner or QA engineer writing scenarios in plain English is, without knowing it, authoring the exact input this system consumes. Nobody has to hand-translate "the system should do X when Y" into a labelled dataset — the scenario already is one.
  • A failed induction reads like a normal BDD failure, not a stack trace. Ordinary test-driven development already trains people to read a failing scenario as "what's wrong with my understanding of the requirement," not "what's wrong with the code." The gap-diagnosis output below (Worked example 3) extends that same reading: a scenario the system can't satisfy comes back as a plain-English question about a missing fact, in the same register as the scenario itself.
  • Coverage growth and rule growth are visibly linked. Add a new scenario, and you can watch the induced rule set either absorb it into an existing branch (the parsimony property every worked example below checks explicitly) or split into a new one — the BDD suite itself is the living record of why the generated code has the shape it does, not a separate design document that can drift out of sync with it.

Worked example 1: flat classification (reproducing a routing table)

The simplest shape: group examples by their expected output label into one PatLang predicate per real category, instead of one fact per example. Six toy scenarios classify a digit into a band:

Given the input is "1"
Then the category is "low"

Given the input is "2"
Then the category is "low"

Given the input is "5"
Then the category is "mid"
...

Six examples, but only three real categories — synth_induce (self_hosting/lib/synthesis.patlang) groups them accordingly and the self-test asserts exactly that:

let categories = synth_induce(examples)
check("induction finds exactly 3 real branches, not 6", to_num(list_len(categories)), 3)

The same mechanism, unchanged, was pointed at a real demo instead of toy data: eight example HTTP requests, four real handlers (two requests each map to UserController_index, two to UserController_update, and so on), reproducing the router DSL demo's hand-written table:

let sols_index = solve("UserController_index", ["GET /users"])
check("GET /users routes to UserController_index (matches router_dsl_demo)",
      to_num(list_len(sols_index)) > 0, true)

This reproduction caught a genuine bug in the process: the native resolver treats any argument string starting with an uppercase letter as a Prolog logic variable, not a constant — "GET /users" was silently unifying with everything until every induced/queried value got grounded with a lowercase marker first. The toy digit corpus ("1", "5", "9") never triggered it; a corpus drawn from a real domain immediately did. One more reason real examples, not just synthetic ones, belong in the suite.

Worked example 2: a recursive rule (reproducing the build-graph demo)

Flat classification can't express recursion. The goal-oriented build demo hand-writes:

rule buildable(X) :- unchanged(X).
rule buildable(X) :- dep(X, Y), buildable(Y).

self_hosting/lib/synthesis_recursive.patlang induces exactly this from three example queries — buildable(a) and buildable(c) positive, buildable(d) negative — plus the same dep/unchanged background facts the demo declares, via a small Metagol-style search over base/chain clause templates:

let winner = synth2_induce_chain("buildable", ["unchanged"], ["dep"], background_src, queries)
check("induces the base clause via unchanged", winner[0], "unchanged")
check("induces the chain clause via dep (the genuinely recursive part)", winner[1], "dep")

The emitted, compiled program matches the hand-written demo's own printed verdicts — 1 solution for a, 0 for d — exactly, on the first real run.

Worked example 3: conjunctions, and rejecting a distractor

self_hosting/lib/synthesis_conjunctive.patlang generalizes further: instead of one fixed template, it searches conjunctions of background predicates, smallest first — the parsimony property extended from "fewest branches" to "fewest conditions per branch." Five example people, one of whom (dave) is also, coincidentally, a student:

let winner = synth3_induce_conjunction("eligible", ["has_job", "good_credit", "is_student"], background_src, queries)
check("the smallest separating conjunction has exactly 2 predicates", to_num(list_len(winner)), 2)
check("the distractor is_student does not survive in the induced rule", synth_list_contains(winner, "is_student"), false)

is_student is true of a positive example (dave) but never actually required — alice is eligible without it. Smallest-first search finds eligible(X) :- has_job(X), good_credit(X) and never lets the merely-correlated predicate leak into the induced rule.

A companion test proves the opposite case matters too: examples with no separating conjunction at all (an XOR-shaped positive/negative split) must come back as "no hypothesis found," not an overfit answer. Every worked example on this page has a matching negative test like this — the engine is checked on what it correctly refuses to solve as carefully as what it solves.

Worked example 4: bottom-up induction, and turning a gap into a question

The modules above are all top-down: guess a clause shape, brute-force every combination the template allows, test each blindly. self_hosting/lib/synthesis_lgg.patlang goes bottom-up instead, the way real ILP systems like Aleph/Progol's "bottom clause" construction actually work: for each positive example, walk the background-fact graph outward from that example's value to find a witnessed chain of relations — real evidence, not a guess — then generalize across examples by taking the longest common prefix of their witnessed chains. That prefix-taking literally is anti-unification: the terms being generalized are predicate sequences, and dropping the tail where two examples' evidence diverges is the generalization step.

The classic ILP "grandparent" benchmark, solved this way:

let facts = [
  synth5_fact_binary("parent", "alice", "bob"),
  synth5_fact_binary("parent", "bob", "carol"),
  synth5_fact_binary("parent", "dave", "erin"),
  synth5_fact_binary("parent", "erin", "frank"),
  synth5_fact_binary("parent", "george", "henry")
]
let result = synth5_induce("grandparent", ["alice", "dave"], queries, facts, 2)
check("derives the same 2-hop parent/parent chain, but bottom-up", result[0], "ok")

Because the mechanism is evidence-driven, a failed induction carries its own explanation. synth5_induce returns a tagged diagnosis, not a bare pass/fail — and synth5_format_diagnosis turns that diagnosis into an actual question, addressed to whoever wrote the scenarios:

let queries = [
  synth2_query("grandparent", "alice", true),
  synth2_query("grandparent", "isaac", true)
]
let outcome = synth5_induce_and_ask("grandparent", ["alice", "isaac"], queries, facts, 2)

> outcome[0]  # the diagnosis
["no_witness", ["isaac"]]

> outcome[1]  # the question, generated from it
["The scenarios say grandparent(\"isaac\") should hold, but no background fact
 connects \"isaac\" to anything at all. Is a fact about \"isaac\" missing from
 the background knowledge, or should this scenario be removed?"]

The scenario said isaac should be a grandparent; the background facts simply never mention him. Rather than a bare test failure, that comes back as a specific, answerable question — and the same mechanism catches the opposite mistake too. A negative example sharing the identical witnessed relation chain as the positives (representing some real-world distinction the given facts don't capture) produces a different, equally specific question:

> outcome[0]  # eve has the same 2-hop parent chain as alice/dave, but is declared NOT a grandparent
["conflict", [["grandparent", "eve", false,
  "negative example wrongly covered by the induced rule -- background facts
   don't yet distinguish it from the positives"]]]

> outcome[1]
["The induced rule also matches \"eve\", but the scenarios say
 grandparent(\"eve\") should NOT hold. Is there a background fact that
 distinguishes \"eve\" from the positive examples that's missing, or is an
 additional condition (a predicate not offered to the search) needed?"]

Both questions name the exact example at fault and the exact kind of gap (missing evidence vs. missing distinction) — the difference between a test suite that says "3 failed" and one that tells you what to go check first. Confirmed to work across three genuinely different relational shapes, not just the grandparent benchmark: a depth-1 chain (has_mentor(X) :- mentored_by(X, Y), the shallowest possible case), and a depth-3 chain (origin_traceable(X) :- supplies(X,Y), supplies(Y,Z), supplies(Z,W), a supply-chain traceability example), each with their own gap and conflict scenarios.

Worked example 5: composing a chain with a filter, via real anti-unification

Every module above was still a separately hard-coded template: milestone 3's conjunctions applied only to the query argument itself, milestones 4-6's chains had no way to attach a condition on where the chain ends. A rule like "a grandparent whose grandchild is young" needs both at once, and neither module alone could induce it.

The fix generalizes the clause body itself into a real literal list: for each positive example, walk every witnessed relation chain and, at every node along it — including the query argument, not just the endpoint — record every unary fact true there. Merging two examples' evidence is genuine anti-unification (in the Plotkin sense): the chain generalizes by common prefix as before, and at each surviving node the two examples' unary-fact sets are intersected, so a predicate only survives if it held at that same position for both:

let facts = [
  synth5_fact_binary("parent", "alice3", "bob3"),
  synth5_fact_binary("parent", "bob3", "carol3"),
  synth5_fact_unary("young", "carol3"),
  synth5_fact_binary("parent", "dave4", "erin4"),
  synth5_fact_binary("parent", "erin4", "frank4"),
  synth5_fact_unary("young", "frank4"),
  synth5_fact_unary("manager", "erin4")   # a distractor, on an INTERMEDIATE node
]
let result = synth7_induce("young_grandparent", ["alice3", "dave4"], queries, facts, 2)

> synth7_emit_clause("young_grandparent", result[1])
"rule young_grandparent(X) :- parent(X, Y), parent(Y, Z), young(Z).\n"

Neither prior module's representation could even express that rule. The manager fact on erin4 (one example's intermediate node) is correctly dropped — it isn't true of the other example's corresponding node, so intersection removes it, the same distractor-rejection property from the conjunction worked example, now proven to hold mid-chain as well as at the query argument. And because this is genuinely one engine rather than two, the earlier pure-conjunction and pure-chain cases still induce identically through it — nothing was lost generalizing the representation.

Worked example 6: two (or three) unrelated reasons, one target predicate

Anti-unification generalizes examples toward each other, but some concepts genuinely shouldn't be generalized toward each other at all. "Eligible for a discount as a veteran, or as an enrolled student" is two facts that share nothing — a veteran fact and a student-plus-enrolled fact have no common structure, and forcing them into one anti-unified clause would either lose one of the two reasons or, worse, silently invent a shared condition neither example actually has.

Rather than replacing the anti-unification engine, a clustering step wraps it: examples are grouped so that each group's evidence does share structure, a new group is opened only when an example can't join any existing one, and one clause is emitted per group. Since multiple rule head(...) :- body. clauses for the same predicate are already ordinary Prolog disjunction, that's the entire mechanism — no new resolution logic:

let facts = [
  synth5_fact_unary("veteran", "alice"),
  synth5_fact_unary("student", "bob"),
  synth5_fact_unary("enrolled", "bob"),
  synth5_fact_unary("student", "dave")   # student but NOT enrolled -- a partial match
]
let result = synth8_induce("discount_eligible", ["alice", "bob"], queries, facts, 2)

> synth8_emit_clauses("discount_eligible", result[1])
"rule discount_eligible(X) :- veteran(X).
rule discount_eligible(X) :- student(X), enrolled(X).
"

dave (a student who isn't enrolled) correctly matches neither clause — a genuine test of whether clustering could accidentally launder a near-miss into a match, since he shares a predicate name with one real cluster but not its full conjunction. Clustering only splits when it has to: two examples whose evidence genuinely does share structure still collapse into a single clause exactly as milestone 7 would produce alone, and a three-unrelated-reasons version of this same domain (enterprise account, or paid-with-an-open-incident, or partner) correctly finds three clauses rather than over- or under-splitting.

Worked example 7: testing several hypotheses without spawning several processes

Every hypothesis test above runs in its own fresh subprocess, because the underlying resolver has no way to un-register a rule once added (rule_add has no retract), so a wrong guess can't be safely tried and rolled back in the same process. That's still true — but it turns out several DIFFERENT hypotheses can safely share one subprocess anyway, as long as each is registered under its own uniquely-renamed head predicate. solve() only ever follows rules for the predicate actually queried, so two unrelated candidate rule sets sitting in the same append-only rule store, under different names, never see each other:

let batch = [
  ["0", "rule reach2(X) :- dep(X, Y), dep(Y, Z).\n", queries_for_reach2],
  ["1", "rule reach1(X) :- dep(X, Y).\n",             queries_for_reach1]
]
let results = synth9_batch_test_hypotheses(background_src, batch)
# both candidates verified correctly, in ONE process spawn

Applied to the conjunction search (worked example 3): what used to be up to 2n subprocess spawns in the worst case became exactly one, testing every candidate conjunction at once and picking the smallest passing one — same result, no more per-candidate spawn cost.

The genuinely useful consequence, though, is what cheap batched verification affords elsewhere: comparing more than one candidate solution, not just more than one candidate hypothesis within a single search. The clustering behind worked example 6 was originally a single greedy pass, processing examples in whatever order they were given. A second, order-insensitive strategy now runs alongside it — at every step it looks at every still-unassigned example against every existing group (and the option of starting a new one) and commits to whichever single choice is richest overall, not just the richest choice for whichever example happens to come first. Neither strategy is guaranteed optimal on its own; running both and keeping whichever verifies with fewer clauses is. In one domain built specifically to probe this (not cherry-picked to flatter the new strategy), the order-insensitive pass actually did worse — four clauses where the original found two — and the system correctly kept the two-clause result anyway, verified together in a single batched call rather than two separate spawns.

Stress-testing against a real project, not another toy domain

Every worked example above was proven against either a toy corpus or a real demo already living inside PatLang's own codebase. The next test was different on purpose: point the whole system at a genuinely external, pre-existing, untested project and see what breaks. The target was fantpop, a Ruby fantasy-population/genealogy simulator with essentially no test coverage of its own — the Ruby source itself was the only authority on its actual behavior, warts included. A research pass over the Ruby found real bugs worth naming (siblings misclassified as "0th cousin" by one relatedness calculation while a second, disagreeing calculation in the same codebase gets it right; a self-as-sibling bug from a hash/array type mismatch; a marriage-candidate selection bug where the randomly sampled partner and the one actually married can differ) — then a new, sibling PatLang-only project (fantpop-patlang) was scoped to reverse-engineer the corrected, intended behavior as BDD scenarios and hand them to this induction engine.

Trying to actually scope those scenarios surfaced three real, previously-undiscovered gaps immediately — not hypothetical, hit on the first attempt to write them down as something inducible:

  • No two-ended relational joins (sibling(X, Y) needs X and Y to each independently reach a shared node).
  • No genuine two-argument relations at all, which turned out to be the more fundamental gap underneath the first one: every chain clause emitted existentially-quantifies its final variable rather than binding it as a real second head argument, so even the "easy" case (ancestor_of(X, Y), a plain single-line chain) wasn't actually inducible — only existential unary predicates like "X has some grandchild" were.
  • No comparison between two different entities' attribute values (needed for "X and Y are the same social class").

Two of the three are now fixed. synth10_induce takes example (X, Y) pairs instead of just X values, searches for witnessed chains from X that land exactly on Y, and emits the chain's final variable literally as Y:

let result = synth10_induce("grandparent_of", [["alice", "helen"], ["dave", "frank"]], queries, facts, 2)

> synth10_emit_relation("grandparent_of", result[1])
"rule grandparent_of(X, Y) :- parent(X, Y1), parent(Y1, Y).\n"

That made the second gap (joins) tractable, since a join is really "X reaches a specific Y" performed from two directions at once, meeting in the middle. synth11_induce searches backward from both X and Y for a shared predecessor node, and reuses milestone 9's same-predicate-family isolation trick from the batching worked example above:

let result = synth11_induce("sibling", [["bob", "carol"], ["helen", "ida"]], queries, facts)

> synth11_emit_join("sibling", result[1])
"rule sibling(X, Y) :- parent(Z, X), parent(Z, Y).\n"

Both landed with a first-run pass on their own selftests. The sibling one comes with an explicit, deliberately-not-hidden limitation check built in: the induced rule has no way to require X != Y (there's still no inequality operator anywhere in the engine — that's the third gap, still open), so querying it with the same individual for both arguments incorrectly succeeds. The selftest asserts that this happens, rather than silently working around it or pretending it doesn't.

A fourth, unplanned finding came from a mid-conversation correction, not from the code: the first pass at a marriage-eligibility rule modeled same-class-and-opposite-sex as a strict requirement, which turned out to be wrong — the actually-intended design allows cross-class and same-sex marriage, just less commonly (same-sex marriage simply produces no biological offspring, a separate concern). A rule like that is inherently probabilistic, and a single Given/Then assertion can't verify a probability. self_hosting/lib/stochastic_bdd.patlang runs many trials and checks that the empirical success rate falls within a statistically-sized tolerance band (the standard error of a proportion, sqrt(p(1-p)/n), scaled by a few standard deviations) of a declared probability, rather than asserting one exact outcome — deliberately kept separate from the rule-induction engine, since this verifies a hand-authored implementation's declared probability against its own behavior, it doesn't derive a probability from data.

One more fix came out of actually trying to use the engine from a separate project: every hypothesis-testing function shelled out to a working-directory-relative path for the engine's own interpreter, so calling the engine from anywhere other than its own repo only worked by accident of the calling shell's current directory. Now absolute, so a project like fantpop-patlang can call the induction engine from its own directory, exactly as intended for an engine meant to be used by other projects, not just tested against itself.

Current limits, honestly

Two gaps remain. The clustering behind worked examples 6 and 7 is still not globally optimal — finding the true minimum number of clusters that anti-unify is a much harder combinatorial problem than running two heuristics and keeping the better one, and a domain adversarial enough could still beat both. And there's still no comparison between two different entities' attribute values (no equality/inequality operator between two nodes anywhere in the engine) — the third fantpop-motivated gap above, needed for genuine pairwise rules like "X and Y are the same social class" or a real X != Y guard on the induced sibling relation. Both are exactly the kind of gap that's easy to name because the system is small enough to read end to end; see PatLang Best Practices and Capabilities & Honest Limitations for the same house style applied to the rest of the language.

Resolved: the witness search used to take the first matching background fact at every hop, so a fact graph with real branching only ever explored whichever fact happened to be declared first; the engine was a fixed library of separate clause-shape templates rather than one that derives structure from evidence; it couldn't induce a rule needing several independent alternative bodies; search cost grew with hypothesis-space size because every candidate needed its own subprocess; no genuine two-argument relation was inducible, only existential unary predicates over chains; and there was no way to induce a relation joining two independently-reached nodes. All four of the limits originally named for this system, plus two more found stress-testing it against a real project, are now fixed — see The Journey of Building PatLang, Continued for the full story.