SHEAF (Simple Holographic Evaluation of Arboreal Fractals) is a dataflow language for tree logic. Its operands are parsimony trees — the simplest representation of a sentence that preserves its original meaning. Its operations are discrete algebraic transformations on those trees.
SHEAF programs are not Turing-complete — intentionally. Every program is a finite DAG (directed acyclic graph). Termination is guaranteed. Independent operations run in parallel automatically. There's no control flow, no loops, no recursion. Just data flowing through transformations.
Think of SHEAF as SQL for meaning: a declarative language where you describe what you want to compute over trees, and the runtime figures out how to execute it efficiently.
Every SHEAF statement has one shape:
binding = operation arg [arg...] [: option=value ...]
One statement per line. Bindings are immutable — write once, read many. Try the simplest possible program: parse a sentence into a tree.
The result is a parsimony tree: a nested structure where each node is a
sense-disambiguated word (cat_N_1.1, not just "cat") connected
by semantic roles (agent, location, etc.).
SHEAF has no type declarations. Types are inferred from operations. A binding is just a name for the result of an operation.
| Type | Produced By | Example |
|---|---|---|
Tree | parse, product, negate, blend... | A parsimony tree |
Node | node | A single element in a tree |
Text | literal "...", field | "hello" |
Int | literal, lex_distance | 42 |
Bool | subsumes, entails | true |
Map | unify, functor | Substitution map |
Path | prove, refute | Proof steps |
KB | kb_create, kb_load | Knowledge base |
Quale | quale, qualia | Pustejovsky quale |
List | contradictions, forward_chain | Collection |
The special binding _ discards the result. Used for side effects
like KB mutations. Multiple _ bindings on the same KB execute
sequentially in source order:
# _ discards the result, but the side effect (adding to KB) still happens _ = assert kb t1 _ = assert kb t2 # executes after the line above
parse is the gateway into SHEAF. It sends text to the parsimony parser
and returns a Tree. Multiple parses with no dependencies run in parallel.
negate toggles the NEG mark on the root predicate of a tree.
This flips the truth value: "The cat eats fish" becomes "The cat does not eat fish."
unify finds the substitution that makes two trees structurally identical.
It returns a Map showing what differs. If the trees can't be unified,
it fails with an error.
With : climb=true, unification can match words to their hypernyms
(more general terms). "cat" unifies with "animal" because cat is a animal.
entails checks whether one tree logically entails another, using
subsumption and hypernym climbing. It returns a Bool.
product computes the categorical conjunction of two trees —
merging their compatible parts. coproduct computes the categorical
disjunction — a tagged union.
normalize applies a named natural transformation to a tree.
Use "canonical" for canonical form, "active_to_passive",
or "passive_to_active" for voice transformations.
extract removes a subtree by role, replacing it with a quantified gap
("universal" or "existential").
node extracts a child node from a tree by its semantic role.
field reads a specific property from a node (like its lemma,
part of speech, or definition). These are local operations —
no network call needed.
A KB (knowledge base) is a named collection of trees that you can
reason over. Create one with kb_create, add trees with assert,
and remove them with retract.
assert can take either a tree binding or a raw string (which gets
parsed automatically).
prove finds the shortest derivation path from KB axioms to a target tree.
refute finds a path to the negation of the target. Both return a
Path — the chain of steps from axioms to conclusion.
Options: : timeout=5000 max_depth=10 to control the search.
contradictions scans a KB and returns all pairs of trees that
contradict each other. A contradiction occurs when one tree asserts P and
another asserts NOT(P) under the same scope.
forward_chain applies all implications in a KB up to a given depth,
deriving new facts. The result is a List of all newly derived trees.
functor finds a structure-preserving map between two trees —
revealing analogies and metaphors. It returns a Map showing how
nodes in one domain correspond to nodes in another.
The functor reveals the metaphor: company maps to lion, competitors map to gazelle. Uses Gemini for semantic reasoning.
quale determines which Pustejovsky quale a predicate activates on
its argument. qualia returns all four qualia for a lemma:
formal (what it is), constitutive (what it's made of),
telic (what it's for), and agentive (how it comes about).
"Enjoying" a book activates its telic quale (reading — what a book is for). "Burning" a book activates its constitutive quale (paper, pages — what it's made of). This is Pustejovsky's logical polysemy.
blend performs conceptual blending — combining two domains
into a new composite concept via dual functor composition. The result is a
new Tree that inherits structure from both inputs.
metonymy resolves a metonymic reference using quale traversal.
When we say "The White House issued a statement," we don't mean the building
literally issued a statement — we mean its occupant (the administration).
causal_chain traces telic quale edges from a source concept to a
target, following "is useful for" relationships. Each step follows one quale edge.
The chain traces: tree → lumber → construction → house. Each link follows the telic quale.
taxonomy returns the full taxonomic neighborhood of a lemma:
hypernyms (more general), hyponyms (more specific), meronyms (parts),
and holonyms (wholes).
lex_distance measures taxonomic distance between two lemmas —
how many edges apart they are in the hypernym/hyponym graph.
SHEAF includes inverse operations for backward search. These reverse the forward operations, enabling bidirectional reasoning:
| Operation | Inverse Of | Description |
|---|---|---|
instantiate | extract | Replace a VAR node with a filler |
factor | product | Remove a component from a product |
specialize | hypernym climb | Replace node with more specific node |
abduce_local | modus ponens | Extract antecedent from rule |
argument_strength evaluates how well a claim is supported vs. refuted
by a knowledge base. It returns both the proof path, the refutation path, and
a comparative verdict.
Trees are persisted and assigned UUID v7 identifiers. Use store to save
a tree, load to retrieve it later, and alias to give it
a human-readable name.
# Store a tree and name it t = parse "All men are mortal" id = store t _ = alias t "all-men-mortal" # Later, in another program: t = load "all-men-mortal" # Or by UUID: t = load 019503a1-4c2d-7000-8000-abcdef123456
UUIDs are time-ordered (v7) and globally unique. Same content produces the same content hash (SHA-256 dedup) regardless of UUID.
SHEAF programs are parsed by a finite state automaton into a dependency DAG. Statements with no shared dependencies run in parallel automatically.
# Program: a = parse "The cat eats fish" # Level 0 b = parse "The dog eats fish" # Level 0 (parallel with a) s = unify a b # Level 1 (waits for a and b) # Execution DAG: # Level 0: [a, b] ← parallel, no shared dependencies # Level 1: [s] ← waits for a and b
Every SHEAF program terminates — the DAG has no cycles. The runtime dispatches operations to serverless cloud functions, maximizing parallelism.
Options appear after : at the end of a statement. Key=value pairs
separated by whitespace.
# Options follow a colon s = unify a b : climb=true max_depth=5 proof = prove kb target : timeout=5000 max_depth=10 t = parse "The cat eats fish" : mod_level=2 # Values can be Text, Int, Float, or Bool s = unify a b : climb=true max_depth=5 quale_aware=true
The complete SHEAF grammar is regular — parseable by a finite state automaton in a single left-to-right scan. No recursion, no nesting.
PROGRAM → LINE*
LINE → COMMENT | STATEMENT | BLANK
COMMENT → '#' [^\n]*
STATEMENT → BINDING '=' OPERATION ARG* (':' OPTION*)?
BINDING → IDENT | '_'
OPERATION → KEYWORD
ARG → IDENT | STRING | INT | FLOAT | BOOL | UUID
OPTION → IDENT '=' VALUE
IDENT → [a-zA-Z_][a-zA-Z0-9_]*
STRING → '"' [^"]* '"'
INT → [0-9]+
FLOAT → [0-9]+ '.' [0-9]+
BOOL → 'true' | 'false'
UUID → [0-9a-f]{8}-[0-9a-f]{4}-7[0-9a-f]{3}-[89ab][0-9a-f]{3}-[0-9a-f]{12}
Complete reference of all 39 SHEAF operations.
| Operation | Args | Returns | Description |
|---|---|---|---|
parse | text | Tree | Parse text into a tree |
unify | tree tree | Map | Find substitution making trees identical |
subsumes | tree tree | Bool | Does first tree generalize second? |
product | tree tree | Tree | Categorical conjunction |
coproduct | tree tree | Tree | Categorical disjunction |
resolve | tree tree | Tree | Resolution on complementary nodes |
normalize | tree text | Tree | Apply named transformation |
extract | tree text text | Tree | Extract subtree, quantify the gap |
negate | tree | Tree | Toggle NEG mark |
entails | tree tree | Bool | Subsumption + hypernym climbing |
| Operation | Args | Returns | Description |
|---|---|---|---|
instantiate | tree text tree | Tree | Replace VAR with filler (inverse of extract) |
factor | tree tree | Tree | Remove component from product |
specialize | tree text tree | Tree | Replace with more specific node |
abduce_local | tree tree tree | Tree | Extract antecedent from rule |
| Operation | Args | Returns | Description |
|---|---|---|---|
node | tree text | Node | Extract child by role |
field | node text | Text | Read a field from a node |
| Operation | Args | Returns | Description |
|---|---|---|---|
kb_create | text | KB | Create a named KB |
kb_load | text | KB | Load existing KB |
kb_trees | kb | List | List all tree UUIDs |
assert | kb tree-or-text | — | Add tree to KB |
retract | kb tree-or-uuid | — | Remove tree from KB |
| Operation | Args | Returns | Description |
|---|---|---|---|
prove | kb tree | Path | Shortest path to target |
refute | kb tree | Path | Shortest path to negation |
contradictions | kb | List | All contradictory pairs |
abduce | kb tree | Tree | Minimal tree making target provable |
forward_chain | kb int | List | Apply implications to depth N |
argument_strength | kb tree | Result | Prove vs refute comparison |
reachability | kb tree | Result | Is target in deductive closure? |
| Operation | Args | Returns | LLM | Description |
|---|---|---|---|---|
functor | tree tree | Map | Gemini | Structure-preserving map (analogy) |
quale | tree | Quale | Gemini | Which Pustejovsky quale is activated? |
blend | tree tree | Tree | Gemini | Conceptual blending |
metonymy | tree text | Tree | Gemini | Resolve metonymic reference |
causal_chain | text text | Path | Gemini | Follow telic quale edges |
| Operation | Args | Returns | LLM | Description |
|---|---|---|---|---|
qualia | text | Quale | Grok | All four qualia for a lemma |
taxonomy | text | Taxonomy | Grok | Full taxonomic neighborhood |
lex_distance | text text | Int | Grok | Taxonomic distance |
| Operation | Args | Returns | Description |
|---|---|---|---|
load | text-or-uuid | Tree | Load stored tree |
store | tree | Text | Persist tree, returns UUID |
alias | tree text | — | Name a stored tree |