SPL Format Reference

SPL (Spindle Lisp) is the input language for Spindle. It replaces the earlier DFL syntax with a LISP-based DSL whose s-expression structure makes it straightforward to add new constructs (temporal operators, trust directives, claims blocks, etc.) without grammar ambiguity.

File Extension

.spl

Comments

Semicolon to end of line:

; This is a comment
(given bird)  ; Inline comment

Grammar Overview

theory      = statement*
statement   = fact | rule | prefer | meta | predicate-decl
            | claims | trusts | decays | threshold

; Core
fact        = "(given" literal ")"
rule        = "(" keyword label? body head ")"
keyword     = "always" | "normally" | "except"
prefer      = "(prefer" label+ ")"
meta        = "(meta" meta-target property* ")"
meta-target = label | predicate-target

; Predicate declarations (SPEC-024)
predicate-decl   = "(predicate" functor argument-list ")"
argument-list    = "(" argument-decl* ")"
argument-decl    = "(" arg-name primitive-sort ")"
primitive-sort   = "symbol" | "integer" | "decimal" | "float" | "number" | "any"
predicate-target = "(predicate" functor arity ")"
arity            = "0" | non-zero-digit digit*

; Trust
claims      = "(claims" source claims-meta* statement* ")"
claims-meta = ":at" atom | ":sig" atom | ":id" atom | ":note" atom
trusts      = "(trusts" source number ")"
decays      = "(decays" source decay-model number ")"
decay-model = "exponential" | "linear" | "step"
threshold   = "(threshold" name number ")"

; Temporal
time-expr   = "(moment" rfc3339-string ")" | integer | "inf" | "-inf"
during      = "(during" literal time-expr time-expr ")"

; Literals
literal     = atom | "(" atom arg* ")" | "(not" literal ")"
            | during | modal
modal       = "(" modal-op literal ")"
modal-op    = "must" | "may" | "forbidden"
body        = literal | "(and" body-elem+ ")"
body-elem   = literal | arith-constraint
atom        = identifier | variable
variable    = "?" identifier
source      = atom
number      = float in [0.0, 1.0]

; Arithmetic (body only)
arith-constraint = bind | compare
bind        = "(bind" variable arith-expr ")"
compare     = "(" cmp-op arith-expr arith-expr ")"
cmp-op      = "=" | "!=" | "<" | ">" | "<=" | ">="
arith-expr  = number | variable
            | "(" nary-op arith-expr+ ")"
            | "(" bin-op arith-expr arith-expr ")"
            | "(" unary-op arith-expr ")"
nary-op     = "+" | "-" | "*" | "/" | "min" | "max"
bin-op      = "div" | "rem" | "**"
unary-op    = "abs"

Facts

Simple Facts

(given bird)
(given penguin)
(given (not guilty))

Predicate Facts

(given (parent alice bob))
(given (employed alice acme))

Flat Predicate Syntax

(given parent alice bob)     ; Same as (given (parent alice bob))
(given employed alice acme)

Rules

Strict Rules (always)

(always penguins-are-birds penguin bird)
(always mortals-die (and human mortal) dies)

Defeasible Rules (normally)

(normally birds-fly bird flies)
(normally penguins-dont-fly penguin (not flies))

Defeaters (except)

(except broken-wing-blocks-flight broken-wing flies)

Unlabeled Rules

Labels are optional (auto-generated):

(normally bird flies)        ; Gets label like "r1"
(always penguin bird)        ; Gets label like "s1"

Literals

Simple

bird
flies
has-feathers

Negated

(not flies)
(not (parent alice bob))

Or with prefix:

~flies

Predicates with Arguments

(parent alice bob)
(employed ?x acme)
(ancestor ?x ?z)

Conjunction

Use and for multiple conditions:

(normally healthy-birds-fly (and bird healthy) flies)
(normally busy-students (and student employed) busy)

Why there is no or

Defeasible logic does not support disjunction in rule bodies. This is by design, not a missing feature — the proof theory (Nute/Billington/Antoniou) defines derivation over conjunctive rules only. Adding or would break the well-defined defeat and superiority semantics that make defeasible reasoning tractable.

Instead, express disjunction as separate rules that conclude the same head:

; "If rain or snow, take umbrella"
(normally rain-means-umbrella rain take-umbrella)
(normally snow-means-umbrella snow take-umbrella)

Each rule independently supports the same conclusion. If either rain or snow is provable, take-umbrella follows. This is the standard encoding of disjunctive conditions in defeasible logic, and it preserves per-rule defeat — you can override one path without affecting the other.

Variables

Variables start with ?:

(given (parent alice bob))
(given (parent bob charlie))

; Transitive closure
(normally parent-is-ancestor (parent ?x ?y) (ancestor ?x ?y))
(normally ancestor-chain (and (parent ?x ?y) (ancestor ?y ?z)) (ancestor ?x ?z))

Wildcard

Use _ to match anything:

(normally has-any-parent (parent _ ?y) (has-parent ?y))

Superiority

Two Rules

(prefer penguins-dont-fly birds-fly)

Chain

(prefer emergency-override safety-protocol standard-rule)

Expands to:

(prefer emergency-override safety-protocol)
(prefer safety-protocol standard-rule)

Predicate Declarations

A predicate declaration records the structure of a predicate — its ordered argument names and primitive sorts — independently of how (or whether) it is used. Declarations are optional: undeclared predicates parse and reason exactly as before. A declaration adds no fact or rule; it only populates the theory's vocabulary.

(predicate assign-to
  ((task  symbol)
   (agent symbol)))

(predicate emergency ())        ; zero-arity predicate emergency/0

The arity is derived from the number of argument declarations, so assign-to/2 above has two positions and emergency/0 has none.

Inline Metadata

A declaration may carry trailing meta properties inline, so you don't have to write a separate (meta (predicate ...) ...) statement for the common case:

(predicate assign-to
  ((task  symbol)
   (agent symbol))
  (description "Assign a task to an agent.")
  (tags ("planning" "scheduling")))

Inline properties are exact sugar for the separate metadata target — they land in the same predicate metadata store — so the declaration above is equivalent to writing the declaration and a (meta (predicate assign-to 2) ...) statement with the same properties. Inline and separate metadata for the same predicate merge (later values win per key).

Primitive Sorts

Each argument declares one primitive sort. Sorts describe the value space only; they carry no domain meaning and do not affect inference.

Declarations are validated when parsed: the argument names must be non-empty and unique, and an unknown sort is a parse error.

Predicate Indicators

For display and CLI interoperability, a predicate is written in Prolog-style functor/arity notation, e.g. assign-to/2 or emergency/0. A functor that contains / is quoted: "rate/limit"/2. This notation is presentation only — the machine representation always keeps functor and arity as separate structured fields, never a parsed string.

Metadata

Attach metadata to a rule (by label) or to a predicate (by structured target):

(meta birds-fly
  (description "Birds normally fly")
  (confidence 0.9)
  (source "ornithology-handbook"))

Properties

(meta rule-label
  (key "string value")
  (key2 ("list" "of" "values")))

Predicate Metadata Targets

A meta target may be a structured (predicate functor arity) selector instead of a label. This attaches metadata to one predicate symbol without overloading a rule label or parsing a predicate-indicator string:

(predicate assign-to ((task symbol) (agent symbol)))

(meta (predicate assign-to 2)
  (description "Assign a task to an agent."))

The predicate target is kept distinct from label metadata and from other arities: metadata for (predicate assign-to 2) never collides with a rule labelled assign-to, nor with assign-to/1. Predicate descriptions do not have to be declared — they can annotate any predicate the theory uses.

The Predicate Vocabulary

Declarations, predicate metadata, and observed rule usage together form a derived, read-only vocabulary: a catalogue keyed by predicate symbol that carries each predicate's signature, a description, observed argument kinds per position, and the rule occurrences that reference it. The vocabulary is a tooling projection — it never changes conclusions. See the Rust Library guide for the API (TheorySignature, Vocabulary).

Modal Operators

Obligation (must)

(normally contract-requires-payment signed-contract (must pay))

Permission (may)

(normally members-may-access member (may access))

Forbidden (forbidden)

(normally no-entry-unauthorized unauthorized (forbidden enter))

Temporal Reasoning

Time Points

Supported time formats:

(moment "2024-06-15T14:30:00Z")  ; RFC3339 / ISO 8601
1718461800000                    ; Epoch milliseconds
inf                              ; Positive infinity
-inf                             ; Negative infinity

Note: Multi-arity forms like (moment 2024 6 15) are reserved for future extensions.

During

(given (during bird 1 10))
(given (during (employed alice acme)
  (moment "2020-01-01T00:00:00Z")
  (moment "2023-01-01T00:00:00Z")))

Allen Relations

SPL status: Allen relations are implemented in the core Rust API but are not yet usable as SPL predicates. Exposing them requires interval variables (e.g., (during p ?t)), planned for a future release. The Allen during relation (interval containment) is distinct from the during SPL operator described above.

Allen's interval algebra defines exactly 13 mutually exclusive relations between two time intervals X and Y. Every pair of intervals satisfies exactly one.

Relation          X              Y           Inverse
─────────────────────────────────────────────────────────
before            ██████                     after
                              ██████

meets             ██████                     met-by
                        ██████

overlaps          ██████                     overlapped-by
                     ██████

starts            ████                       started-by
                  ██████████

during              ████                     contains
                  ██████████

finishes              ████                   finished-by
                  ██████████

equals            ██████████
                  ██████████                 (self-inverse)

Each relation has a strict inverse (reading the diagram with X and Y swapped), giving 6 symmetric pairs plus equals:

Arithmetic Expressions

Arithmetic expressions can appear in rule bodies as bind constraints, comparison guards, or as arguments to predicates.

Numeric Literals

42          ; Integer
3.14        ; Decimal (arbitrary precision)

Operators

(+ 1 2)           ; => 3
(* 2 3 4)         ; => 24
(- 10 3 2)        ; => 5 (left fold: 10-3-2)
(div 7 2)         ; => 3
(rem 7 2)         ; => 1
(** 2 10)         ; => 1024
(abs (- 3 10))    ; => 7
(min 5 3 8)       ; => 3

Bind Constraints

Bind a variable to the result of an arithmetic expression:

(normally compute-total
  (and (price ?p) (tax-rate ?r)
       (bind ?total (+ ?p (* ?p ?r))))
  (total ?total))

Comparison Guards

Compare two arithmetic expressions:

(normally adult-by-age
  (and (age ?x ?a) (> ?a 18))
  (adult ?x))

(normally failing-score
  (and (score ?x ?s) (<= ?s 50))
  (failing ?x))

Available operators: =, !=, <, >, <=, >=

Arithmetic in Predicate Arguments

Arithmetic expressions can appear as predicate arguments in rule bodies:

(normally compute-invoice
  (and (price ?item ?p) (tax-rate ?r))
  (invoice ?item (+ ?p (* ?p ?r))))

Type Promotion

Numeric types are promoted during arithmetic: Integer → Decimal → Float.

• Integer + Integer = Integer
• Integer + Decimal = Decimal
• Any + Float = Float
• div and rem require integer operands

Cross-type matching: Integer(2) matches Decimal(2.0) matches Float(2.0).

Reserved Keywords (REQ-008)

The following cannot be used as predicate names or rule labels:

+  -  *  /  div  rem  abs  min  max  **
bind  =  !=  <  >  <=  >=

Future reserved: sum, count, avg, round, floor, ceil

Restrictions

• Arithmetic constraints cannot appear in rule heads or facts (REQ-009)
• Arithmetic constraints cannot be negated with not or ~ (REQ-011)
• Temporal variables cannot be used as arithmetic operands (REQ-006)

Claims

The claims block attributes statements to a named source, with optional metadata.

(claims agent:alice
  :at "2024-06-15T12:00:00Z"
  :sig "abc123"
  :id "claim-001"
  :note "sensor reading"
  (given sunny)
  (normally no-umbrella-when-sunny sunny (not umbrella)))

Syntax

(claims source [:at timestamp] [:sig signature] [:id block-id] [:note annotation]
  statement ...)

• source — an atom identifying the claiming agent (e.g., agent:alice).
• :at — optional RFC3339 timestamp for when the claim was made.
• :sig — optional signature string for verification.
• :id — optional block identifier.
• :note — optional free-text annotation.

Statements inside a claims block are ordinary SPL expressions (given, always, normally, except, prefer) that automatically receive source metadata. See the Trust & Multi-Agent guide for details.

Complete Example

; The Penguin Example

; Predicate declaration + metadata (optional structural documentation)
(predicate flies ())
(meta (predicate flies 0) (description "Capable of flight."))

; Facts
(given bird)
(given penguin)

; Strict rule
(always penguins-are-birds penguin bird)

; Defeasible rules
(normally birds-fly bird flies)
(normally birds-have-feathers bird has-feathers)
(normally penguins-dont-fly penguin (not flies))
(normally penguins-swim penguin swims)

; Superiority — specificity
(prefer penguins-dont-fly birds-fly)

; Defeater
(except broken-wing-blocks-flight broken-wing flies)

; Metadata
(meta birds-fly (description "Birds typically fly"))
(meta penguins-dont-fly (description "Penguins are an exception"))