1 Before anything else

1.1 Who this is for

This note is written for someone who ships software. It assumes fluency with SQL, comfort with at least one of LINQ, XQuery, list comprehensions or a collection pipeline API, and the ordinary working knowledge of concurrency that comes from having debugged it. It assumes no category theory, no process algebra, and no prior contact with the rho calculus.

There is a companion document, Graph-Structured Lambda Theories: A Reference for the Working Developer [30], which covers overlapping ground for a reader who wants the theory first and is willing to spend a chapter on bisimulation to get it. This note is the other entrance to the same building. A reader who finishes here and wants proofs will find them there; a reader who starts there and wants to write code will find that here. Neither is a prerequisite for the other.

1.2 Why the order is backwards

The convention is to teach a language’s data definition language first — here are the types, here is how to make values — and its control flow language second. The convention is defensible and this note ignores it.

The reason is that the control flow language of f1r3|@ng has a familiar door and the data definition language does not. Every working developer has written a query comprehension. Walking through that door and following the shape until it breaks generates, in order, exactly the questions the data definition language answers. Taught the other way round, the Theory block looks like an unusually elaborate schema declaration and its point is invisible.

So the order here is: the comprehension; what a comprehension cannot do; what f1r3|@ng adds; what that addition forces us to have; and then, twice, what happens when we widen the thing that was added.

1.3 The running example

One example runs from beginning to end. A forager moves through an environment of specimens. Some specimens are rich and worth the cost of opening; some are decoys and are not. The forager has a cheap structural test it can apply, and that test is evidence rather than proof. It has a finite budget, it spends from that budget to look and to open, and if the budget reaches zero the forager stops — permanently.

The example is drawn from a research programme on learning as computation, in which such a forager is a very small instance of a mortal scientist [38]: a computation that forms hypotheses about its environment, pays to test them, and is punished by the environment when they are wrong. The point of choosing it is not the biology. It is that the same four lines of code are legible at every stage of this note — as a query, as a transaction, as a hypothesis, and finally as a learning rule — and that the numbers quoted in the last part were measured by running it.

1.4 Notation, and three conventions worth flagging

The language is f1r3|@ng, and it has two halves. Its control flow sublanguage — CFL for short — is the part that makes things happen: sends, receipts, the comprehension of §2. Its data definition sublanguage — DDL — is the part that says what there is: the Module and Theory declarations of §3. Both acronyms are older than either language and are used here in their ordinary sense. Neither half has a separate name. There is one language.

f1r3|@ng inherits a good part of its CFL from rholang, and this note names the debt where it is useful — the sends and receipts of §2 will be familiar to anyone who has written rholang, and the translation table of §2.5 would read much the same for either. The inheritance is not an equivalence, and it is worth being precise about where it stops. The where clause of §5 answers with a value rather than a verdict, and a program whose guards return values is not a program with better guards — it is a different kind of object, a simulation of a population rather than a transition of a state. That single change puts f1r3|@ng somewhere rholang does not reach, and most of the second half of this note is an account of where.

The calculus underneath both is the rho calculus [46]. The name abbreviates reflective higher order calculus, and dropping the periods gives the transliteration of the Greek letter after $\pi$ — a joke about what comes after the $\pi$-calculus. It is written “rho calculus”, never with the Greek letter.

Quotation is written @P: the name that stands for the process P. Dereference, sometimes called dropping or unquoting, is written *x: the process that the name x stands for. These are inverse in one direction on the nose — @*x is x — and that fact does more work later than it looks like it should.

Code listings in this note come from two places, and it is worth knowing which is which. Listings labelled as running examples are taken verbatim from the f1r3node-rust repository [49, 50], where they compile and are covered by tests. Listings that illustrate a design under development are marked as such. Nothing here silently pretends that a plan is a product; §3.13 is a table of what actually runs.

2 The control flow language

2.1 The forager, as a query

Start with the forager’s problem, stated the way a developer would state it first. There is a table of specimens. There is a cheap test, $\chi$. The question is which specimens pass the test.

SELECT   spec
FROM     prey
WHERE    chi(spec)

Three clauses. FROM says where the data lives. WHERE says which of it we want. SELECT says what shape to hand back. The shape is so useful that it has been reinvented in every decade since it was introduced [6, 5].

The four descendants are LINQ [14], XQuery’s FLWOR [26], and the list comprehension in the form Wadler gave it [24]. The persistence of the shape across five languages with nothing else in common is the fact worth taking seriously. It is not a syntax fashion. The comprehension is what data access looks like when you write down honestly what you are doing: naming a source, filtering it, and projecting the survivors.

2.2 What LINQ was actually for

There is a step in this history that is usually told as a story about convenience and is better told as a story about expressiveness.

SQL is a complete language for asking. It is not a language for acting. A query returns a result set to someone else — an application, in another language, which then does whatever is to be done. The boundary between the two is where the impedance mismatch lives, and every ORM ever written is an attempt to plaster over it.

LINQ exists for precisely this reason: it embeds the query comprehension into a host language, so that a developer can at last express the DO. That is the whole point. Once from-where-select is a first-class expression of C# or F#, the result of a query is an ordinary value in a language that can act on it, and the mismatch is gone — for reads. XQuery’s FLWOR has the same ambition inside XML, and the same limit; XQuery Update [27] was bolted on afterwards precisely because the return clause cannot cause anything.

f1r3|@ng takes the desideratum LINQ identified and goes the rest of the way. Rather than embedding the comprehension in a host language, it builds the language around the comprehension. The comprehension is not a query expression that yields a value; it is the sole way anything happens at all.

2.3 SELECT-FROM-WHERE-DO

Here is the forager’s query again, in f1r3|@ng.

for( @spec <- prey where Chi(spec) ) {
  Break!(spec)
}

Clause by clause, against the SQL:

Two of those rows deserve more than a line.

2.3.0.1 The pattern is the projection, and it is stronger than one.

A SELECT list picks columns. A f1r3|@ng pattern matches structure: it can destructure nested terms, bind sub-terms to variables, and — as §3 explains — it matches up to the equations of the theory that types the channel, so two spellings of the same value match the same pattern without the developer arranging it. A pattern is a projection in the same sense that a regular expression is a substring test.

2.3.0.2 The DO is a process, not a value.

The continuation { Break!(spec) } is not returned to a caller. It runs. It may send on channels, spawn further comprehensions, or do nothing. There is no host language to hand results back to, because there is no outside.

2.4 The other half: the write

A query language has one privileged verb. f1r3|@ng has two, and the second is the reason the first behaves differently than it does in SQL:

prey!( spec )

That is the write. It is a term, it composes in parallel with everything else using |, and — this is the part with consequences — it is addressed the same way the read is. The reader names prey; the writer names prey; neither names the other.

Being explicit about both halves is what distinguishes this from a query language with side effects bolted on. In SQL, INSERT and SELECT are different kinds of statement, mediated by an engine that owns the table. Here they are two terms in one program, and the table is not owned by anybody.

2.5 The translation table

The following is probably the most useful page of this note for a reader coming from SQL. f1r3|@ng distinguishes three ways of reading — inheriting the distinction, and the notation, from rholang — and it is exactly the distinction a database developer already makes between a destructive read, a standing query, and a plain look.

The three arrows are worth committing to memory, because choosing among them is the main design decision in a f1r3|@ng program and the choice is invisible in the SQL vocabulary that motivates it. A linear receipt <- is the default. It consumes. Persistence <= and peeking <<- are the deviations, and each gives something up: a persistent receipt gives up the guarantee that a datum is handled once; a peek gives up the guarantee that reading it means nobody else will.

2.6 Joins, groups, and where the where goes

The full form of the comprehension is a sequence of groups, and each group is a set of receipts that must occur together:

for( ptrn_11 <- chan_11 & ... & ptrn_1n <- chan_1n  where cond_1 ;
     ...                                                         ;
     ptrn_k1 <- chan_k1 & ... & ptrn_km <- chan_km  where cond_k ) P

Inside a group, & means simultaneity: all of those receipts happen at once or none of them do. Between groups, ; means sequence. Each group carries its own where, and cond_j may mention any variable bound by a pattern in group $i$ for $i \leq j$ — so the guard on a later group can test what an earlier group received. The comprehension commits only when every pattern matches and every condition holds.

A SQL developer will recognise & as a join and should immediately notice the difference. A SQL join is over static extents: the rows are all already there, and the join is a computation over them. A f1r3|@ng join is over concurrent writers: the rows are being produced by other running programs, and the join is a rendezvous. It succeeds when a matching datum is available on every joined channel at once, and until then it waits.

2.7 The witnessed transaction

Now the payoff for having made both halves explicit.

When a reader and a writer meet on a channel, one rule fires. In the f1r3|@ng presentation of the calculus [48] it is written like this — and this is a real excerpt from a language definition, not pseudocode:

(PPar {(PInput n ^x.p), (POutput n q), ...rest})
    ~> (PPar {(subst ^x.p (NQuote q)), ...rest});

In words: a parallel composition containing a receipt on n and a send on n rewrites to the same composition with both of them replaced by the receipt’s body, with the sent term substituted for the bound variable. Everything else, ...rest, is untouched.

The substitution is the point. After the step, the running term contains the evidence that this reader met this writer over this datum: the datum is sitting in the continuation, in the position the pattern named. Nothing external recorded the event. The event left a mark on the program.

This is not a subtle argument, and the implementation makes it concrete. The comment at the head of the shipped example [49] says it plainly: a failing guard leaves the message in the tuple space, exactly as a non-matching pattern does. A failed transaction is not rolled back; it never began.

// Receive-side `where` guard: only commit when both the spatial pattern
// matches AND the guard evaluates to true. Failing the guard leaves the
// message in the tuple space -- same as a non-matching pattern.
new chan, stdout(`rho:io:stdout`) in {
    chan!(-3) |
    chan!(0)  |
    chan!(7)  |
    for (@x <- chan where x > 0) {
        stdout!(("kept", x))
    }
}

Three consequences a developer will care about.

2.7.0.1 Multi-party commit is a language construct.

A join & across $m$ channels is one transaction over $m$ resources. It either takes a datum from each or takes none. The protocol machinery that would normally implement this — prepare, vote, commit, the coordinator, the timeout — is not written, because the rule that fires is the multi-channel one.

2.7.0.2 The witness is where cost attaches.

Because there is an identified event, there is something to charge for. This is what makes the metering of §3.12 possible without instrumenting an interpreter: the unit of billing is the same unit as the unit of commitment.

2.7.0.3 Candidates.

For a join across several channels with several available data, there may be more than one way to assign data to patterns. Each such assignment is a candidate. Ordinarily one of them happens and the others do not, and a developer never thinks about it. Keep the word anyway: candidates are the thread that runs through the rest of this note. In §4 a condition is evaluated per candidate; in §5 a candidate carries a weight rather than a verdict, and everything interesting follows from that.

2.8 The forager, in full

Enough machinery is now on the table to write the running example properly. The forager has a belief, held as data on a channel. It races two courses of action: open the specimen, or ignore it and graze a low-yield but safe alternative.

new bel, prey, wall in {
  bel!( (1, 0.5) ) |                    // (n, s): one unit of prior evidence

  // the two branches race for the belief and the specimen
  for( @(n,s) <- bel ; @spec <- prey  where  Chi(spec) ) {
    Break!(spec) | bel!( revise(n, s, spec) )
  } |
  for( @(n,s) <- bel ; @spec <- prey  where  g ) {
    Graze!(*wall) | bel!( (n, s) )
  }
}

Read it as a developer. Two comprehensions compete for the same two resources: the belief and the next specimen. Whichever fires consumes both, does its work, and puts an updated belief back. Because the belief is consumed, the two branches cannot both act on the same specimen — mutual exclusion is not arranged, it is what a linear receipt means.

Three questions are now unavoidable, and they are the agenda for the rest of this note.

1. Chi(spec) is a condition about the structure of a specimen. Where does the vocabulary for saying that come from? (§3.)

2. What else could a condition say, beyond structure — and what does saying more cost? (§4.)

3. g in the second branch is not a Boolean. It is a number. What is a numeric where clause, and what does a program mean when its conditions stop answering yes or no? (§5.)

3 Where the pattern and the condition come from

3.1 The question the comprehension cannot answer

The comprehension of §2 presupposes two things it does not supply. Its pattern @spec must have a grammar of terms to match against. Its condition Chi(spec) is a claim about structure, so there must be a notion of what structure a specimen has.

In SQL both come from the schema. spec is a row of a known table with known column types, and chi is a predicate over those columns. The schema is the data definition language, and the query language leans on it entirely.

f1r3|@ng’s schema is the Theory declaration, and the reason to keep reading is that it is a great deal more than a schema.

3.2 A Theory declaration, whole

Here is one, complete [50]. It defines the rho calculus [46] itself — which is a useful thing to see early, because it shows that the calculus f1r3|@ng is built on is not privileged: it is one language definition among others, written in the same form a developer would use for an invoice format.

Theory RhoCalc() {
    Types {
        Proc;
        Name;
    }
    Terms {
        PZero  . |- "0" : Proc;
        PDrop  . n:Name |- "*" "(" n ")" : Proc;
        POutput. n:Name, q:Proc |- n "!" "(" q ")" : Proc;
        PInput . n:Name, ^x.p:[Name -> Proc] |- n "?" x "." "{" p "}" : Proc;
        PPar   . ps:HashBag(Proc) |- "{" ps.*sep("|") "}" : Proc;
        NQuote . p:Proc |- "@" "(" p ")" : Name;
    }
    Equations {
        (NQuote (PDrop N)) == N;
    }
    Rewrites {
        RComm : (PPar {(PInput n ^x.p), (POutput n q), ...rest})
                  ~> (PPar {(subst ^x.p (NQuote q)), ...rest});
        RDrop : (PDrop (NQuote P)) ~> P;
        RPar  : if S ~> T then (PPar {S, ...rest}) ~> (PPar {T, ...rest});
    }
}

Four blocks. Types names the syntactic categories. Terms gives one constructor per line: a label, then the arguments it takes with their sorts, then — after the turnstile — the concrete syntax written in terms of those argument names, then the category it produces. So the grammar and the pretty-printer come from the same declaration. Equations says which distinct terms are to be regarded as the same. Rewrites says how terms move — in the style Plotkin introduced for operational semantics [16] and Milner used to such effect for processes [15].

From that block, the toolchain generates the abstract syntax types, a parser and a bidirectional printer, capture-avoiding substitution that respects binding, and a rewrite engine.

Three details in the Terms block repay a second look, because each is carrying weight a conventional schema language has no way to carry. ^x.p:[Name -> Proc] declares that PInput’s second argument is an abstraction: x binds in p. Binding is part of the data declaration, which is why substitution can be generated rather than hand-written. ps:HashBag(Proc) declares that PPar takes an unordered collection with multiplicity, and ps.*sep("|") says how to render one. And in RComm, ...rest binds whatever else was in the bag and puts it back — which is what lets a rule fire on two participants inside an arbitrary parallel composition without saying anything about the others.

3.3 The four rungs

The blocks form a ladder, and where a given language definition stops on that ladder determines what kind of thing it is.

An ordinary data definition language stops on the first rung. Records, sums, products, lists, maps: that is the whole of what most type systems can say about data, and it is a lot. The second and third rungs are where this differs, and the second rung is the one that will surprise a working developer most, so take it first. The fourth is the subject of §3.6–§3.7, and answers the question every developer asks on seeing the declaration above: can I reuse part of one of these?

3.4 Rung two: equations, or the comment your type system cannot read

Every codebase of any size contains comments of this form:

This is a list, but order doesn’t matter — always compare as a set.
This is a string, but compare case-insensitively.
Addresses with an empty line-2 are equal to the same address without it.

Each is an equation. Each is being maintained by hand, in prose, because the type system cannot express it. The consequences are familiar: a hand-written equals, a normalisation function called on the way in and forgotten in one code path, a cache keyed by the wrong representative, and a class of bug that only appears when two spellings of the same value meet.

An equations block moves that comment into the definition:

Equations {
    (NQuote (PDrop N)) == N;
}

The payoff is not that the compiler now checks something. It is that pattern matching happens up to the equations. When the comprehension of §2 matches @spec against a datum, it matches modulo the theory that types the channel. A developer never writes normalisation, never chooses a canonical form, and never has the bug where one code path forgot.

This is why the PPar constructor above takes a HashBag rather than a list: parallel composition is associative and commutative, and rather than being a special case hard-wired into an interpreter, that is a property of the data declaration. The same mechanism is available for an invoice.

3.5 Rung three: rewrites, or data that wiggles

The third rung adds rewrites, and with it the thing an ordinary schema cannot do: the data moves on its own.

Rewrites {
    Beta     : (App (Lam ^x.body) arg) ~> (subst ^x.body arg);
    AppCongL : if M0 ~> M1 then (App M0 N) ~> (App M1 N);
}

That is the lambda calculus, in two of the four lines a real definition takes. The first line is the computation rule — and note that beta reduction is literally the substitution of an argument into an abstraction, written as such. The second is a congruence rule saying where the first is allowed to fire; the if …then premise is the horizontal bar of an inference rule. Together they make a term of type Term not an inert value but a small running program.

Once a channel is typed by such a definition, sending on that channel means sending a term of a language — a term that can be inspected, matched against, and stepped by the recipient. Two agents that share a language definition can exchange programs in a domain-specific language constructed for the purpose, and the recipient knows what it received because the definition came with it.

The slogan for this rung is the data can wiggle, and its practical form is that the boundary between data and code, which most systems maintain by convention and defend with a serialisation format, is a dial here rather than a wall.

3.6 Rung four: a language definition takes parameters

A developer who has just written the RhoCalc declaration above will notice something about it. Parallel composition is associative, it is commutative, and PZero is its unit. That is a commutative monoid. It is also, verbatim, the structure of integer addition, of string concatenation up to reordering, of set union, and of every other commutative monoid the developer has ever implemented. Writing it out again is the same waste it always was.

The fourth rung is the answer, and it is the familiar one.

Theory EmptySet() {
    Types { Elem; }
    Exports { Elem; }
}

Theory Monoid(s: EmptySet) {
    s
      Terms {
        One  . |- "1" : Elem;
        Mult . x:Elem, y:Elem |- "(" x "*" y ")" : Elem;
      }
      Equations {
        (Mult (Mult x y) z) == (Mult x (Mult y z));
        (Mult x (One)) == x;
        (Mult (One) x) == x;
      }
}

Theory CommutativeMonoid(m: Monoid) {
    m
      Replacements {
        One  => Zero . |- "0" : Elem;
        Mult => Plus . x:Elem, y:Elem |- "(" x "+" y ")" : Elem;
      }
      Equations {
        (Plus x y) == (Plus y x);
      }
}

Two things are happening, and the second is the unfamiliar one.

Monoid takes a theory as a parameter and extends it. That is an ML functor, or a generic class, or whatever the reader’s language calls a module parameterised by another module. Note where the parameter appears: not only in the head, but as the first thing in the body. s is the theory the chain starts from, and each block after it applies to the result of the one before. A body is not a record of five fields; it is a pipeline.

And CommutativeMonoid does something a generic class cannot: a Replacements block renames an inherited constructor and gives it new concrete syntax. Zero and Plus are not new operations sitting alongside One and Mult; they are One and Mult, spelled additively. Every equation proved of the one holds of the other, because they are the same element of the same theory. This is the distinction that the rest of §3.8 turns on, so it is worth naming now: a replacement changes a spelling and preserves an identity.

Which is what lets f1r3|@ng’s parallel composition be defined rather than declared:

Theory ParMonoid(cm: u.CommutativeMonoid) {
    cm
      Exports {
        Elem => Proc;
      }
      Replacements {
        Zero => PZero . |- "0" : Proc;
        Plus => PPar  . ps:HashBag(Proc) |- "{" ps.*sep("|") "}" : Proc;
      }
      Rewrites {
        RPar : if S ~> T then (PPar {S, ...rest}) ~> (PPar {T, ...rest});
      }
}

Parallel composition is commutative-monoid multiplication with the carrier renamed to Proc. That is the whole definition. Associativity, commutativity, and the unit law arrive with it and are not restated.

3.7 The module declaration

Theories do not float free. They are declared inside a Module, which is the unit of distribution — the thing that has a name, gets published to an address, and is imported by other people’s code.

import "UnivAlg.module" as u
import Monoid from "UnivAlg.module"

Module Rholang {

    Theory ParMonoid(cm: u.CommutativeMonoid) { ... }
    Theory QuoteDropCalc(pm: ParMonoid)       { ... }
    Theory RhoCalc(qd: QuoteDropCalc)         { ... }
    Theory NewReplCalc(qd: QuoteDropCalc)     { ... }

    Theory Rholang(nr: NewReplCalc, rc: RhoCalc) {
        nr \/ rc
    }

    Theory FreeRholang() {
        let s  = u.EmptySet() in (
        let m  = u.Monoid(s) in (
        let cm = u.CommutativeMonoid(m) in (
        let pm = ParMonoid(cm) in (
        let qd = QuoteDropCalc(pm) in (
        let nr = NewReplCalc(qd) in (
        let rc = RhoCalc(qd) in (
        Rholang(nr, rc)
        )))))))
    }

    theory FreeRholang()
}

The theory names are the historical ones and are worth reading as such: Rholang here names the calculus f1r3|@ng inherited its control flow from, presented as one theory among others. Naming it is the point — §3 began by saying the calculus underneath is not privileged, and this is what that looks like in a file.

Four things in that skeleton are worth calling out, because each is a decision a developer will meet on the first afternoon.

3.7.0.1 Imports name an address, not a path.

import "…" as u brings a whole module in under an alias, after which its theories are reached by dotted path — u.CommutativeMonoid. import Monoid from "…" brings one theory in unqualified. The string is a URL. This is the choice that aligns the module system with the deployment target: a language definition published on chain has an address, and importing it is the same act whether it came from the next directory or from another party’s node. Resolution happens at compile time, in the client toolchain. A node never fetches anything.

3.7.0.2 Capital Theory declares; lowercase theory instantiates.

A module full of Theory declarations has produced no language yet; it has produced a vocabulary for building one. The final theory FreeRholang() is the entry point, and it is what the elaborator runs. The last such line in the entry module wins. Keeping the two acts apart is what allows a library module to ship a dozen theories and commit to none of them.

3.7.0.3 A theory body is an expression, and it has a grammar.

Everything between the braces of a Theory declaration is one expression built from three kinds of thing.

Because the builders form an ordered chain rather than a record, they can interleave — AbelianGroup in the universal-algebra module does a Replacements block and then joins with a sibling — and they carry an obligation the record form did not: a Terms block must precede any Equations or Rewrites block that mentions its labels. A forward reference is a diagnostic, not a resolution pass.

3.7.0.4 Types declares, Exports publishes.

These are two jobs and they used to be one, which is worth a sentence because the separation is what turns a class of modelling error into a compiler message. Types brings a syntactic category into being. Exports controls which of them a consumer can see, and optionally renames them on the way out — Elem => Proc above. A theory can now have a category that is real and private. More to the point, two theories that each declare a category called Name are now visibly declaring two different categories, which is exactly the mistake §3.8 is about.

3.8 What sharing means, and why the compiler argues about it

The combination operator has a subtlety that is worth a developer’s attention, because the compiler will raise it whether or not the developer was expecting the conversation.

Look again at FreeRholang. One theory adds restriction and replication, another adds send and receive, and both are built on QuoteDropCalc. Combining them must not produce two parallel compositions, two Name categories, and two quotation operators.

The let chain is what prevents it. QuoteDropCalc(pm) is elaborated once and bound to qd; both nr and rc are built from that one instance; so when they are combined, everything they inherited from it is recognised as the same thing arriving by two routes, and appears once. The combination is a pushout over the shared ancestor rather than a union.

What makes that work mechanically is that every element gets an identity token when it is introduced, and carries it through inheritance — including through a Replacements block, which is why renaming preserves sharing. Two elements are the same element if they have the same origin. Combination identifies elements by origin, the common fragment intersects by origin, and subtraction removes by origin. Names have nothing to do with it.

The practical consequence is that sharing is a claim, and the compiler holds you to it. Build the two halves from two separate instances and combine them, and the result is a diagnostic rather than a silently doubled calculus. The reference elaborator ships a corpus of these; the four that a working developer is most likely to trip over are worth having seen once:

This is unfamiliar and it is worth sitting with, because it is the same diagnostic that catches genuine modelling errors. A rig has one carrier and two monoid structures on it — addition and multiplication — and the natural way to write it is to instantiate Monoid once and pass it as both arguments. That is wrong: it asserts that addition and multiplication are the same operation. The compiler says so. Instantiating Monoid twice over one shared EmptySet is the correct structure, and it says exactly what a rig is: two monoids, one carrier.

A developer used to inheritance will recognise the diamond problem here, and should notice that the resolution is different in kind. There is no linearised method resolution order and no “last one wins”. Two elements are the same element if they have the same origin, and otherwise they are two elements; if they also have the same name, that is an error rather than a silent override.

3.9 The parameter as a contract: extending a theory you did not write

The reuse story so far is about not repeating yourself. There is a second payoff, and for anyone maintaining a language definition alongside other people it is the larger one.

Consider a design that has an object language — a dependently typed calculus with typed holes, used as the specification format for a marketplace of partly specified programs [43] — and a second design that adds prices to it. The priced language is not a copy of the first with extra lines. It is a theory that takes the first as a parameter:

Theory PricedPFLam(pf: PFLam) {
    pf
      Types {
        Price;       // an element of the preference quantale
        Obsv;        // a time-varying observable
      }
      Terms {
        Priced . h:HoleId, ty:Term, p:Price
               |- "?" h ":" ty "@" p                  : Term;
        Scale  . o:Obsv, c:Term |- "scale" "(" o "," c ")" : Term;
        Give   . c:Term         |- "give" "(" c ")"        : Term;
      }
      Equations {
        (Give (Give c)) == c;
      }
}

Everything established about PFLam arrives with the parameter. Nothing is restated. And — the point — if a later revision of PFLam renames Hole or changes its arity, the break is reported here, at elaboration, rather than discovered later by a reader noticing that two documents disagree. Before the fourth rung existed, this delta was written as prose on a listing: only additions shown. A prose annotation cannot be checked. A parameter can.

The same applies at combination. If a venue also imports a reputation theory over the same hole identifiers, the two join over their shared PFLam instance and the identifiers are identified once. Passing two independently instantiated copies is rejected, and correctly: it would assert that the priced holes and the reputed holes are different holes.

3.10 Channels are typed by language definitions

The connection back to §2 is one sentence: a channel’s type is a language definition — which is to say, an elaborated Theory.

That single design decision explains the rest of the note. Sending on the channel means sending a term of that theory. Matching a pattern on it means matching a term of that theory, up to that theory’s equations. And — the point of §4 — asking a condition about what arrived means asking a question in a logic that is generated from that theory, because the theory says what there is to ask about.

For the forager, this means the specimen language is a language definition, Chi is a formula in the logic that definition generates, and there was never a moment at which someone hand-designed a predicate vocabulary.

3.11 MeTTa, and what this adds to it

Readers coming from SingularityNET’s Hyperon stack [11] will have recognised the shape of the third rung, because MeTTa is built on it. The relationship is worth stating precisely, in both directions.

The two gaps compound. Without equations, a developer who wants “these two atoms are the same” writes rewrite rules that say so, and then owns the confluence question — whether the order in which rules fire can change the answer. Without a witnessed transaction, a developer who wants two atom spaces updated together writes a protocol, and then owns the partial-failure question. Both are exactly the questions the two blocks and the communication rule answer for free.

None of which is a dismissal. MeTTa has a large working ecosystem, a substantial body of practice around the atom space as a shared knowledge medium, and Probabilistic Logic Networks [12], which is a serious piece of engineering for reasoning under uncertainty. It is worth saying plainly that PLN is not left behind here: in §5 it comes back as one of the value algebras a where clause can be graded in, which is to say that PLN inference can drive execution rather than sitting beside it. The relationship this note is proposing is embedding with an addition, not replacement.

3.12 What an operation costs

One more piece belongs to the data definition story, because it is the thing that makes the forager’s budget real rather than notional.

Cost accounting in this system adds exactly two surface forms, and both of them lower to ordinary f1r3|@ng:

That is the entire mechanic. Spending fuel is a communication: the gate consumes one token, releases its payload, and then P runs. If no token is available on the signature channel, the gate parks forever and P never runs — and that is what metering means here. A budget is a stack of nested sends, and its depth is how many operations it funds.

Two things follow that a developer should notice.

First, metering is not a virtual-machine feature bolted onto a language. It is a program in the language, and the transpiler’s job is only to write it for you. Anything true of unmetered f1r3|@ng is true of metered f1r3|@ng.

Second, it composes with Claim 3 in a satisfying way. A communication that is not funded is a communication that does not happen, and it is indistinguishable from a communication whose guard failed. Both are non-events. There is no separate failure mode for running out of budget, no exception, and nothing to unwind — which is exactly the property that lets the forager’s death be modelled as “it stops” rather than as an error path.

The repository [49] ships a worked demonstration of this at scale: a supply chain in which factories produce, carriers ship, sellers wholesale and buyers retail, with money and inventory both conserved, and every single operation gated by a token. It is the best available answer to “show me this doing something real”.

3.13 What actually runs

Honesty about status is more useful to a developer than enthusiasm, so the table below separates three things a reader has every right to keep apart: specified means the surface is frozen and written down; implemented means there is code a reader can run; planned means neither yet.

The condition language a developer can write today is boolean expressions over the variables the patterns bound — x > 0, and so on. Everything in the next section is about what that slot is going to hold, and why the choice is more interesting than it looks.

4 Widening one: what a condition can see

4.1 The condition language is generated, not designed

Here is the claim of this section, stated first so the rest can be read as support for it.

The vocabulary available in a where clause is not a fixed list of built-in predicates, and nobody sat down and designed it. It is constructed from the language definition that types the channel. Change the language definition, and the condition language changes with it, automatically and in a specified way.

That is worth dwelling on because the alternative — a fixed predicate library — is what every other system does, and its failure mode is familiar. A query language ships with the predicates its designers anticipated. When a developer needs one that was not anticipated, the escape hatch is a user-defined function, which is opaque to the optimiser, the index, and the type system. Generated conditions have no escape hatch because they have no fixed list to escape from.

A generated condition language has three components, and the account of why it has exactly these three is a realizability argument set out elsewhere [31]. Two of them come from the language definition and one is a choice.

4.2 Structural connectives: pattern matching that can talk about namespaces

The structural component is the easiest to get a feel for, because it is recognisably a generalisation of pattern matching.

Every constructor in the terms block yields a connective. If the theory has POutput . n:Name, q:Proc |- n "!" "(" q ")" : Proc, the logic gets a way to say “a send, on a name satisfying $\varphi$, of a term satisfying $\psi$”. Nested, these compose into descriptions of arbitrary shape.

Two of the generated connectives are worth naming because they do things ordinary patterns cannot.

4.2.0.1 Separating conjunction.

Because parallel composition is associative-commutative — an equation, from rung two — the connective it generates is not ordinary conjunction but a separating one: $\varphi \mid \psi$ holds of a term that splits into two parts, one satisfying $\varphi$ and one satisfying $\psi$, with the split being a real partition. This is the same idea as separation logic’s separating conjunction [19], and the same connective the spatial logics for concurrency carry [4], and it is what lets a condition say “there are two of these, and they are not the same one” — a sentence ordinary conjunction cannot express.

4.2.0.2 The name predicate.

Because names are quoted terms, a condition can descend from a name into the term it quotes [47]: @$\varphi$ holds of a name whose quoted process satisfies $\varphi$. In developer terms, this means a condition can talk about namespaces — about the shape of the addresses involved, not just the payloads. The forager’s belief channel and the specimen channel are distinguishable to a condition by what kind of name they are, which is how one describes a region of the address space rather than enumerating it.

4.3 Behavioural connectives: asking about the future

The behavioural component is the one with no analogue in a query language. For each rewrite rule, and each position in the term where that rule could fire, the logic gets a modality $\langle K \rangle \varphi$ — a refinement of the modality of Hennessy–Milner logic [13], indexed by rewrite rule and position rather than by action [42] — read: there is a step of this rule at this position, after which $\varphi$ holds.

The forager’s use for this is immediate. Chi(spec) as written is a structural question — does this specimen look a certain way. A behavioural question is different: does this specimen, if poked, do a certain thing. Both are legitimate hypotheses. They are priced very differently.

Remark 1 now acquires a sharper form. Driving means acting, and acting on the thing you are trying to observe changes it. A system that wants perception to be non-disturbing must arrange that its observational apparatus uses peeks and its interactions use linear receipts — and the two must sit in different namespaces, so that a formula meant to look cannot accidentally claim. In the forager, reading the specimen’s structure and opening the specimen must be different names, or the assessment eats the subject.

4.4 The collection component is a dial

The third component is a choice, and it is the most consequential one in this section. A logic needs somewhere to put its witnesses — the things that make a formula true — and the container chosen determines which logical operations even exist.

The distinction between the first two rows is the distinction between counting and noticing. A Boolean condition, asked whether there are three red items, answers a question about presence: there are red ones. It cannot count them, because in a set two witnesses of the same kind collapse into one. A linear condition keeps them apart, because in a quantale they do not collapse. If you have ever wanted a query that says “at least three distinct matching rows, and consuming one of them consumes it for everyone”, the second row is where that lives.

The third row is stranger and more useful than it sounds. Coalition logic asks about groups: is there a set of participants such that, together, they can bring something about. Read as a condition on a running population — other programs in the environment — it asks whether a quorum has formed [37]. The forager can use this to ask whether the specimens around it are of a kind that behaves as a group, without participating in any protocol they might be running.

4.5 What the dial costs

Turning the dial up is not free, and the price is worth stating in the terms a developer cares about.

4.5.0.1 A more expressive condition may not terminate.

The behavioural modality asks about steps, and a term can step forever. Fixed points over the modality — “it keeps being able to do this” — are expressive and unbounded. The mitigation is that evaluating a guard is metered like everything else: a budget bounds the check, and an unfunded check is a non-event by §3.12, so it fails safe.

4.5.0.2 Restricting to make checking terminate loses something real.

A developer who wants guards that always answer can restrict to a fragment — fewer connectives, or a smaller slice of the theory. That works. What is surrendered is adequacy: the property that the logic can distinguish any two programs that actually behave differently. In general, a logic whose model checking always terminates cannot be adequate for a Turing-complete theory. This is not a defect of the construction; it is the shape of the trade, and the dial exists precisely so it can be made deliberately rather than by accident.

4.5.0.3 Adequacy is a property of the target, not of the generator.

It is tempting to assume that a machine-generated logic comes with a guarantee. It does not, and it should not: whether the generated logic is adequate depends on which connectives were asked for. Without something like a negation and a conjunction, it will not be. A generated type system, for instance, is generated by the same family of algorithms and is not expected to be adequate at all [42, 30].

4.6 The forager’s ladder

Return to the running example. Chi(spec) was a placeholder for one hypothesis. The dial says there is a whole ladder of possible hypotheses, from cheap structural ones to expensive behavioural ones, and the forager can afford to sit anywhere on it.

That is not a metaphor: it has been measured. In a companion study [39], a learner of exactly this shape was equipped with a ladder of hypotheses expressed as where clauses, each priced by the depth of the formula it installs, and run to exhaustion against a fixed environment.

The last row is the one to carry forward. It says that the right position on the dial is not a property of the problem, and certainly not a matter of rigour. It is an economic question about the environment the program is deployed into, and it is answerable — because both the sight and the acting are priced in the same currency.

5 Widening two: when the condition stops answering yes or no

5.1 The move

A guard returns a truth value, and the communication fires or does not. That is one choice, not the only one. The second widening is to let a condition return a value in some other algebra — a probability, a rate, a cost, a complex amplitude — and to interpret that value as how much this candidate happens rather than whether it happens.

Before anything else, the reassurance a developer needs:

So this is an extension in the strict sense. A developer who never grades a condition never encounters any of what follows. A developer who grades one gets something that turns out to be much larger than a weighted choice.

5.2 What a value algebra has to supply

Not every set of values will do. The condition language has conjunction and disjunction in it, so whatever the values are, there must be an operation to interpret each. The requirement is mild: a commutative semiring [33]. Multiplication $\otimes$ interprets conjunction, addition $\oplus$ interprets disjunction, and the units behave as true and false do.

Which value algebra a program is read in is not merely a choice of numerics: it fixes how much of the non-determinism a resolver has to decide, and that question has a precise hierarchy behind it [36]. One casualty is worth naming immediately, because it surprises people. Negation does not survive. Over $[0,1]$ the map $x \mapsto 1-x$ behaves well enough, but over the complex numbers there is no canonical negation and De Morgan fails. The practical consequence is that the design keeps two sorts of formula: a crisp sort with the full Boolean structure, used for gating, and a graded sort with a semiring only, used for weighting. A where clause keeps its old job and gains a new slot.

5.3 The guard becomes a weight

Recall candidates from §2.7: for a comprehension with data available, each way of assigning data to patterns is a candidate. In the crisp setting the condition is evaluated per candidate and admits or refuses it. In the graded setting the condition is evaluated per candidate and scores it.

That is the entire mechanism, and three worthwhile things fall out of it without further work.

5.3.0.1 The propensity is the formula’s value, and formulas move.

A crisp guard is a fixed policy: it fires on the same specimens forever, because the formula does not change. A graded guard’s behaviour is the formula’s value, evaluated against the current state — and the current state includes whatever the program has learned. Nothing needs to be scheduled.

5.3.0.2 Weight tables are unnecessary.

A common design for stochastic execution [41] attaches a table of rates to each rule, keyed by conditions, and then requires those conditions to partition the space so that lookup is single-valued. A graded clause needs none of that: a formula has one value, so single-valuedness is free, and overlapping conditions are simply fine.

5.3.0.3 Plasticity is free.

Because the clause is evaluated against the current term, weights that change during execution require no update mechanism. The weight is not stored; it is computed.

5.4 Three readings of one program

Here is where the section earns its title. The same program text, under three different value algebras, is three different kinds of artefact.

5.4.0.1 Booleans: a state transition.

The program is what it has been all along — code running in a node, manipulating state, committing transactions. Programming in the small.

5.4.0.2 Non-negative reals: a stochastic simulation.

Each candidate carries a rate. The total rate at a configuration determines how long the system waits and which step it takes; this is the standard Gillespie construction [9], and it turns the program into a generator of trajectories — the same move that took the $\pi$-calculus to the stochastic $\pi$-calculus and to SPiM [17, 18], and that the weighted reading of a language definition generalises [41]. Running it many times gives you the distribution of outcomes rather than one outcome. Programming in the large: the subject is no longer this program’s state but the behaviour of a population of them.

5.4.0.3 Complex numbers: a quantum simulation.

Each candidate carries an amplitude [34], and candidates that reach the same outcome have their amplitudes added before magnitudes are taken — which is to say, they interfere. Two branches that are individually possible can cancel — the effect Shor’s algorithm is built out of [23]. A developer’s summary: disjunction stops being monotone, and a false disjunction with true disjuncts becomes expressible.

5.5 Programming in the small, programming in the large

The reason to care is not that a simulator exists. Simulators exist. The reason to care is that it is the same program text.

The usual arrangement in industry is two artefacts: the system, written in one language by one team, and the model of the system, written in another language by another team, for capacity planning or risk or verification. The model is always a little wrong, it goes stale immediately, and the discrepancy is discovered in production.

Here the model and the system are the same source. A developer writes a comprehension with a graded condition; under the node’s resolver it is a transaction, and under the simulator’s resolver it is a model of what a population of such transactions would do. There is no translation step in which fidelity is lost, because there is no translation step.

The practical questions this makes askable, in the language the system is written in:

• If this contract is deployed a thousand times against that environment, what is the distribution of outcomes?

• Which of these two policies survives longer under a shift in the environment?

• Is there a configuration reachable from here that we would consider a failure, and how much would getting there cost an adversary?

5.6 The forager, graded

Now the running example, all the way through. The forager’s clause becomes:

new bel, prey, wall in {
  bel!( (1, 0.5) ) |                    // (n, s): one unit of prior evidence

  for( @(n,s) <- bel ; @spec <- prey  where  Chi(spec) * Pow(n,s) ) {
    Break!(spec) | bel!( revise(n, s, spec) )
  } |
  for( @(n,s) <- bel ; @spec <- prey  where  g ) {
    Graze!(*wall) | bel!( (n, s) )
  }
}

Chi(spec) is the crisp structural predicate of §4, entering the graded sort as an indicator. Pow(n,s) is a graded ground formula whose value is the PLN power $s\cdot c$, where $c= n/(n+k)$ is confidence and $k$ is the learner’s scepticism [12]. * is graded conjunction. g is a scalar: the value of grazing.

Two comprehensions, each with a weight. The forager opens the specimen with propensity $sc$ against the wall’s $g$. Everything below was measured by running exactly this.

5.6.0.1 The bootstrap trap, and why exploration is a disjunct.

A belief with no evidence has $c= 0$, hence power $0$, hence a clause value of zero, hence a receipt that never fires — so it never acquires evidence. Measured: a forager initialised with no prior evidence opens $0.00$ specimens across $400$ encounters and ends with exactly the grazing baseline, against $3543.7$ for the same forager given one unit of prior evidence.

The remedy is written in the clause language, not in a framework. Either the belief carries prior evidence $n_0 \geq 1$, or the clause is $\mathrm{Pow}(n,s) \oplus\varepsilon$ for a small scalar $\varepsilon$. That second form is $\varepsilon$-greedy exploration, and it is a disjunct.

5.6.0.2 Confidence buys variance, not yield.

Four foragers, two worlds, $20{,}000$ lives each. In the benign world the crisp forager — which acts on a satisfied guard from its first encounter — has the highest mean terminal holdings, $4084.7$, and the lowest survival, $0.8501$. The graded forager has survival $0.9485$ and holdings $3543.7$. That is the trade a mortal program actually faces, and a Boolean guard cannot express it.

5.6.0.3 A Boolean guard has no coordinate in which to record disappointment.

In the hostile world, where opening is a net loss, the crisp forager survives $0.29\%$ of the time. It cannot do otherwise: its policy is the formula, and the formula does not change. The graded forager’s policy is the formula’s value, which moves:

Strength falls as decoys accumulate, confidence rises, the product falls, and with it the willingness to open. The forager learns to stop. Note that nothing in the clause is a schedule: early caution and late decisiveness are consequences of a coordinate of the truth value, not of a hyperparameter someone tuned.

5.6.0.4 Your where clause has become a learning rule.

This is the point at which the exposition arrives somewhere a developer would not have predicted from §2. In a one-dimensional grading, the revision step that updates the belief turns out to be a natural gradient step [2] on the underlying likelihood — to machine precision, verified over $20{,}000$ random instances at a worst discrepancy of $1.1 \times 10^{-16}$. Better, it is an implicit step in the sense of stochastic approximation [20], and therefore unconditionally stable: it cannot leave the valid range of values for any observation, where the explicit version can. The confidence coordinate is not a second belief. It is the metric with respect to which the first one is being learned.

The score that the gradient is assembled from decomposes into contributions computable at each communication site, from what the site already has — which is the identity that makes policy-gradient methods implementable [25] and, here, makes the gradient a message rather than a backward pass. The developer’s version of that sentence: grading a condition gives you gradient descent in the small, correctly conditioned, without importing a learning framework and without a separate training loop. The learning rule is the clause.

5.7 What is settled and what is not

Three honest boundaries, since the previous subsection was enthusiastic.

5.7.0.1 The stochastic reading is solid; the quantum reading has a fence around it.

The complex-valued case is established for a restricted fragment — finite, contractive, staged — and not for the language as a whole. Two specific hazards sit behind that fence. Left unrestricted, the construction buys post-selection, and a language with free post-selection decides more than quantum computers do [1]. And the coherent branching this needs is quantum control rather than the architecture of the quantum process calculi, which keep the quantum state beside the process rather than in the branching [8, 29, 3]. The research note that develops it [34] states its own boundary as: a finite, contractive, staged fragment of graded rho admits a candidate quantum interpretation, and the extension to unrestricted reflective concurrency remains open. That fence is where it is for good reasons, and a developer should read the complex row of the table above as “there is a real construction here for circuit-shaped programs” rather than “f1r3|@ng is a quantum language”.

5.7.0.2 Learning under a moving target is not solved.

The measured experiments include a regime shift, and under it every arm’s accuracy degrades in proportion to how much evidence it had accumulated. Accumulated confidence makes a learner rigid, and rigidity is exactly wrong when the world changes. This is a known gap, named as such in the companion note [35], and it is the most consequential one.

5.7.0.3 Two searches, not one.

Grading gives a gradient within a hypothesis — tuning the numbers in a clause. It does not give a gradient between hypotheses — changing which formula the clause contains. That second search is discrete and looks like recombination rather than descent [40]. The split between the two is not an engineering decision; it follows from the shape of the hypothesis space.

6 Where this leaves a developer

6.1 The through-line in one page

The exposition began at a place every reader already knew and moved by necessity rather than by exposition. It is worth collecting the steps, because each was forced by the one before.

1. The comprehension SELECT-FROM-WHERE is what data access looks like, in every language that has one. It has no DO.

2. LINQ exists to embed it in a host language so that a developer can finally express the DO. f1r3|@ng goes the rest of the way and builds the language around the comprehension: for( ptrn <- chan where cond )P, with chan!(Q) as its dual.

3. Making both the read and the write explicit turns a communication into a meeting, and the substitution the rule performs is the witness. Transactions become a property of the program text: a failed guard is not rolled back because nothing was consumed.

4. That leaves the pattern and the condition unaccounted for, which forces a data definition sublanguage. f1r3|@ng’s Theory declaration supplies it in four rungs: grammar, equations, rewrites, parameters. The second rung holds all the invariants your type system cannot read; the third makes the data wiggle; the fourth makes a language definition something you can ship, import by address, and extend without copying.

5. Because the fourth rung exists, a language definition composes like a module rather than like a file. Theories combine over shared ancestors, and the elaborator holds you to the claim: two things that arrived by different routes are two things, and if they share a name that is an error rather than an override.

6. That structure subsumes MeTTa — rules are rewrites, atom spaces are channels — and adds the two things MeTTa lacks: an equational layer and a witnessed transaction.

7. The condition language is generated from the language definition rather than designed. Choosing the container for witnesses turns a dial between Boolean, linear and coalition sight, and the choice is an economic one about the deployment environment rather than a matter of rigour.

8. Grading the condition replaces the verdict with a value. At Booleans nothing changes; at the non-negative reals the program becomes a stochastic simulation of a population of itself; at the complex numbers, on a fenced fragment, a quantum one. Same text, two resolvers, no model drift.

9. In the graded setting the forager’s guard is a learning rule, and the update is a correctly conditioned, unconditionally stable gradient step — arrived at without importing anything.

6.2 What to do on Monday

For a developer who wants to touch this rather than read about it, in order of increasing commitment:

• Run the two guard examples — the receive guard and the match fall-through — on the cost-accounting-transpiler branch of f1r3node-rust [49]. They are small, they compile, and they are covered by tests. Change the guard and watch what does and does not get consumed.

• Run the cost-accounting demonstration in the same directory. It is a supply chain with conserved money and conserved inventory in which every operation is gated by a token, and it is the best available answer to what metering feels like when it is a program rather than a runtime flag.

• Run the reference elaborator on its own corpus, on the branch that carries it [50]. It is dependency-free and builds in seconds. The instructive half of that corpus is the bad/ directory: six modules that are wrong on purpose, each with the diagnostic it earns. Reading those is the fastest way to acquire the sharing-is-a-claim reflex of §3.8.

• Write a Theory declaration for a data format you already own — ideally one whose type has an invariant currently maintained by a comment. Put the comment in the Equations block. That single exercise is the fastest way to feel the difference between rung one and rung two.

• Then, if the shape of the thing appeals, add a Rewrites block and discover that you have written a domain-specific language — and then take the part of it that was not specific to your domain, give it a parameter, and discover you have written two.

6.3 Where to read next

This note is deliberately the shallow end. The following are the deep ends, one line each.

6.4 A closing observation

There is a temptation, reading a note like this, to treat the last two sections as the interesting part and the first two as preliminaries. Your author would put it the other way round.

The two widenings are widenings of one slot. That slot exists because the comprehension has a WHERE clause, and it has a WHERE clause because SQL had one in 1974 [5]. Nothing was invented to accommodate generated logics or graded values; a place for them was already present in the shape every developer already uses, and had been sitting empty. What this note describes is mostly the consequence of taking that shape seriously enough to build a language around it rather than embedding it in one.

The DO is the part LINQ went looking for. The rest of it is what you find when you keep going.

• [1] S. Aaronson. Quantum computing, postselection, and probabilistic polynomial-time. Proceedings of the Royal Society A, 461(2063):3473–3482, 2005.
• [2] S.-I. Amari. Natural gradient works efficiently in learning. Neural Computation, 10(2):251–276, 1998.
• [3] C. Badescu and P. Panangaden. Quantum alternation: prospects and problems. In Proceedings of Quantum Physics and Logic (QPL), EPTCS, 2015. arXiv:1511.01567.
• [4] L. Caires and L. Cardelli. A spatial logic for concurrency (part I). Information and Computation, 186(2):194–235, 2003.
• [5] D. D. Chamberlin and R. F. Boyce. SEQUEL: A structured English query language. In Proceedings of the ACM SIGFIDET Workshop on Data Description, Access and Control, pages 249–264, 1974.
• [6] E. F. Codd. A relational model of data for large shared data banks. Communications of the ACM, 13(6):377–387, 1970.
• [7] M. J. Gabbay and G. Losa. Semitopology: distributed collaborative action via topology, algebra and logic. Manuscript, 2023.
• [8] S. J. Gay and R. Nagarajan. Communicating quantum processes. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 145–157, 2005.
• [9] D. T. Gillespie. Exact stochastic simulation of coupled chemical reactions. The Journal of Physical Chemistry, 81(25):2340–2361, 1977.
• [10] J.-Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1–101, 1987.
• [11] B. Goertzel et al. OpenCog Hyperon: a framework for AGI at the human level and beyond. Manuscript, SingularityNET, 2023.
• [12] B. Goertzel, M. Iklé, I. F. Goertzel, and A. Heljakka. Probabilistic Logic Networks: A Comprehensive Framework for Uncertain Inference. Springer, 2008.
• [13] M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137–161, 1985.
• [14] E. Meijer, B. Beckman, and G. Bierman. LINQ: reconciling object, relations and XML in the .NET framework. In Proceedings of the ACM SIGMOD International Conference on Management of Data, page 706, 2006.
• [15] R. Milner. Functions as processes. Mathematical Structures in Computer Science, 2(2):119–141, 1992.
• [16] G. D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University, 1981. Reprinted in Journal of Logic and Algebraic Programming, 60–61:17–139, 2004.
• [17] C. Priami. Stochastic $\pi$-calculus. The Computer Journal, 38(7):578–589, 1995.
• [18] A. Phillips and L. Cardelli. Efficient, correct simulation of biological processes in the stochastic $\pi$-calculus. In Computational Methods in Systems Biology (CMSB), LNCS 4695, pages 184–199, 2007.
• [19] J. C. Reynolds. Separation logic: a logic for shared mutable data structures. In Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS), pages 55–74, 2002.
• [20] H. Robbins and S. Monro. A stochastic approximation method. The Annals of Mathematical Statistics, 22(3):400–407, 1951.
• [21] K. I. Rosenthal. Quantales and Their Applications. Pitman Research Notes in Mathematics 234. Longman, 1990.
• [22] M. Pauly. A modal logic for coalitional power in games. Journal of Logic and Computation, 12(1):149–166, 2002.
• [23] P. W. Shor. Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer. SIAM Journal on Computing, 26(5):1484–1509, 1997.
• [24] P. Wadler. List comprehensions. In S. L. Peyton Jones, The Implementation of Functional Programming Languages, chapter 7. Prentice Hall, 1987.
• [25] R. J. Williams. Simple statistical gradient-following algorithms for connectionist reinforcement learning. Machine Learning, 8(3–4):229–256, 1992.
• [26] S. Boag, D. Chamberlin, M. F. Fernández, D. Florescu, J. Robie, and J. Siméon. XQuery 1.0: An XML query language. W3C Recommendation, 2007.
• [27] J. Robie, D. Chamberlin, M. Dyck, D. Florescu, J. Melton, and J. Siméon. XQuery Update Facility 1.0. W3C Recommendation, 2011.
• [28] D. N. Yetter. Quantales and (noncommutative) linear logic. The Journal of Symbolic Logic, 55(1):41–64, 1990.
• [29] M. Ying, N. Yu, and Y. Feng. Alternation in quantum programming: from superposition of data to superposition of programs. arXiv:1402.5172, 2014.
• F1R3FLY.io working notes. Unless otherwise stated, each of the notes below lives in the F1R3FLY.io publications repository, and the directory holding it is given so that it can be found. Several of them predate the name f1r3|@ng and speak of MeTTaIL, or of rholang 1.4. They are the same language.
• [30] L. G. Meredith. Graph-structured lambda theories: a reference for the working developer. F1R3FLY.io working note, 2026. GSLT-intro/.
• [31] L. G. Meredith. Splitting the mind of Zeus: packaging, splittings, and the three components of a logic. F1R3FLY.io working note, 2026. on-the-nature-of-logic/.
• [32] L. G. Meredith. Observation disciplines: how logics are generated from term structure, and why graded where-clauses are the mortal scientist’s instrument. F1R3FLY.io working note (omnibus), 2026. rho-mind/observation-disciplines/.
• [33] L. G. Meredith. Graded where-clauses: non-crisp truth values as the syntax of non-determinism resolution in the rho calculus. F1R3FLY.io working note, 2026. fuzzyware/.
• [34] L. G. Meredith. Races decided by the Born rule. F1R3FLY.io working note, 2026. fuzzyware/.
• [35] L. G. Meredith. Graded where-clauses over the reals: one-dimensional grading as the mortal scientist’s gradient, and probabilistic logic as the metric that gradient requires. F1R3FLY.io working note, 2026. fuzzyware/.
• [36] L. G. Meredith. Choice principles as graded where-clauses: one programming paradigm at every altitude of the Weihrauch lattice. F1R3FLY.io working note, 2026. choice-types/.
• [37] L. G. Meredith. Reading the herd: coalition logic as a graded hypothesis language for populations of computations. F1R3FLY.io working note, 2026. consensus-types/.
• [38] L. G. Meredith. The mortal scientist: learning as cost-accounted computation in a reflective higher-order calculus. F1R3FLY.io working note, 2026. rho-life/.
• [39] L. G. Meredith. Learning to play. F1R3FLY.io working note, 2026. rho-life/.
• [40] L. G. Meredith. Composing learners: populations as namespaces, parallel composition as the operator. F1R3FLY.io working note, 2026. rho-life/.
• [41] L. G. Meredith. Weighted graph-structured lambda theories: stochastic and quantum execution for f1r3|@ng. F1R3FLY.io working note, second version, 2026. rho-life/.
• [42] M. Stay, L. G. Meredith, and J. B. Wells. Generating hypercubes of type systems. F1R3FLY.io working note, 2026. drafts/Hypercube/.
• [43] L. G. Meredith. Plausible fiction on f1r3|@ng: a requirements and design document for a typed marketplace of programmatic intentions. F1R3FLY.io working note, in dialogue with D. Spivak (Topos Institute), 2026. plausible-fiction/.
• [44] L. G. Meredith. Priced plausible fiction: PJES combinators over the conditional demand tree. F1R3FLY.io working note, 2026. plausible-fiction/.
• [45] L. G. Meredith. The data definition sublanguage and its module system: decisions, normative surface, and development plan. F1R3FLY.io working note, 19 August 2026, held under module-syntax/documentation/ on the branch cited below [50].
• [46] L. G. Meredith and M. Radestock. A reflective higher-order calculus. Electronic Notes in Theoretical Computer Science, 141(5):49–67, 2005.
• [47] L. G. Meredith and M. Radestock. Namespace logic: a logic for a reflective higher-order calculus. In Trustworthy Global Computing, LNCS 3705, pages 353–369, 2005.
• Software.
• [48] F1R3FLY.io. mettail-rust: the language-definition toolchain — generated parser, printer, substitution and rewrite engine — with definitions shipped for lambda, ambient, the rho calculus and a calculator. https://github.com/F1R3FLY-io/mettail-rust.
• [49] F1R3FLY.io. f1r3node-rust, branch feature/cost-accounting-transpiler: where guards, match guards, and the cost-accounting transpiler, with runnable examples under examples/. https://github.com/F1R3FLY-io/f1r3node-rust.
• [50] F1R3FLY.io. f1r3node-rust, branch feature/module-syntax: the mettail-elab reference elaborator for the Module and Theory surface, its worked corpus under examples/modules/ and its negative corpus under examples/modules/bad/, together with the grammar delta for the parser. https://github.com/F1R3FLY-io/f1r3node-rust.