What is SHEAF?

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.

Your First Program

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.).

Bindings & Types

SHEAF has no type declarations. Types are inferred from operations. A binding is just a name for the result of an operation.

TypeProduced ByExample
Treeparse, product, negate, blend...A parsimony tree
NodenodeA single element in a tree
Textliteral "...", field"hello"
Intliteral, lex_distance42
Boolsubsumes, entailstrue
Mapunify, functorSubstitution map
Pathprove, refuteProof steps
KBkb_create, kb_loadKnowledge base
Qualequale, qualiaPustejovsky quale
Listcontradictions, forward_chainCollection

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

Parsing

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.

Negation

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."

Unification

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.

Entailment

entails checks whether one tree logically entails another, using subsumption and hypernym climbing. It returns a Bool.

Product & Coproduct

product computes the categorical conjunction of two trees — merging their compatible parts. coproduct computes the categorical disjunction — a tagged union.

Normalize & Extract

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 & Field

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.

Creating a Knowledge Base

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).

Proving & Refuting

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

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 Chaining

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 (Analogy)

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 & Qualia

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

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

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

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

taxonomy returns the full taxonomic neighborhood of a lemma: hypernyms (more general), hyponyms (more specific), meronyms (parts), and holonyms (wholes).

Lexical Distance

lex_distance measures taxonomic distance between two lemmas — how many edges apart they are in the hypernym/hyponym graph.

Inverse Operations

SHEAF includes inverse operations for backward search. These reverse the forward operations, enabling bidirectional reasoning:

OperationInverse OfDescription
instantiateextractReplace a VAR node with a filler
factorproductRemove a component from a product
specializehypernym climbReplace node with more specific node
abduce_localmodus ponensExtract antecedent from rule

Argument Strength

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.

Storage & UUIDs

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.

Execution Model

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

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

Grammar

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}

All Operations

Complete reference of all 39 SHEAF operations.

Core Tree Operations

OperationArgsReturnsDescription
parsetextTreeParse text into a tree
unifytree treeMapFind substitution making trees identical
subsumestree treeBoolDoes first tree generalize second?
producttree treeTreeCategorical conjunction
coproducttree treeTreeCategorical disjunction
resolvetree treeTreeResolution on complementary nodes
normalizetree textTreeApply named transformation
extracttree text textTreeExtract subtree, quantify the gap
negatetreeTreeToggle NEG mark
entailstree treeBoolSubsumption + hypernym climbing

Inverse Operations

OperationArgsReturnsDescription
instantiatetree text treeTreeReplace VAR with filler (inverse of extract)
factortree treeTreeRemove component from product
specializetree text treeTreeReplace with more specific node
abduce_localtree tree treeTreeExtract antecedent from rule

Node Access

OperationArgsReturnsDescription
nodetree textNodeExtract child by role
fieldnode textTextRead a field from a node

Knowledge Base

OperationArgsReturnsDescription
kb_createtextKBCreate a named KB
kb_loadtextKBLoad existing KB
kb_treeskbListList all tree UUIDs
assertkb tree-or-textAdd tree to KB
retractkb tree-or-uuidRemove tree from KB

Inference

OperationArgsReturnsDescription
provekb treePathShortest path to target
refutekb treePathShortest path to negation
contradictionskbListAll contradictory pairs
abducekb treeTreeMinimal tree making target provable
forward_chainkb intListApply implications to depth N
argument_strengthkb treeResultProve vs refute comparison
reachabilitykb treeResultIs target in deductive closure?

Semantic Operations

OperationArgsReturnsLLMDescription
functortree treeMapGeminiStructure-preserving map (analogy)
qualetreeQualeGeminiWhich Pustejovsky quale is activated?
blendtree treeTreeGeminiConceptual blending
metonymytree textTreeGeminiResolve metonymic reference
causal_chaintext textPathGeminiFollow telic quale edges

Lexicon

OperationArgsReturnsLLMDescription
qualiatextQualeGrokAll four qualia for a lemma
taxonomytextTaxonomyGrokFull taxonomic neighborhood
lex_distancetext textIntGrokTaxonomic distance

Storage

OperationArgsReturnsDescription
loadtext-or-uuidTreeLoad stored tree
storetreeTextPersist tree, returns UUID
aliastree textName a stored tree