Dedalus

Temporal Datalog variant (Alvaro, Marczak, Conway, Hellerstein, Maier) designed as a formal model of state and time in distributed computation. Tuples carry a logical timestamp; rules are partitioned into deductive (same-time), inductive (next-time), and asynchronous (non-deterministic-time). Dedalus is the logical basis of Bloom Language and the substrate on which the CALM Theorem is proved for programmable systems.

In this vault

Backlinks

Bloom Language line 10
Relational Transducer line 11
CALM Theorem line 25
Keeping CALM - When Distributed Consistency is Easy line 41
Keeping CALM - When Distributed Consistency is Easy line 28
Keeping CALM - When Distributed Consistency is Easy line 10

Linked Pages

Relational Transducer

Ameloot-Neven-Van den Bussche formalisation of a distributed program node: a relational event-loop server that, on each tick, (1) ingests an unordered batch of insert/delete requests into local relations, (2) queries the updated relations (a monotonic relational query: selection, projection, join, union, transitive closure), and (3) sends results as messages to other machines and outputs.

A relational transducer network distributes data across machines of this shape. The CALM Theorem is proved over this model: a query has a coordination-free evaluation plan on such a network iff the query is monotone.

In this vault

Foundations of Logic Programming - Lloyd

Foundations of Logic Programming (Chapter 1: Preliminaries)

Reference: J. W. Lloyd (1987). Springer-Verlag, Second Extended Edition. Source file: 2022-08-18 13-38-01-Lloyd.pdf. URL

Summary

The opening chapter of Lloyd’s canonical textbook on the mathematical foundations of logic programming. It introduces first-order theories, syntax (alphabets, terms, well-formed formulas, clauses, Horn clauses), interpretations and models, and Herbrand semantics as the preferred route for reasoning about logical consequence of a program.

Lloyd motivates logic programming as Kowalski’s insight that “algorithm = logic + control”: a definite program is a set of Horn clauses (the logic), and the inference strategy (SLD-resolution, search order) is the control. He distinguishes “system” languages (committed-choice, concurrent) from “application” languages (PROLOG-style), and sets up the semantic machinery — Herbrand interpretations, models, logical consequence, unsatisfiability — needed for the rest of the book.

Key Ideas

Algorithm = Logic + Control (Kowalski’s principle)
Horn clauses as the executable fragment of first-order logic
Herbrand universe and base; Herbrand interpretations suffice for clause sets
Definite programs vs normal programs (negation)
SLD-resolution as refutation procedure (developed in later chapters)

Connections

Conceptual Contribution

Claim: Logic — specifically first-order Horn-clause logic with SLD-resolution — can serve as a programming language, where a program is a set of definite clauses, a computation is resolution refutation, and the declarative semantics (Herbrand models, least fixpoint) coincides with the procedural semantics.
Mechanism: Rigorously build up first-order theories, interpretations, Herbrand interpretations/bases, unification, and the T_P fixpoint operator; prove soundness and completeness of SLD-resolution; develop negation-as-failure, the Closed World Assumption, and semantics of normal programs; treat Prolog as the canonical realisation of the Kowalski slogan “algorithm = logic + control”.
Concepts introduced/used: Logic Programming, Horn Clauses, SLD Resolution, Herbrand Universe, Unification, Negation as Failure, Fixpoint Semantics, Prolog, Closed World Assumption, First-Order Logic, Algorithm = Logic + Control
Stance: formal / foundational textbook
Relates to: Theoretical substrate for Agent-Oriented Programming, ACRE Agent Conversation Reasoning Engine, and Ensuring Trustworthy and Ethical Behaviour in Intelligent Logical Agents (all of which assume BDI agents implemented in logic-programming languages). The mentalistic-semantics side of ACLs (KQML as an Agent Communication Language, FIPA-ACL) presupposes Lloyd-style logical machinery.

In this vault

CALM Theorem

Consistency As Logical Monotonicity (Hellerstein 2010 conjecture; Ameloot, Neven, Van den Bussche 2013 proof). A distributed program has a consistent, coordination-free implementation if and only if it is expressible in monotonic logic.

Monotonic programs produce a set of outputs that only grows as inputs arrive (S ⊆ T ⟹ P(S) ⊆ P(T)). Such programs are safe under missing information: any conclusion reached on a subset of inputs remains valid when more arrive. Non-monotonic programs may retract earlier conclusions, so they must wait for “all the news” — which is what distributed coordination enforces.

CALM is the positive counterpart to the CAP Theorem: it names the exact class of programs that can satisfy Consistency, Availability, and Partition-tolerance simultaneously.

Why it matters

Moves consistency from a property of storage (linearizability, serializability) to a property of programs — Confluence.
Tells programmers what kinds of features are free (monotonic: set union, counting up, set-containment) and what must be paid for (non-monotonic: set difference, strict aggregation, count-exact, deletions without tombstones).
Gives a design rule for coordination-free systems: build from monotonic primitives — CRDTs, Immutable Data Structures, Tombstones, monotonic accumulators — and only add coordination at non-monotonic boundaries.

Formal statement

Using Relational Transducer networks as the execution model and Confluence as the consistency criterion, Ameloot et al. prove: a query Q has a coordination-free distributed evaluation plan iff Q is monotone.

In this vault

Keeping CALM - When Distributed Consistency is Easy — the definitive survey
CAP Theorem
Confluence
Monotonic Logic
Coordination Avoidance
Relational Transducer
Bloom Language
Dedalus
CRDTs
Non-monotonic Reasoning

Keeping CALM - When Distributed Consistency is Easy

Keeping CALM: When Distributed Consistency is Easy

Reference: Joseph M. Hellerstein & Peter Alvaro (2019). arXiv:1901.01930v2. Source file: ../1901.01930v2.pdf (in parent directory). URL

Summary

An accessible, updated statement of the CALM Theorem — Consistency As Logical Monotonicity: a program has a consistent, coordination-free distributed implementation if and only if it is monotonic in a formal logical sense. Monotonic programs are “safe” under missing information and can proceed without waiting: once something has been concluded, it stays concluded. Non-monotonic programs (“change their mind” in the face of new inputs) are necessarily order-sensitive and therefore require coordination to produce a single deterministic outcome.

CALM is a positive counterpart to the negative results of the CAP Theorem and the FLP impossibility. Where CAP says “you can’t always have it all”, CALM delineates the class of programs that can in fact satisfy all of C, A, and P simultaneously: exactly the monotonic ones. The theorem shifts attention away from storage consistency (linearizability, serializability) toward program consistency — Confluence: deterministic outcomes despite non-deterministic message delivery and ordering.

The paper traces the theorem’s implications for Bloom Language, Dedalus, CRDTs, coordination-free design patterns (monotonic accumulation, tombstones, immutable data), distributed garbage collection, and Amazon’s shopping-cart example. It closes with open questions: expressiveness of monotonic languages, program synthesis targeting monotonicity, repair of non-monotonic code, and a possible Stochastic CALM for near-optimum stochastic algorithms.

Key Ideas

Monotonicity ⇔ coordination-freeness ⇔ consistency (CALM)
Program consistency = confluence: same outputs regardless of message order / batching
Non-monotonic operations retract earlier conclusions, hence must wait for “all the news” — requiring Coordination Avoidance logic to know when
Formalisation via Relational Transducer networks (Ameloot, Neven, Van den Bussche)
CAP is a special case: linearizable storage is one non-monotonic operation; CALM asks the question across all programs
Practical playbook: immutable data structures, tombstones, set-monotonic accumulation, CRDTs as object-oriented monotonic types
Bloom gives syntactic monotonicity checking — a programmer writing monotonic Bloom is guaranteed coordination-free correctness

Connections

Conceptual Contribution

Claim: A distributed program is consistent and coordination-free iff it is expressible in monotonic logic — a tight, provable characterisation that converts “distributed consistency is hard” into a precise question about a program’s logical shape.
Mechanism: Formalise programs as networks of Relational Transducers (Ameloot et al.); define Confluence as program-level determinism under non-deterministic delivery; prove biconditional between confluence and monotonic-logic expressibility.
Concepts introduced/used: Monotonic Logic, Confluence, Coordination Avoidance, Relational Transducer, Bloom Language, Dedalus, CRDTs, CAP Theorem, Immutable Data Structures, Tombstones, Stochastic CALM
Stance: foundational / survey
Relates to: Provides the theoretical companion to the Gossip Protocols cluster (Gossip-Based Computation of Aggregate Information, Gossip-based Aggregation in Large Dynamic Networks) — gossip aggregation with mass conservation is exactly a monotonic accumulation, hence coordination-free. Frames why Extensible Distributed Coordination must reach for stored-procedure coordination precisely where programs are non-monotonic. Contrasts with Are Multiagent Systems Resilient to Communication Failures: that paper shows game-theoretic MAS are brittle under message loss — CALM identifies the logical class of programs immune to such loss. The monotonic/non-monotonic split echoes Foundations of Logic Programming - Lloyd’s distinction between Horn-clause logic and Negation as Failure.