A tree-structured representation of source code produced by a parser. Each node represents a syntactic construct; the tree abstracts away concrete syntax details like whitespace and punctuation, preserving only semantic structure. Used as the intermediate representation in compilers, linters, and metaprogramming systems.

A model of concurrent computation whose universal primitive is the actor: an isolated entity that responds to a message by sending finitely many messages, spawning finitely many new actors, and designating the behaviour it will use for the next message it receives. Communication is asynchronous and addressed to a named mailbox; actors share no state.

The linear connectives that encode choice: $\mathbin{\&}$ (with) and $\oplus$ (plus). They split proof search into branches rather than combining resources in parallel, distinguishing between internal choice (with) and external choice (plus).

A temporal logic whose path quantifiers are coalitions: $\langle\!\langle A\rangle\!\rangle\varphi$ says the agents in $A$ have a joint strategy that guarantees $\varphi$ whatever everyone else does. Where CTL asks what may or must happen, ATL asks who can make it happen, which turns questions of strategic ability in a multiagent system into model-checkable properties.

Deleuze and Guattari’s agencement: a working arrangement of heterogeneous components whose identity lies in what they do together rather than in what each component is. Relations are external to their terms, so a component can be unplugged and plugged into a different assemblage, and the whole holds together not by essence but by continual processes of territorialisation and deterritorialisation.

Mathematical notation for describing the limiting behaviour of functions. Includes $O(f(n))$ (upper bound), $\Omega(f(n))$ (lower bound), and $\Theta(f(n))$ (tight bound). For example, if $T(n) = 3n^2 + 2n + 1$, then $T(n) = O(n^2)$.

The sub-calculus of the π-calculus in which output carries no continuation: $\bar{x}\langle y\rangle$ is a whole process rather than a prefix, so sending never blocks and a pending output is simply a message in flight. Synchronous communication remains encodable via acknowledgement channels, so little expressive power is lost, and the variant is the usual formal setting for actor languages and other mailbox-based concurrency.

The belief-desire-intention model of agency, from Bratman’s philosophy of practical reasoning: an agent holds beliefs about the world, desires ranking the states it would prefer, and intentions, the desires it has committed to and now filters its options by. The point of intention is resource-bounded stability: an agent that reconsiders everything at every step never acts, so commitment is what makes deliberation tractable.

A mathematical notation that describes the limiting behaviour of a function when the argument tends towards a particular value or infinity. In computer science, it’s used to classify algorithms according to how their running time or space requirements grow as the input size grows.

A behavioural equivalence between processes: a relation in which each process can match every transition of the other, step for step, arriving at states that are again related. Two bisimilar processes are indistinguishable to any observer interacting with them, which makes bisimulation the standard notion of “sameness” in process calculi, in place of syntactic or trace equality.

A space-efficient probabilistic data structure used to test whether an element is a member of a set. It can have false positives but never false negatives, making it useful for applications where approximate membership queries are acceptable.

The ability of a distributed computing system to continue operating correctly even when some of the nodes fail or act maliciously. Named after the Byzantine General’s Problem, it addresses scenarios where components may provide conflicting information to different parts of the system.

A single global description of a multi-party protocol, written from the viewpoint of no participant in particular (“A sends x to B, then B sends y to C”), from which each participant’s local behaviour is derived by endpoint projection. The contrast is with orchestration, where one central component directs the others. Well-formed choreographies yield local processes that are deadlock-free by construction.

A complete subgraph where every pair of vertices is connected by an edge. The Clique problem asks whether a graph contains a clique of size k or larger, which is NP-complete for k ≥ 3.

A proposition is common knowledge in a group when everyone knows it, everyone knows that everyone knows it, and so on through every level of nesting: the infinite conjunction $\varphi \wedge E\varphi \wedge EE\varphi \wedge \dots$ where $E$ means “everyone knows”. The coordinated attack result shows it cannot be attained over unreliable communication, which places a hard ceiling on the guarantees any coordination protocol can offer.

The oldest and most influential task-allocation protocol in multiagent systems: a manager announces a task, contractors evaluate it and bid, the manager awards the task to the best bid, and the contractor reports results, possibly subcontracting in turn. Announcement, bid and award form a small conversation whose structure is independent of how any participant deliberates.

A structural rule that allows you to duplicate an assumption: from $\Gamma, A, A \vdash B$ infer $\Gamma, A \vdash B$. Linear logic removes contraction so resources cannot be copied freely; duplication is only permitted for formulae marked with $!$.

A direct relationship between computer programs and mathematical proofs, where types correspond to logical propositions and programs correspond to proofs. This fundamental connection shows that programming and logic are essentially the same activity.

The decentralised partially observable Markov decision process: several agents share one reward function but each acts on its own local observations, with no free communication. It is the canonical model of optimal cooperative behaviour under uncertainty, and its headline result is negative: solving one is NEXP-complete, a formal proof that fully general decentralised coordination does not scale.

Semantic content a system’s states possess only under an externally supplied interpretation, as opposed to original intentionality, which a system would possess intrinsically. The structure is that of model-theoretic semantics: symbols denote nothing until an interpretation function assigns them denotations. In agent formalisms the interpretation of belief and goal atoms is fixed by the designer, so the formal agent’s intentionality is derived by construction, and the formal theories require nothing stronger to do their work.

In Deleuze and Guattari, the movement by which a component of an assemblage escapes the fixed relations that stabilise it, opening the assemblage to reconfiguration; reterritorialisation is the counter-movement that stabilises new relations. An assemblage is always doing both at once: holding a working shape while parts of it leak toward other arrangements.

In linear logic, duality is given by linear negation $(\cdot)^{\perp}$, which swaps inputs and outputs and exchanges connectives (e.g. $(A \otimes B)^{\perp} = A^{\perp} \mathbin{\parr} B^{\perp}$ and $(A \mathbin{\&} B)^{\perp} = A^{\perp} \oplus B^{\perp}$). Saying one connective is the dual of another means they correspond under this negation.

The modal logic of knowledge: $K_a \varphi$ says agent $a$ knows $\varphi$, interpreted over possible worlds an agent cannot distinguish. Its power in distributed settings comes from nesting: what $a$ knows about what $b$ knows is exactly what protocols manipulate, and coordination requirements can be stated as knowledge conditions that a protocol must establish.

The unary operators $!A$ (“of course”) and $?A$ (“why not”) that reintroduce weakening and contraction in linear logic. They mark formulae as freely copyable or discardable, restoring classical behaviour locally while keeping the surrounding system resource-aware.

Girard’s programme for interpreting proofs not as static objects but as processes of interaction: cut elimination is modelled as information flowing between the components of a proof until a stable result emerges. It gives a mathematical reading of computation as communication from the proof-theory side, and influenced game semantics and optimal reduction in the λ-calculus.

A cycle in a graph that visits every vertex exactly once and returns to the starting vertex. The Hamiltonian Cycle problem asks whether such a cycle exists, which is NP-complete.

A language is homoiconic when its code and data share the same representation. Programs can be read, generated, and manipulated as ordinary data structures using the language’s own tools—macros, pattern matching, and standard library functions all apply directly to source code.

Aboutness: the property of mental states (beliefs, desires, intentions) of being directed at something beyond themselves. Brentano proposed it as the mark of the mental. Not to be confused with “intention” in the everyday sense; a fear or a perception is intentional in this technical sense, because it is of or about something.

Cohen and Levesque’s formalisation of what makes several agents a team: a shared commitment to a goal together with an obligation of mutual belief about its status. An agent that privately discovers the goal is achieved, impossible, or irrelevant may not silently drop it; the theory obliges it to make that discovery mutually believed first. Concrete communication requirements fall out of this single axiom.

A formal system in which all computation is expressed as function abstraction and application. A term is a variable, an abstraction $\lambda x.M$, or an application $M\,N$; computation is β-reduction, substituting an argument for the bound variable. Despite this minimalism it is Turing-complete, and it underlies the theory of functional programming languages.

Girard’s resource-sensitive logic: by removing the structural rules of weakening and contraction, every assumption must be used exactly once, so a proposition behaves as a resource consumed by its use. The familiar connectives split into multiplicative and additive forms, and the exponential $!A$ reintroduces unlimited use where explicitly marked. It is the proof-theoretic setting in which processes, messages and capabilities have their natural logical reading.

The standard model of sequential decision-making under uncertainty: states, actions, transition probabilities and rewards, with the Markov property that the future depends only on the current state. An optimal policy maximises expected cumulative reward. The partially observable variant (POMDP) gives the agent only noisy observations, forcing it to act on beliefs rather than states.

Game theory run in reverse: instead of predicting behaviour within given rules, one designs the rules so that self-interested behaviour produces the outcome the designer wants. The central trick is incentive compatibility, arranging payoffs so that honest reporting is each participant’s best strategy, as in the second-price auction where bidding one’s true value is dominant.

The practice of describing a machine with mental predicates such as belief, goal, or intention. McCarthy’s criterion is informational: the ascription is legitimate when it expresses the same information about the system’s behaviour more compactly than a mechanistic description. In agent logics the ascribed states are modal operators with fixed axiom systems, belief typically as $\mathrm{KD45}$ and knowledge as $\mathrm{S5}$, so the ascription carries formal content independent of any psychological claim.

Algorithmic verification: given a finite model of a system and a property in a temporal (or epistemic, or strategic) logic, exhaustively decide whether the model satisfies the property, returning a counterexample trace when it does not. Unlike testing it covers every execution, and unlike theorem proving it is push-button; the price is the state-explosion problem.

A compilation technique used in languages like Rust where generic functions and types are replaced with concrete implementations for each specific type they’re used with. This enables zero-cost abstractions by eliminating runtime type dispatch.

A system composed of multiple autonomous agents, each pursuing its own goals with only partial knowledge of the whole, that interact by communicating, coordinating and negotiating. The field studies both the internal architecture of an agent (how it decides what to do) and the interaction protocols between agents (how joint behaviour is organised).

The pair of linear connectives that combine resources simultaneously: tensor $\otimes$ and par $\mathbin{\parr}$. Proofs using them consume all the supplied resources in lockstep rather than offering a choice between branches.

A profile of strategies, one per player, from which no player can improve their own payoff by deviating unilaterally. It is the standard prediction of behaviour among self-interested agents and the baseline notion of stability for any coordination scheme: an arrangement that is not an equilibrium relies on agents acting against their own interests to sustain it.

Completeness for non-deterministic exponential time, the class of problems solvable by a non-deterministic machine in time $2^{n^{O(1)}}$. By the time hierarchy theorem NEXP provably exceeds P, so NEXP-complete problems are unconditionally intractable, not merely conjectured so as with NP. A NEXP-completeness result is a proof that no clever algorithm is coming.

A complexity class of decision problems for which no known polynomial-time algorithm exists, but any solution can be verified in polynomial time. A problem is NP-complete if it is both in NP and every problem in NP can be reduced to it in polynomial time.

The multiplicative disjunction of linear logic, written $A \mathbin{\parr} B$. It represents co-availability: a consumer must be ready to interact with either side, and under linear negation it is dual to tensor $\otimes$. Par often models demand-driven or concurrent use of resources.

A bipartite graph of places (holding tokens) and transitions (which fire by consuming tokens from input places and producing them on output places), modelling concurrency, synchronisation and resource contention directly. Workflow nets specialise them to tasks with a start and an end, where soundness, meaning every run can complete and no task is dead, is a decidable property.

The additive disjunction of linear logic, written $A \oplus B$. It expresses external choice where the environment selects which branch is offered. Its dual under linear negation is with: $(A \oplus B)^{\perp} = A^{\perp} \mathbin{\&} B^{\perp}$.

A family of formal languages for modelling concurrent systems as collections of independent processes interacting through message passing. Where the λ-calculus reduces computation to function application, a process calculus reduces it to communication: processes are composed in parallel, synchronise on shared channels, and are compared by their observable behaviour rather than the values they return.

Graphical representations of logical proofs introduced by Girard for linear logic. They eliminate the bureaucratic details of sequential proof trees, revealing the essential geometric structure of logical reasoning. Each proof net is a graph where nodes represent logical connectives and edges represent the flow of logical resources.

Deleuze and Guattari’s figure for structure without hierarchy: a network in which any point can connect to any other, with no root, no privileged level, and no single entry point. Opposed to the tree (arborescence), which subordinates every node to a trunk. A rhizome is mapped rather than traced: the map has multiple entrances and is always being redrawn.

The Boolean Satisfiability Problem: determining whether there exists an assignment of Boolean values to variables that makes a propositional formula evaluate to true. This is the canonical NP-complete problem.

The widening of a restricted name’s scope when that name is sent to a process outside it. The structural congruence rule permits the restriction to move outward past any process not already using the name, so a communication can hand a private channel to a new participant. The name stays restricted throughout: nobody outside the (now larger) scope can use it, which is what makes freshly created names behave as unforgeable capabilities.

A type discipline for communication channels: where an ordinary type constrains a value, a session type prescribes a protocol, the sequence, direction and payload of the messages exchanged over a channel. Well-typed processes are guaranteed to conform to the protocol and, in the classical systems, to be free of communication mismatches and deadlock. Session types grew directly out of the π-calculus, and correspond to linear logic propositions under a Curry-Howard-style interpretation.

Given a universe of elements and a collection of subsets, find the smallest subcollection whose union covers all elements. The Set Cover problem is NP-complete and a fundamental problem in combinatorial optimisation.

The canonical answer to fair division of a coalition’s joint payoff: each player receives their marginal contribution averaged over every possible order in which the coalition could have formed. It is the unique division satisfying a small set of fairness axioms, and reappears wherever contribution must be attributed to members of a group that only produces value together.

The view, from Austin and Searle, that utterances are actions rather than mere descriptions: to promise, request, or declare is to do something with words. Agent communication languages adopted it directly; a message between agents is typed by its illocutionary force (inform, request, propose), which fixes what sending it commits the sender and receiver to.

An equivalence relation, written $\equiv$, identifying process terms that differ only in inessential syntactic arrangement: the order of parallel components, the placement of restrictions, the unfolding of replication. Reduction in the π-calculus is defined up to structural congruence, so terms may be rearranged freely before a communication step is applied.

Modal logic over time: formulae qualify when things hold, with $\square\varphi$ (“always $\varphi$”) and $\lozenge\varphi$ (“eventually $\varphi$”) as the basic operators. Linear-time logics (LTL) quantify over single executions; branching-time logics (CTL) over the tree of possible futures. Safety (“nothing bad ever happens”) and liveness (“something good eventually happens”) properties of concurrent systems are stated in it.

The multiplicative conjunction of linear logic. A proof of $A \otimes B$ delivers both resources together and a proof that uses it must consume both. Under linear negation it is dual to $\mathbin{\parr}$.

A mathematical model of computation that defines an abstract machine which manipulates symbols on a strip of tape according to a table of rules. Despite its simplicity, a Turing machine can simulate the logic of any computer algorithm.

A set of vertices such that every edge in the graph has at least one endpoint in the set. The Vertex Cover problem asks for the smallest such set, which is NP-complete.

A structural rule that allows you to introduce an unused assumption: from $\Gamma \vdash A$ infer $\Gamma, B \vdash A$. Linear logic drops weakening so resources cannot be discarded unless wrapped in an exponential such as $!A$. This preserves resource-sensitive behaviour.

The additive conjunction of linear logic, written $A \mathbin{\&} B$. It offers both branches internally and the consumer selects which proof to use. Under linear negation it is dual to plus: $(A \mathbin{\&} B)^{\perp} = A^{\perp} \oplus B^{\perp}$. This is often what is meant when someone says “dual with”.