This document presents Gph-enriched Lawvere theories and Graph-Structured Lambda Theories (GSLTs) as alternatives to full OSLF when bound variables can be eliminated through reflection or combinators. These approaches directly capture operational semantics as graphs enriching the hom-sets.
Target audience: Compiler engineers implementing operational semantics
Primary Sources:
Most of what you need to implement (handles 80% of cases):
Skip for initial implementation:
// GSLT representation
struct GSLT {
name: String,
generating_sorts: Vec<Sort>, // P, N, R, etc.
generating_morphisms: Vec<Morphism>,
interaction: Option<Morphism>, // The magmal operation
structural_equations: Vec<Equation>,
reductions: Vec<Reduction>,
}
struct Sort {
name: String,
is_process_sort: bool, // P
is_reduction_sort: bool, // R
}
struct Morphism {
name: String,
domain: Vec<Arity>,
codomain: Sort,
}
enum Arity {
Sort(Sort),
Product(Box<Arity>, Box<Arity>),
Exponential(Box<Arity>, Box<Arity>),
Unit, // 1
}
struct Reduction {
name: String,
inputs: Vec<(String, Arity)>,
source_equation: String, // src(r(...)) = ...
target_equation: String, // tgt(r(...)) = ...
}
| Component | What It Specifies | Implementation |
|---|---|---|
| Generating sorts | Base types (P, N, R, ...) | Enum variants |
| Generating morphisms | Term constructors | AST node types |
| Interaction | Binary reduction trigger | Pattern match target |
| Structural equations | Equivalence classes | Normalization rules |
| Reductions | Computation steps | Reduction rules |
This table shows how the same concepts manifest across different calculi.
| Feature | Lambda | SKI | RHO | Ambient | MeTTa |
|---|---|---|---|---|---|
| Generating Sorts | P | P | P, N | P, N, M | Term, State, KB, List, MSet |
| Reduction Sort | R | R | R | R | R (state transitions) |
| Binding | Lam: (P->P)->P | None | ?: N x (N->P)->P | nu: (N->P)->P | Pattern vars |
| Interaction | App | App | | (par) | | (par) | State transition |
| Reflection | None | None | @, * | None | quote, eval |
GSLT Lambda:
Generating Sorts: (none beyond P, R)
Generating Morphisms:
s, t : R -> P ; Graph structure
App : P x P -> P ; Application
Lam : (P -> P) -> P ; Abstraction
Interaction: App
Reductions:
Beta : (P -> P) x P -> R
Beta(K, N) : App(Lam(K), N) ~> ev(K, N)
Head : R x P -> R ; In-context
Head(r, B) : App(s(r), B) ~> App(t(r), B)
GSLT SKI:
Generating Sorts: (none beyond P, R)
Generating Morphisms:
s, t : R -> P
S : 1 -> P
K : 1 -> P
I : 1 -> P
App : P x P -> P
S1 : P -> P ; S with 1 arg
S2 : P x P -> P ; S with 2 args
K1 : P -> P ; K with 1 arg
Interaction: App
Structural Equations:
App(S, x) = S1(x)
App(S1(x), y) = S2(x, y)
App(K, x) = K1(x)
Reductions:
Sigma3 : P x P x P -> R
Sigma3(x, y, z) : App(S2(x, y), z) ~> App(App(x, z), App(y, z))
Kappa : P x P -> R
Kappa(x, y) : App(K1(x), y) ~> x
Iota : P -> R
Iota(x) : App(I, x) ~> x
GSLT RHO:
Generating Sorts: N (names)
Generating Morphisms:
s, t : R -> P
0 : 1 -> P ; Nil process
| : P x P -> P ; Parallel
! : N x P -> P ; Output (lift)
? : N x (N -> P) -> P ; Input
* : N -> P ; Dereference (drop)
@ : P -> N ; Quote
Interaction: | (parallel composition)
Structural Equations:
|(P, 0) = P ; Unit
|(P, Q) = |(Q, P) ; Commutativity
|(|(P, Q), R) = |(P, |(Q, R)) ; Associativity
@(*x) = x ; Quote-drop identity
Reductions:
Comm : N x (N -> P) x P -> R ; Communication
Comm(x, K, Q) : |(?(x, K), !(x, Q)) ~> ev(K, @(Q))
ParL : R x P -> R ; In-context (left)
ParL(r, Q) : |(s(r), Q) ~> |(t(r), Q)
ParR : P x R -> R ; In-context (right)
ParR(P, r) : |(P, s(r)) ~> |(P, t(r))
GSLT Ambient:
Generating Sorts: N (names), M (capabilities)
Generating Morphisms:
s, t : R -> P
0 : 1 -> P
| : P x P -> P
[] : N x P -> P ; Ambient bracket
. : M x P -> P ; Capability prefix
nu : (N -> P) -> P ; Restriction
! : 1 -> P ; Replication
in : N -> M ; Enter capability
out : N -> M ; Exit capability
open : N -> M ; Open capability
Interaction: | (parallel)
Reductions:
In : N x N x P x P x P -> R
In(n, m, Q, R, S) : |([](n, |(.(in(m), Q), R)), [](m, S))
~> [](m, |([](n, |(Q, R)), S))
Out : N x N x P x P x P -> R
Out(n, m, Q, R, S) : [](m, |([](n, |(.(out(m), Q), R)), S))
~> |([](n, |(Q, R)), [](m, S))
Open : N x P x P -> R
Open(n, P, Q) : |(.(open(n), P), [](n, Q)) ~> |(P, Q)
| Aspect | Lambda | SKI | RHO | Ambient |
|---|---|---|---|---|
| # of base reductions | 1 (beta) | 3 (S, K, I) | 1 (comm) | 3 (in, out, open) |
| Duplication in reductions | None | S (z appears 2x) | Comm (x appears 2x) | All (n, m appear 2x) |
| Structural equations | None | Partial application | Par monoid, quote-drop | Par monoid |
| Names | No | No | Yes (via reflection) | Yes (primitive) |
| Mobility | No | No | No | Yes |
Full OSLF (Native Type Theory) handles arbitrary binding structures via presheaves, but this complexity is unnecessary when:
The key insight from Stay & Meredith (2017):
"With nominal features eliminated as syntactic sugar via reflection, multisorted Lawvere theories enriched over graphs suffice to capture the operational semantics of the calculus."
| Aspect | Gph-enriched Lawvere | OSLF/Native Types |
|---|---|---|
| Binding | Via reflection/combinators | Directly via presheaves |
| Complexity | Simpler | More general |
| Types | Sorts in multi-sorted theory | Predicates on terms/behavior |
| Rewrites | Graph edges in hom | Internal graph + modalities |
| Best for | Name-free calculi | Full nominal calculi |
While basic Gph-theories capture operational semantics, Graph-Structured Lambda Theories (GSLTs) extend this framework with:
GSLTs provide a complete framework for:
A directed multigraph G consists of:
s t
E ─────> V <───── E
Multiple edges between the same vertices are allowed (multi-graph).
Gph is the category where:
Gph is cartesian closed:
G^H$ exist (graph of homomorphisms from H to G)A category enriched over Gph has:
The category Th(Gph) has:
s
───────>
R P
───────>
t
A graph-structured theory Th is equipped with a functor from Th(Gph) to Th, embedding this basic graph structure.
A multisorted Lawvere theory L consists of:
Bill Lawvere pioneered the use of categories to capture grammars modulo equations for structural congruence. Lawvere proved that his theories correspond to finitary monads. Todd Trimble generalized this to multisorted Lawvere theories with a similar monadicity theorem.
A Gph-theory is a Lawvere theory where:
Hom_G(A, B) = ⟨V, E, s, t⟩
Where:
Given f ⇒ f' : A → B and g : B → C, we get:
g ∘ f ⇒ g ∘ f' : A → C (post-composition)
Similarly for pre-composition. This makes composition a graph morphism.
Lawvere's original theories were cartesian categories (finite products only). While it is possible to define bound variables and substitution in a Lawvere theory, it is cumbersome and not particularly enlightening.
Lambda theories use cartesian closed categories instead, which handle bound variables and substitution automatically via the internal hom objects.
GSLTs are Lawvere theories equipped with extra structure and stuff that allow us to:
A Graph-Structured Lambda Theory (GSLT) is:
Multi-sorted: At least two generating sorts—one for processes (P) and one for rewrites (R)
Graph-structured: A functor from Th(Gph) → Th embedding the source/target maps s, t : R → P
Magmal: A distinguished binary morphism $\odot$ : X × Y → P called the
interaction, where X, Y are sorts
Lambda theory: A cartesian closed category, automatically handling bound variables via exponential objects
The term "magmal" refers to the algebraic structure where we have a binary operation
(the interaction $\odot )$ without requiring associativity or other laws. This is
appropriate because:
In lambda calculus, beta reduction is of the form:
((λx.T) U) ~> T[U/x]
whose source is an application of one process to another
In pi calculus, the comm rule is of the form:
for(y <- x)P | x!z ~> P[z/y]
whose source is a juxtaposition (parallel composition) of two processes
The magmal structure gives rise to modal types. Consider the type of terms:
⟨⊙([], A)⟩B
This represents terms that, when placed into a context $\odot ([], x)$ where x : A, may
reduce to a term of type B.
| Calculus | Interaction $\odot$ | Modal Type | Interpretation |
|---|---|---|---|
| Lambda calculus | Application | A ⇒ B | Function type |
| Pi calculus | Parallel | ◇(A ▷ B) | Possibility modal |
| Pi calculus | Parallel | □(A ▷ B) | Necessity modal |
The "possibility" modal type ◇ corresponds to Caires' rely-guarantee type A ▷ B. If B can depend on x, these become dependent product types.
A finitely generated GSLT can be presented concisely using:
Generating sorts: A finite set including distinguished sorts P (processes) and R (rewrites) from the graph structure
Interaction: A choice of distinguished binary morphism:
⊙ : X × Y → P
for some pair of sorts X, Y
Generating morphisms: A finite set including:
Equations: A finite set of equations between morphisms
A rewrite constructor r : $\prod _{i} Z_{i} \to R$ whose codomain does not contain a factor of R
must factor through the interaction:
∃! f : ∏ᵢ Zᵢ → X × Y. ⊙ ∘ f = s ∘ r
This ensures that the source of any top-level rewrite is an application of the interaction operator.
We write:
r : A ~> B
as shorthand for the equations:
s(r(z₁, ..., zₙ)) = A
t(r(z₁, ..., zₙ)) = B
where A and B use the same free variables zᵢ.
Top-level rewrites: Codomain does not contain a factor of R
In-context rewrites: Codomain contains a factor of R
The simplest non-trivial Gph-theory:
Gph-Theory SKI:
Sorts: T (terms)
Constructors (vertices in Hom(1, T)):
S : 1 → T
K : 1 → T
I : 1 → T
Application (vertex in Hom(T × T, T)):
app : T × T → T
Notation: We write (M N) for app(M, N)
Reductions (edges):
σ : (((S x) y) z) ⇒ ((x z) (y z)) ; S-reduction
κ : ((K y) z) ⇒ y ; K-reduction
ι : (I z) ⇒ z ; I-reduction
The reductions $\sigma , \kappa , \iota$ are edges in the hom-graph Hom(T³, T), Hom(T², T), Hom(T, T)
respectively.
Here is a complete GSLT presentation for untyped lambda calculus with head normal form evaluation strategy:
GSLT Lambda_HNF:
Generating Sorts: (none beyond P, R)
Generating Morphisms:
; Graph structure (built-in)
s, t : R → P
; Term constructors
App : P × P → P ; Application
Lam : (P → P) → P ; Lambda abstraction (uses exponential)
; Rewrite constructors
Beta : (P → P) × P → R ; Top-level: beta reduction
Head : R × P → R ; In-context: reduction in head position
Interaction: App
Equations:
; Beta reduction (top-level)
Beta(A, B) : App(Lam(A), B) ~> ev(A, B)
; Head reduction (in-context)
Head(r, B) : App(s(r), B) ~> App(t(r), B)
Key observations:
Lambda abstraction uses the exponential P → P from the cartesian closed structure—this automatically handles variable binding
Beta reduction uses the evaluator ev : (P → P) × P → P from the cartesian
closed structure—this is function application in the internal logic
Head reduction is an in-context rule that propagates reductions through the application constructor, but only in head position (left of App)
The interaction is App, so the source of Beta factors through application
Lambda calculus can be embedded into SKI:
Translation [−]:
[x] = x
[M N] = ([M] [N])
[λx.M] = abstract(x, [M])
Where abstract is:
abstract(x, x) = I
abstract(x, M) = K M (if x ∉ FV(M))
abstract(x, M N) = S (abstract(x, M)) (abstract(x, N))
This eliminates bound variables, enabling the Gph-theory approach.
For MeTTa's multisets:
Gph-Theory MSet:
Sorts: T (terms), M (multisets)
Constructors:
empty : 1 → M
insert : T × M → M
Structural Equations (as parallel edges):
comm : insert(x, insert(y, m)) ⇔ insert(y, insert(x, m))
Note: ⇔ means edges in both directions (equivalence)
A simplified pi calculus as a Gph-theory:
Gph-Theory Pi_Core:
Sorts: P (processes), N (names)
Constructors:
0 : 1 → P ; Null process
par : P × P → P ; Parallel composition
input : N × (N → P) → P ; Input (with binding)
output: N × N → P ; Output
Interaction: par
Structural Equations:
par(0, P) = P ; Null identity
par(P, Q) = par(Q, P) ; Commutativity
par(par(P, Q), R) = par(P, par(Q, R)) ; Associativity
Reductions:
; Communication (top-level)
comm : par(output(x, v), input(x, F)) ~> ev(F, v)
; Parallel reduction (in-context)
parL : par(s(r), Q) ~> par(t(r), Q)
parR : par(P, s(r)) ~> par(P, t(r))
Section 6 of Stay & Meredith (2017) shows how to model:
Add a constructor R : T → T that marks the "active" position:
Constructors:
R : T → T ; Reduction context marker
Reduction Rules (consume R):
σ_R : (((S (R x)) y) z) ⇒ ((x z) (y z))
κ_R : ((K (R y)) z) ⇒ y
ι_R : (I (R z)) ⇒ z
The marker R is consumed during reduction—it acts as a linear resource.
For blockchain VMs, extend with a gas counter:
Sorts: T, G (gas)
Constructors:
zero : 1 → G
succ : G → G
gas : G × T → T ; Term with gas budget
Reductions (consume gas):
σ_g : gas(succ(g), (((S x) y) z)) ⇒ gas(g, ((x z) (y z)))
κ_g : gas(succ(g), ((K y) z)) ⇒ gas(g, y)
ι_g : gas(succ(g), (I z)) ⇒ gas(g, z)
stuck : gas(zero, M) ⇒ gas(zero, M) ; Out of gas (no progress)
Each reduction step consumes one unit of gas. When gas reaches zero, computation is stuck.
For more realistic resource modeling, different operations can have different costs:
Constructors:
sub : G × G → G ; Gas subtraction (saturating at zero)
Reductions (variable cost):
σ_g : gas(g, (((S x) y) z)) ⇒ gas(sub(g, 3), ((x z) (y z)))
κ_g : gas(g, ((K y) z)) ⇒ gas(sub(g, 2), y)
ι_g : gas(g, (I z)) ⇒ gas(sub(g, 1), z)
MeTTa's "effort objects" mentioned in Meta-MeTTa can be modeled this way:
state_with_effort : Term × KB × MSet × MSet × Effort → State
; Reductions consume effort
query_e : state_with_effort(p, k, w, o, succ(e))
⇒ state_with_effort(ε, k, w ∪ matches, o, e)
The paper provides a complete Gph-theory for RHO combinators, showing the approach works for real concurrent calculi.
Gph-Theory RHO:
Sorts: W (processes), N (names)
Constructors:
; Process constructors
0 : 1 → W ; Null process
(|) : W × W → W ; Parallel composition
drop : N → W ; Drop: ⌊x⌋
inp : N × (N → W) → W ; Input (combinator form)
out : N × W → W ; Output (lift)
; Name constructor
quote : W → N ; Quote: ⌈P⌉
Structural Equations:
(| 0) P = P ; Null identity
P | Q = Q | P ; Commutativity
(P | Q) | R = P | (Q | R) ; Associativity
In standard RHO calculus, input has a bound variable:
x(y).P ; y is bound in P
Using combinators, this becomes:
inp(x, λy.P) ; λ represented via SKI
The reflection mechanism $\lceil \lfloor x\rfloor\rceil \equiv _N x$ (quote-drop identity) ensures this encoding
is faithful.
Reductions:
; SKI reductions (for the combinator part)
σ, κ, ι : (standard SKI rules)
; Communication
ξ : out(x, Q) | inp(x, F) ⇒ F(quote(Q))
; Send Q on x, receive as quoted name
; Evaluation (drop-quote)
ε : drop(quote(P)) ⇒ P
; Evaluate a quoted process
The paper proves (Theorem 4):
The Gph-theory RHO preserves barbed bisimilarity: if $
P \approx Q$ in the standard RHO calculus, then $P \approx Q$ in the Gph-theory interpretation.
This validates that the combinator encoding faithfully represents the original calculus.
A key benefit of GSLTs is that they compile directly to Rholang, enabling optimal reduction via RSpace.
The general idea is to:
Interpreter = ∑ for(LHS_Pattern <- @0) {
@0!(RHS) | Interpreter
}
Where:
LHS and RHS mean left- and right-hand side\sum$ indicates mutually exclusive options (a disjunction)One problem: there may be unboundedly many patterns to match against. We don't want the interpreter term to be infinitely large.
Solution: Allow many internal reductions by the interpreter for each reduction by the original GSLT, and enumerate patterns lazily:
Interpreter = PatternGen(0)
PatternGen(n) = for(LHS_Pattern(n) <- @0) {
@0!(RHS(n)) | Interpreter
} + PatternGen(n+1)
A smarter enumeration uses the structure of the current state to prune patterns:
Interpreter = for(state <- @0) {
PatternGen'(0, state) | @1!(state)
}
PatternGen'(n, state) = for(LHS_Pattern'(n, state) <- @1) {
@0!(RHS(n)) | Interpreter
} + PatternGen'(n+1, state)
Here, LHS_Pattern'(n, state) uses the structure of state to enumerate only
those patterns that state might match—avoiding futile pattern match attempts.
The Rholang interpreter uses RSpace, a highly efficient data structure for:
GSLTs compiled to Rholang inherit these optimizations automatically.
For even higher performance, RSpace can be implemented on MORK (MeTTa Optimal Reduction Kernel), which provides:
See MORK/PathMap Integration for details.
Given an untyped GSLT, we can systematically generate a typed version using the hypercube functor. This is implemented in MeTTaIL Scala.
The basic idea:
From the untyped lambda calculus GSLT:
; Untyped
App : P × P → P
Lam : (P → P) → P
The hypercube functor generates:
; Typed (parametric)
App[A, B] : P[A → B] × P[A] → P[B]
Lam[A, B] : (P[A] → P[B]) → P[A → B]
The interaction operator $\odot$ gives rise to modal types. For lambda calculus:
⟨App([], A)⟩B ≈ A → B (arrow type)
For pi calculus:
⟨par([], A)⟩B ≈ ◇(A ▷ B) (possibility)
□(A ▷ B) (necessity)
The hypercube functor provides a mechanical procedure that approximates what OSLF does more generally:
| Hypercube Functor | OSLF |
|---|---|
| Lifts constructors to typed | Derives predicates on terms |
| Systematic parameter addition | Presheaf construction |
| Modal types from interaction | Behavioral modalities |
| Compile-time checking | Full behavioral reasoning |
For cases where the hypercube functor suffices, it provides a simpler path than full OSLF.
The key question is whether MeTTa's binding (pattern variables) can be eliminated via combinators or reflection.
Arguments for Gph-theories:
Arguments for full OSLF:
GSLT MeTTa_Core:
Generating Sorts: Term, Atom, List, MSet, KB
Generating Morphisms:
; Graph structure (built-in)
s, t : R → P
; Term constructors
atom : Atom → Term
list : List → Term
mset : MSet → Term
quote : Term → Term ; Quotation (reflection)
; List constructors
nil : 1 → List
cons : Term × List → List
; Multiset constructors
empty : 1 → MSet
insert : Term × MSet → MSet
; State constructor
state : Term × KB × MSet × MSet → State
; Rewrite constructors
Query : Term × KB → R ; Pattern matching
Output : MSet × MSet → R ; Move workspace to output
AddAtom : Term × KB → R ; Add to knowledge base
RemAtom : Term × KB → R ; Remove from knowledge base
Interaction: (state constructor, treating it as binary)
Structural Equations:
; Multiset commutativity
insert(x, insert(y, m)) = insert(y, insert(x, m))
Reductions:
; Query (simplified—actual unification more complex)
Query(p, k) : state(p, k, w, o) ~> state(ε, k, w ∪ matches(p, k), o)
; Output
Output(w, o) : state(out, k, w, o) ~> state(ε, k, ∅, o ∪ w)
; Add atom
AddAtom(t, k) : state((add t), k, w, o) ~> state(ε, k ∪ {t}, w, o)
; Remove atom
RemAtom(t, k) : state((rem t), k, w, o) ~> state(ε, k \ {t}, w, o)
; Quote-unquote (reflection)
Reflect : quote(unquote(t)) ~> t
The recommended path for MeTTa:
In the three-tier correction architecture:
| Tier | Component | GSLT Role |
|---|---|---|
| 1 | liblevenshtein | N/A (character-level) |
| 2 | MORK/PathMap | GSLT patterns for grammar |
| 3 | MeTTaIL/MeTTaTron | GSLT-based type checking |
The GSLT framework provides:
Provide:
Extend Gph-theories with:
| Approach | Use When |
|---|---|
| Basic Gph-theory | Simple combinatory systems (SKI) |
| GSLT | Full calculi with binding (lambda, pi) |
| GSLT + Hypercube | Need typed versions of untyped calculi |
| Full OSLF | Need behavioral predicates, bisimulation |
Can MeTTa's unification patterns be given a combinator representation?
MeTTa's reflective nature (quoting) suggests the simpler path is viable.
For defining new GSLTs, use this template:
GSLT <Name>:
Generating Sorts:
<list of sorts beyond P, R>
Generating Morphisms:
; Graph structure (built-in)
s, t : R → P
; Term constructors
<constructor> : <domain> → <codomain>
...
; Rewrite constructors
<rewrite> : <domain> → R
...
Interaction: <binary morphism on P>
Structural Equations:
<equation> = <equation>
...
Reductions:
; Top-level rewrites
<rewrite>(args) : <source> ~> <target>
; In-context rewrites
<rewrite>(r, args) : <source[s(r)]> ~> <source[t(r)]>
...
This template captures the essential information for a finitely generated GSLT and provides a standard format for documentation and implementation.
Can you improve this documentation?Edit on GitHub
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |