Prolog in C#, declaratively

Every serious C# codebase eventually grows a rules engine. It starts as a switch statement, becomes a chain of ifs with comments explaining the order, and ends as a class nobody wants to touch because the logic and the plumbing have fused. The reason is that C# is a language for saying how; the rules were always a statement of what.

Shin is MLambda's answer: a rule-based expert-system language in which you declare facts, rules and queries the way you would in Prolog or Datalog — and which compiles, at build time, into ordinary C# that links against a runtime engine. No interpreter to embed, no strings to parse at startup. The rules are source; the C# is generated.

What a Shin program looks like

Facts are typed records — Haskell-style algebraic data types with product, sum and payloads. Rules are predicates over them: a when clause that is a full first-order formula with modal operators, and a then clause that asserts, retracts, emits or binds. Queries use Prolog's :-, compose rules and other queries, recurse freely, and return either a truth value, a list comprehension, or a bound last parameter — Prolog's mode discipline, made explicit.

Here is a rule file from MLambda's own analysis module, deciding whether an analysed specification says enough to be finished:

record StoryFacts { id: String, name: String, narrative: String, acceptance: String, cases: String }

-- A story with no acceptance cannot be accepted: that is an error, not taste.
rule story_without_acceptance(s: StoryFacts)
  when s is StoryFacts { acceptance: "no", ... }
  then assert SpecFinding { id: s.id, severity: "error", says: "no acceptance scenario" }

Read the comment in the original source: "Whether a trigger is PRESENT is a fact; whether it is a GOOD trigger is not, and a rule that pretended otherwise would be guessing in the voice of a checker." That sentence is the whole discipline. Rules decide facts; they do not impersonate judgment.

Pattern matching that earns the word

Matching in Shin is structural over records: bare-name variables bind, as binds the whole match, ... takes the rest, { name, ... } is field shorthand, and | gives value disjunction inside a pattern. Every parameter is typed — a concrete record type or a type variable in the ML style ('a) — and (c: Class) is sugar that desugars into a type-constraint conjunct, so the unifier always knows what it is unifying. Rules with the same name and different parameter types dispatch by backtracking on pattern failure: overloading with no dispatch machinery, just Prolog. A singleton-variable diagnostic catches the typo you would otherwise ship.

Three engines under one knowledge base

Most rule systems pick one evaluation strategy. Shin's kernel is a hybrid, and each part is there because it earns its keep. Forward chaining is semi-naive Datalog evaluation — the algorithm behind Soufflé and DDlog — deriving consequences as facts arrive. Backward chaining is SLD resolution with tabling, so recursive queries terminate, and stratified negation as failure, with unstratifiable programs rejected at build time rather than looping at run time. Term rewriting is a Stratego-style strategy interpreter — innermost, outermost, and the classic combinators — over typed term trees.

The knowledge base underneath all three is an immutable persistent structure (HAMT-backed). Every assert returns a new version with structural sharing. Reads are lock-free, tabling is trivially safe because a memo key is a goal plus a version, and you get time-travel for free: any earlier state of the world is still a valid value.

The intelligence kit

On top of the kernel: justification-based truth maintenance, so retracting a premise cascade-retracts everything that depended on it. Aggregation, incremental over the delta. Defeasible rules with explicit strength and defeats. Probabilistic facts with confidence propagation. Meta-rules that inspect the engine's own execution traces to ask whether a program is sound, complete, terminating or consistent. And two constructs Prolog never had as first-class citizens: explain, which returns the proof tree behind an answer, and abduce, which returns the minimal set of facts that would make a goal true. When the reasoning layer inside Turing refuses a proposal, the refusal comes with its proof.

Four families of modal logic are available in when clauses and assertions: temporal (LTL), epistemic (S5), deontic (KD) and alethic (S5). They are strictly unary at the surface — necessary (P and Q) is a syntax error; you must distribute it — which forces correct distribution and keeps the parser honest. The engine evaluates them over explicit Kripke frames it maintains internally; the language surface stays small.

Metaprogramming: rules become C# at build time

This is the part that makes Shin usable in an ordinary .NET solution. A .shin file is compiled by a Roslyn incremental source generator during MSBuild. The generator parses, desugars to a core AST, normalises the first-order formulas into Horn clauses — Kripke encoding for the modal operators, CNF, skolemisation — and emits C#: a Tags class, a sealed record per fact type, and an engine class that registers the rules with the runtime. The generated file for the rule above is called Specification_staticEngine.g.cs and reads like code a careful engineer would have written. Build-time diagnostics (SHIN0001–SHIN0099) catch the untyped parameter, the unstratifiable negation, the modal operator in the wrong position — before anything runs.

The consequence is that a C# project can contain Prolog-style knowledge as source, with IntelliSense-adjacent tooling, versioned in git, checked in CI, and callable from ordinary code as typed methods returning IAsyncEnumerable<Binding>. Declarative where the logic is declarative, imperative where it isn't, and the boundary is a file extension.

Theorem proving, and proving the prover

The deepest use of Shin inside MLambda is on the TLA+ checker in Genesis. A model checker's verdict rests on its semantics — how it evaluates an LTL formula over a lasso, how it reduces a TLA+ expression. If the checker and the certifier share that code, a bug in one is a bug in both, and the certification proves nothing. So the verdict-bearing semantics are being expressed a second time, as Shin rules: LTL over a lasso as a least fixpoint over position facts, and TLA+'s operational semantics as a rewrite system of about thirty rules normalised by Shin's own innermost strategy. Every reported violation is then evaluated through both the C# evaluator and the Shin semantics, and if they disagree, the checker throws rather than reports. Two independent implementations of the meaning, agreeing, is how you trust a verdict — and one of them is a declarative program in a language that compiles to C#.

Shin is also used to analyse Shin: data-flow, constraint-based and abstract-interpretation analyses from Nielson, Nielson and Hankin, written as Shin rules over Shin programs, because a Datalog engine is already a least-fixpoint engine and that is exactly what a monotone framework needs.

Where it sits

Shin is one of the eleven Genesis packages and ships MIT on NuGet. Inside Turing it is the reasoning layer's proof engine — the thing that decides, after the language model has proposed. It is research-grade and multi-year by design; the runtime's stated priority order is correctness, then latency, then throughput, then memory, and optimisation waits until the engine is provably conformant to its formal semantics. That order is the reason it is trusted with verdicts.

---

Genesis — MIT, on NuGet. Documentation at genesis.mlambda.net.