10 Advanced Topics
This section covers advanced features of Spindle.
10.1 Modal Operators
Spindle supports deontic modal operators for normative reasoning.
10.1.1 Obligation (must)
What agents are required to do:
; DFL: Use [O] prefix r1: employee => [O]attend_meetings ; SPL: Use must keyword (normally r1 employee (must attend-meetings))
10.1.2 Permission (may)
What agents are allowed to do:
; DFL r1: member => [P]access_library ; SPL (normally r1 member (may access-library))
10.1.3 Prohibition (forbidden)
What agents must not do:
; DFL: Use [F] or [O]¬ r1: visitor => [F]enter_restricted ; SPL (normally r1 visitor (forbidden enter-restricted))
10.2 Temporal Reasoning
Spindle supports temporal extensions for time-based reasoning.
10.2.1 Time Points
Associate literals with time points:
; SPL temporal literals (during valid_license t1 t2) (time event_occurred 2024-01-15)
10.2.2 Allen Interval Relations
Express relationships between time intervals:
before / after —
One interval precedes another meets —
End of one touches start of another overlaps —
Partial overlap contains —
One contains another starts / finishes —
Share start/end point equals —
Same interval
10.3 Trust-Aware Reasoning
Two-stage reasoning with trust evaluation.
10.3.1 Trust Rules
Define how trust is established:
; Trust propagation rules r1: verified_user => trust_level_high r2: new_user => trust_level_low ; Trust-dependent access r3: trust_level_high => can_access_sensitive r4: trust_level_low => ¬can_access_sensitive
10.3.2 Source Attribution
Track where conclusions come from:
--- dc:source: "security-policy-v2.pdf" prov:wasAttributedTo: "security-team" --- r1: admin => full_access
10.3.3 Weakest-Link Semantics
Trust propagates using weakest-link: the trust of a conclusion is the minimum trust of all rules in its derivation.
10.4 Abductive Reasoning
Find explanations for observations.
10.4.1 Forward Abduction
“What facts would make X true?”
(require spindle/query) (define result (requires theory (simple-literal "goal"))) (for ([solution (abduction-result-solutions result)]) (displayln (abduction-solution-facts solution)))
10.4.2 Defeater Analysis
The abduction system also identifies potential defeaters:
(define result (requires theory goal #:analyze-defeaters #t)) (abduction-result-potential-defeaters result)
10.5 Module System
Organize theories into reusable modules.
10.5.1 Basic Imports
@import "./base-facts.dfl" . |
@import "./policies/access.dfl" . |
10.5.2 Prefixed Imports
Avoid naming conflicts:
@import "./security.dfl" as sec . |
@import "./compliance.dfl" as comp . |
|
r1: sec:verified => comp:approved |
10.5.3 Import Semantics
The imported file is reasoned first
Its conclusions become facts in the importing file
Circular imports are detected and rejected
10.6 Performance Optimization
10.6.1 Theory Indexing
Build indexes for faster rule lookup:
(define indexed-theory (build-theory-index theory)) (reason indexed-theory)
10.6.2 Memoization
Spindle caches intermediate results. Clear if needed:
(clear-memoization-cache!)
10.6.3 Adaptive Iteration
The reasoner uses adaptive iteration with convergence detection, so no fixed iteration limits are needed.
10.7 Extending Spindle
10.7.1 Custom Literal Types
Extend the literal system for domain-specific needs:
(define lit (predicate-literal "owns" (list "alice" "book1")))
10.7.2 Custom Output Formats
The explanation system is extensible. See src/explanation.rkt for the output format implementations.
10.7.3 Integration
Spindle can be embedded in larger applications:
(require spindle spindle/query) (define (check-policy user action resource) (define theory (load-policy-theory)) (define request-lit (predicate-literal "request" (list user action resource))) (define theory+request (theory-add-rule theory (make-fact "req" request-lit))) (query theory+request (simple-literal "permitted")))