1 Introduction↩︎

Volition-guarded multiagent atomic transactions. The most prevalent distributed systems today include people and their personal machines (smartphones). In such systems, computations are driven by people’s volitions: a payment when a person wishes to pay someone, befriending when two people wish to become friends, etc. Volition-Guarded Multiagent Atomic Transactions [1] were proposed as an abstract specification language for such systems. In them (i) each agent consists of a person and their machine; (ii) a multiagent atomic transaction can be guarded by both the machine states and the personal volitions of its participating agents. For example, the befriending of two people is guarded by both persons and unfriending by either; a payment is guarded by the payer, a swap by both parties. An illustrative example is child-safe online befriending [2]: it is guarded by the volitions of the two children and one parent of each, and by the machines not recording the two children as friends and recording the two parents as friends.

Previous work [1] presented volition-guarded specifications for the grassroots social graph, grassroots social network [3], and grassroots currencies [4], [5], as well as their implementations via Communicating Volitional Agents, an implementation-ready restriction of the general model in which the only non-unary transactions are the binary discovery of one agent by another and the volition-free binary transfer of a message from the sender to its recipient. Volition-guarded transactions thus condition machine transitions on persons’ volitions. Formally, such a transition can occur only if the will for it is part of the volitional state of the person, namely is in the person’s head. Given today’s technologies, the only way for a machine to know what’s in a person’s head is for the person to express it; this is the fundamental reason for a UI. The goal of this paper is to rationalise the design of a UI that can elicit volitions from the person’s head, when needed.

Existing programming languages treat the person as a source of input — a stream of clicks [6]–[9], an event [10]–[13], the environment [14]–[16] — so input drives computation, but no step of any semantics awaits a person’s will (Section 8).

Communicating Volitional Agents. Implementing a multiagent atomic transactions-based specification must go through unary transactions, carried out by each agent. In the case of such volition-guarded transactions, the corresponding implementation-ready model is called Communicating Volitional Agents (CVA) [1]. Mathematically, CVA is but a restriction of the general model: It has unary volition-guarded transactions, in which a machine carries out a transaction — offering friendship or accepting a friendship offer, sending a payment — when, and only when, its person is willing. Unary transactions may also be unguarded, for example accepting a received valid payment. The machine state of an agent includes an inbox and an outbox, and an agent placing in its outbox a message addressed to another agent is a unary transaction. A message in the outbox of the sender is transferred to the inbox of the addressee by a binary atomic transaction unguarded by volitions. The other CVA binary transaction is discovery, by which one agent gets to know of another. When realising CVA on a smartphone, the basic requirement from the smartphone UI is one: to elicit, from the person operating the smartphone, the volitions the transactions require.

Grassroots platforms. Abstractly, a distributed system is grassroots [17]–[19] if it can have multiple instances that (1) can operate independently of each other and of any global resource other than the net, and (2) may interoperate and coalesce into ever-larger instances. Practically, a grassroots platform is a smartphone app with these two properties (while making some concessions in order to communicate through NATs and firewalls). Grassroots platforms are envisioned as an egalitarian/democratic alternative to the dominant centralised/autocratic (Facebook) and decentralised/plutocratic (Bitcoin) global platforms [20], [21].

Example: Volition-guarded atomic child-safe befriending [2]. Child-safe befriending extends the grassroots social graph [3], the foundational grassroots platform on which all other grassroots platforms are built. The machine state of each agent \(a\) is a set of friends \(c_a\subseteq \Pi\); \(c'_a\) is the machine state of \(a\) after the transaction is carried out; \(r\), \(s\) are children with respective parents \(p\), \(q\), where \(r,s,p,q\) are four distinct agents with the stated precondition.

The preconditions \(q\in c_p\) and \(s\notin c_r\) state that the parents are friends and the children are not. Child befriending requires all four—both children and both parents—to be willing; child unfriending can be initiated by any one of the four.

Grassroots Logic Programs (GLP) and AI. For AI to derive smartphone-based grassroots platforms from such abstract specifications, Grassroots Logic Programs (GLP) [22]–[24], a high-level, typed, multiagent, concurrent programming language, was designed and implemented by AI in Dart/Flutter, which is deployable on most smartphones (iPhone/Android). So far, AI derived GLP implementations of these platforms from (volition-free) multiagent atomic transactions [18]. However, specifying the role of people in such platforms is out-of-reach for this formalism, and hence the key step of designing and implementing the app’s UI was an ad hoc, “manual” process.

To rectify that, we need formal foundations for the implementation of unary volition-guarded transactions, not only for attaining mathematical elegance and completeness, but, more pragmatically, for AI to methodically develop the volition-eliciting UI for abstractly-specified grassroots platforms. Moreover, we wish for a single smartphone app, running the GLP engine, to support multiple, dynamically-loaded grassroots platforms written in GLP, and for that we cannot have an ad-hoc UI for each new platform.

Volition-guarded GLP. In this paper, we aim to achieve all that: We define the programming language volition-guarded GLP (vGLP), which extends GLP with volition-guarded clauses. A volition guard has the form *(\(X_1{=}T_1,\ldots,X_i{=}T_i,\,Y_1?,\ldots,Y_j?\)), declaring the question \(X_1,\ldots,X_i\), with \(T_1,\ldots,T_i\) constraining the answers for which this clause is applicable, and the context \(Y_1?,\ldots,Y_j?\), the values of which define the context in which the question is asked.

Three clauses of the deployed coins-among-friends agent (Section 6) preview the language. The first, tail-recursive, lets the person mint their own coins at any time, the person supplying K; the second and third are the accept and decline clauses of a responder goal, spawned per arriving friend offer, by which the person answers it:

*(K)
agent(Id, UserIn, NetIn, Outs, Holdings) :-
    ground(Id?), integer(K?) |
    add_coin(Id?, K?, Holdings?, Holdings1),
    after_change(Id?, Holdings1?, UserIn?, NetIn?, Outs?).

*(Answer=yes, From?)
respond_coldcall(offer(From), Resp?,
    [decision(Answer?, From?, response(Resp))]) :-
    ground(From?) | true.
*(Answer=no, From?)
respond_coldcall(offer(From), Resp?,
    [decision(Answer?, From?, response(Resp))]) :-
    ground(From?) | true.

The first clause is reducible whenever the person wills a mint, the willed volition supplying K — a question expecting any answer; fulfilled by the reduction, it re-arises with the tail-recursive call, so the interface renders it as a persistent compose form. The accept and decline clauses are reducible only while the offer awaits its answer, each by its own answer, yes or no, binding Answer, the context reader From? identifying the offer — rendered as one inbox card, its buttons those two answers.

Volition-guarded GLP as an instance of Communicating Volitional Agents. We then define the operational semantics of vGLP as an instance of CVA: each agent pairs the person’s volitional state with the machine’s resolvent; a volition-guarded clause is reducible only if the person wills the reduction; the willed volition is fulfilled once the reduction is taken; and the person’s change-volition transitions are their own, carrying no liveness obligation. We prove that on programs with no volition-guarded clauses the semantics coincides with GLP’s (conservativity), and that every volition-guarded reduction fulfils a volition its person expressed (volitional soundness).

Since a volition-guarded reduction requires the person’s will, a correct implementation must elicit the person’s volitions; this is the reason for the UI. We derive the UI from the semantics: a pending reduction determines the question posed, the answers awaited, and the sibling clauses among which the person chooses. The manifest of a program assigns each volition-guarded clause a user-interface construct: its content the context, its fields the question, its buttons the siblings. We prove that the constructs offer exactly the pending volitions (elicitation completeness). A clause posing the empty question yields a compose form, persistent when tail-recursive; a clause posing an arrived offer yields an inbox card, answered by its buttons. The implementation compiles vGLP onto GLP: the vGLP agent is compiled into a GLP agent and a mediator that escrows the pending reductions, and the UI constructs perform the person’s grants. We prove that the compilation correctly implements vcGLP. We also prove that every CVA platform (Section 2.5) can be realised by a vGLP program.

We demonstrate the approach on the grassroots social graph, grassroots social network, and grassroots currencies: each platform is a vGLP program, generated by AI from volition-guarded multiagent atomic transactions. The implementation of vGLP, also created by AI, then maps its volition-guarded clauses into the user-interface constructs, resulting in a single working app deployed on a physical smartphone (Section 7).

Paper outline. Section 2 recalls volition-guarded multiagent atomic transactions, transition systems, implementations, grassroots protocols, and CVA. Section 3 recalls GLP and its multiagent operational semantics maGLP. Section 4 defines vGLP and its operational semantics vmaGLP, with conservativity, volitional soundness, liveness of simple programs, and realisation. Section 5 derives the interaction primitives, proves elicitation completeness, defines the manifest and the compilation of vGLP onto GLP, and proves that the compilation correctly implements vcGLP. Section 6 presents the three platforms as volition-guarded transactions, communicating volitional agents, and vGLP programs, with the before and after of each compilation. Section 7 demonstrates the approach. Section 8 reviews related work, and Section 9 concludes.

2 Volition-Guarded Multiagent Atomic Transactions↩︎

This section recalls the mathematical foundations on which the paper is based [1], [25]. Each agent consists of a person and a machine (e.g., smartphone) operated by the person. A machine transaction specifies what machines do; a volition guard specifies which persons must be willing for the transaction to occur.

We assume a potentially infinite set of agents \(\Pi\), but consider only finite subsets of it, so we assume any particular set of agents \(P \subset \Pi\) to be nonempty and finite. We use \(\subset\) to denote the strict subset relation and \(\subseteq\) when equality is also possible. As standard, we use \(S^P\) to denote the set of all total functions from \(P\) to \(S\), and if \(c\in S^P\) we use \(c_p\) to denote the value of \(c\) at \(p\in P\).

2.1 Volition-Guarded Transactions↩︎

Machine transactions are atomic and asynchronous [25]—they can be carried out by their participants at any time, regardless of the states of non-participants. Participants include both active agents (whose state changes) and stationary agents (whose state is a precondition but does not change). Volition-guarded transactions are machine transactions that can be carried out only if their guards \(Q'\subseteq Q\) are willing. When we say a transaction is “guarded by \(\{p,q\}\),” both must be willing; when we say it is “guarded by either \(p\) or \(q\),” we mean there are two volition-guarded transactions over the same machine transaction, \((t,\{p\})\) and \((t,\{q\})\), so that either person’s volition suffices. Distinct machine transactions can represent “the same action” in different configurations, captured by an equivalence relation on machine transactions.

A person’s volitional state is a set of equivalence classes of machine transactions they are willing their machine to participate in.

A volition-guarded transaction with an empty guard (\(Q' = \emptyset\)) — an unguarded transaction — requires no volitions and is enabled whenever its machine precondition is met.

When a volitional machine transaction induced by \((t,Q')\) is taken, the class \([t]\) is removed from every agent’s volitional state: the will is fulfilled by any equivalent transaction. A person may independently change their volitional state via change-volition transactions, which may add or remove classes; beyond these, the framework removes a class from \(c^v_p\) only upon fulfilment.

2.2 Transition Systems↩︎

A partial equivalence, rather than a total one, is used so that some transitions may carry no liveness requirement: only transitions in the domain of \({\sim}\) form classes and thereby incur a liveness obligation, while transitions outside the domain — belonging to no class — may occur in a correct run but are never required to.

Rather than specifying a multiagent transition system directly, we specify it via transactions, each over its own participants; the closure operator induces from them transitions over a fixed \(P\), in which non-participants are stationary.

If distinct transactions in \(R\) have disjoint \(P\)-closures — as when every participant of every transaction in \(R\) changes state — then each transition in \(R{\uparrow}P\) has a unique inducing transaction, \({\sim}{\uparrow}P\) relates two transitions exactly when their inducing transactions are related, and \({\sim}{\uparrow}P\) is a partial equivalence whenever \({\sim}\) is.

A set of volition-guarded transactions with an equivalence on their underlying machine transactions likewise induces a multiagent transition system, over agent states:

A class of volitional machine transactions is enabled at a configuration in the sense of Definition 6 exactly when some volition-guarded transaction inducing it is enabled in the sense of Definition 4; this determines which runs are live and correct. Unguarded transactions carry the liveness obligation with no volitional prerequisite: once the machine precondition holds, some class representative must eventually be taken. Change-volition transitions impose no liveness obligation; personal choices remain free.

A protocol is a family of multiagent transition systems, one for each finite \(P \subset \Pi\), over a common local-states function assigning to each \(P\) a set of local states containing the initial state [1], [17]. A set of volition-guarded transactions with a transaction equivalence over a local-states function thus defines a protocol: it assigns to each \(P\) the volitional multiagent transition system it induces over \(P\).

2.3 Implementations↩︎

An implementation relates a specification transition system to one that implements it, via a mapping of configurations.

2.4 Grassroots Protocols↩︎

We are particularly interested in  grassroots protocols [1], [17], [18], defined informally as follows. Runs of two disjoint sets can be interleaved into a run of their union. A protocol is oblivious if every interleaving of two correct runs of disjoint sets of agents is a correct run of the union, and interactive if some correct run of the union is not an interleaving of any two such independent runs, because it includes a step whose participants span both sets; it is grassroots if both [1], capturing formally the informal idea that grassroots platforms (specified by grassroots protocols) can have multiple instances that can form and operate independently, yet may coalesce into ever-larger instances, possibly (but not necessarily) into a single global platform.

2.5 Communicating Volitional Agents↩︎

The framework of Section 2 abstracts over how a volition-guarded multiagent atomic transaction is carried out: a \(k\)-ary transaction simultaneously updates the machine states of all its participants, with no notion of how participating machines come to act in concert. An implementation on networked smartphones has no such simultaneity: every exchange between two agents is a separate asynchronous message-passing event, and a \(k\)-ary transaction must be realised by a protocol composed of such events.

To achieve that we recall communicating volitional agents (CVA) [1], an implementation-ready restriction of volition-guarded transactions. CVA volition-guarded machine transactions are drawn from four syntactic forms only: binary discover transactions by which an agent comes to know of another; binary communicate transactions that copy a message from one agent’s outbox to another’s inbox; a unary advance-date transaction by which an agent advances its own local clock; and unary platform transactions. Thus, a CVA platform need only specify its platform transactions. Moreover a CVA protocol is grassroots by construction [1].

Local states. A CVA agent’s local state packages five components: a set of known peers with whom the agent can communicate, an outbox of messages awaiting delivery, an inbox of messages received, a platform state in which each platform specifies whatever data it requires (friend sets, groups, bonds, feeds, and so on), and a local date—a logical clock the agent advances on its own, giving a substrate notion of local time without reference to any global clock. A message is a triple of sender, recipient, and cargo; outboxes and inboxes are sets of messages. The cargo space \(C\) and the platform state space \(A\) are parameters of the CVA platform.

The local-states function \(S\) satisfies \(P\subseteq P' \implies S(P)\subseteq S(P')\), as required of a transactions-based protocol; the added \(\mathbb{N}\) factor is independent of \(P\) and does not affect this.

Volition-guarded transactions. A CVA protocol consists of three “built in” transactions—the binary discover and communicate and the unary advance-date—and platform-specific unary transactions, specified below:

Advance-date is unguarded and always enabled. The local date \(t_p\) is CVA’s only notion of time; timeouts and periodic behaviour are preconditions on it [1]. Being always enabled, Advance-date is excluded from quiescence [1], which would otherwise be unreachable. A platform transaction is reactive if it is unguarded and its precondition requires an arrived message: the machine carries it out on receipt. A reactive transaction reads the inbox but does not consume from it; its precondition is written to fail once the transaction has fired, so a retained message cannot enable it twice. Inboxes only grow; bounding them is left to the implementation.

Distinct CVA transactions have disjoint \(P\)-closures: Communicate changes the state of both its participants, every other form of one, and Discover, Advance-date, and the platform transactions change disjoint components of that state. A CVA platform thus induces over each \(P\subset\Pi\) the volitional multiagent transition system of its transactions (Definition 10), and thereby a protocol (Section 2); its correct runs are those of Definition 6, and the correctness statements of Sections 4 and 5 are over them.

3 GLP↩︎

This section recalls the GLP language and its multiagent operational semantics maGLP [22]; its single-agent case, concurrent GLP (cGLP), is the singleton instance. vGLP (Section 4) extends the language with volition-guarded clauses and maGLP with the volitional layer. While GLP need not be typed, it was augmented with a parameterised moded type system [24], which proved indispensable for AI-based programming.

3.1 GLP Syntax↩︎

GLP extends logic programs by adding a paired reader \(X?\) to every “ordinary” logic variable \(X\), now called a writer.

GLP terms, unit goals, goals, and clauses are as in LP but defined over the variables in \(\hat{\mathcal{V}}\).

Stream(X) ::= [] ; [X|Stream(X)].

procedure merge(Stream(X)?, Stream(X)?, Stream(X)).
merge([X|Xs], Ys, [X?|Zs?]) :- merge(Ys?, Xs?, Zs).
merge(Xs, [Y|Ys], [Y?|Zs?]) :- merge(Xs?, Ys?, Zs).
merge([], Ys, Ys?).
merge(Xs, [], Xs?).

3.2 Goal Reduction↩︎

Guards have three-valued semantics [22]. Each guard predicate explicitly defines its success condition. A guard suspends if it does not succeed but some instance of it under a readers substitution would succeed. A guard fails if no such instance exists. A guard conjunction succeeds if all members succeed; it suspends if any member suspends and none fail; it fails if any member fails. Definition 20 is augmented to succeed if the guard also succeeds. Guard occurrences count toward SRSW satisfaction, and a guard whose success implies that \(X?\) is ground licenses multiple occurrences of \(X\) and \(X?\) in the clause [22].

3.3 maGLP: Multiagent Operational Semantics↩︎

Each agent’s initial resolvent is the atomic goal agent(ch(_?,_),ch(_?,_)), providing two bidirectional channels: the first to the person operating the machine, the second to the network [22]. Anonymous variables make the initial local states syntactically identical yet semantically unshared; variable pairs whose writer and reader are held by different agents are the communication channels, and Cold-call bootstraps shared variables between previously-disconnected agents through the network streams [22].

Reduce differs from LP in the use of a writer mgu instead of a regular mgu, and in the choice of the first applicable clause instead of any clause; Communicate communicates an assignment from its writer to its paired reader — within one agent, or across the two agents holding the pair’s two sides; Cold-call transfers a term with its variables through the network streams, creating paired variables between previously-disconnected agents [22]. Distinct maGLP transactions have disjoint \(P\)-closures — every participant of each changes state — so \({\sim}{\uparrow}P\) is an equivalence (Definition 8). The transition equivalence is total, so every transition carries a liveness obligation; in vGLP (Section 4), the person’s Change-Volition transitions lie outside the domain of the equivalence. Implementation-wise, if a GLP goal \(A\) cannot be reduced now, but there is a readers substitution under which it can, the goal suspends on these readers and is rescheduled once any of them is assigned.

4 Volition-Guarded GLP↩︎

Here we define volition-guarded GLP (vGLP). Syntactically, it extends GLP clauses with an optional volition guard. Semantically, it assumes volitional agents and thus we define its operational semantics as an instance of CVA.

4.1 Syntax↩︎

Here are vGLP code fragments used in this paper:

*(Friend, Coin, Amt)
agent(Id, UserIn, NetIn, Outs, Holdings) :-
    ground(Friend?), ground(Coin?), integer(Amt?) |
    sub_coin(Coin?, Amt?, Holdings?, Status, Holdings1),
    do_pay(Status?, Id?, Friend?, Coin?, Amt?, Holdings1?,
           UserIn?, NetIn?, Outs?).

agent(Id, UserIn, [msg(Id1, intro(From, Resp?))|NetIn],
      Outs, Holdings) :-
    Id? =?= Id1? |
    respond_coldcall(offer(From?), Resp, Ans),
    merge(Ans?, UserIn?, UserIn1),
    agent(Id?, UserIn1?, NetIn?, Outs?, Holdings?).

*(Answer=yes, From?)
respond_coldcall(offer(From), Resp?,
    [decision(Answer?, From?, response(Resp))]) :-
    ground(From?) | true.

4.2 Operational Semantics↩︎

Here we define vmaGLP, the operational semantics of vGLP, which both extends maGLP (Section 3), the multiagent operational semantics of GLP, and is an instance of CVA (Section 2.5).

Reduce alone reads the volitional state and, when the selected clause is volition-guarded, fulfils a volition. Definition 24 applies to vmaGLP runs verbatim, Change-Volition leaving the resolvent unchanged.

Change-Volition transactions are the person’s own: the program reads \(V_p\) only through volition-guarded reductions, and the person performs every change to it. Lying outside the domain of the equivalence, they carry no liveness obligation: the machine cannot compel the person. A volition is fulfilled by the reduction it authorises and is retractable by Change-Volition until fulfilled, as in volitional multiagent atomic transactions (Section 2). The willed volition names its clause, so sibling volition-guarded clauses of the same goal — accept and decline — are the person’s choice: the unwilled sibling suspends, blocking a later otherwise, while a later ordinary clause that succeeds may fire.

Cold-call requires two agents, so vcGLP has Reduce, Communicate, and Change-Volition only; it adds the volitional layer to the single-agent case of maGLP, and is the specification the compilation of Section 5 implements.

A pending clause is a question the machine puts to its person: do you will this reduction? The person answers by a Change-Volition adding a pending volition — its \(\theta\) the person inputs they supply. How questions reach the screen and answers return is the interface’s task (Section 5).

4.3 Conservativity, Volitional Soundness, and Liveness↩︎

The proof is in Appendix C of the supplementary material.

A willed reduction is not, in general, eventually taken: the first clause whose reduction succeeds is selected, so textually earlier clauses can preempt a willed clause indefinitely. In the following syntactic class, only preceding unit clauses and willed siblings can.

The proof is in Appendix C of the supplementary material.

4.4 Realisation of Volition-Guarded Specifications↩︎

A volition-guarded specification (Section 2) is decomposed by CVA (Section 2.5) into its built-in transactions — Discover, Communicate, Advance-date — and unary platform transactions, each guarded by \(\emptyset\) or by the acting agent’s person. Each maps to a clause of the agent’s vGLP program: a transaction with guard \(\emptyset\) to an ordinary clause; one with guard \(\{p\}\) to a volition-guarded clause — its parameters the person inputs; its context readers none when its precondition reads the local state, and the arrived message’s variables when it requires one; and Communicate to the transfer of a message from its sender to its recipient. The correctness statement uses the implementation framework of Section 2.

The construction — one simple procedure per platform transaction, so that Theorem [thm:simple-liveness] carries CVA’s liveness obligation — and the proof are in Appendix C of the supplementary material.

5 Elicitation: The Interaction Primitives↩︎

Formally, the person’s volitions are in \(V_p\), which the machine cannot read. Implementation therefore requires elicitation: offering the person the means to express volitions the machine needs to know in order to fulfil them. Here we describe how this can be done, methodically.

5.1 The Volition Elicitation Construct↩︎

Two extremes of the construct are the interface’s stock elements, and we name the clauses after them, informally. A request clause poses the empty question and expects any answer: its construct is all fields and one button — a compose form — and the volition originates with the person, who supplies the transaction’s parameters — mint, pay, post, offer friendship. A respond clause poses an arrived offer: its construct carries the offer as content and the siblings’ answers — accept and decline — as buttons — an inbox card — and the person answers. In the platforms every volition-guarded clause is one of the two: a clause of the agent procedure, perpetually pending — its guards range over the person inputs and the groundness of the goal’s own arguments, so every quiescent agent state satisfies them, with state dispatch in the body — or a clause of a responder, spawned per arriving offer (Section 4), pending exactly while the offer awaits its answer.

The proof is in Appendix C of the supplementary material.

5.2 Implementation: Elicitation as User-Interface Constructs↩︎

GLP’s semantics gives the person channel (Section 3) no interpretation; vGLP supplies it: the volition-guarded clauses are where the person enters the language. An implementation must therefore map the volition-guarded clauses into concrete user-interface constructs. Pragmatically, the constructs are rather standard [10], [11]:

• a pending reduction of a respond clause — an inbox card carrying the offer, its buttons the siblings’ answers;

• a request clause, perpetually pending — a compose form collecting the person inputs, through its fields or through the selection that opens it;

• a Change-Volition adding a volition — the person’s tap; removing one — cancel;

• the fulfilment of a volition by its reduction — the card’s removal;

• outcomes and state — ordinary output streams to the screen, the classic stream I/O of concurrent logic programming, a chat list or balance kept live as a stream read.

How a construct is laid out is pragmatics; its semantic content is the Change-Volition it performs.

5.3 The Implementation: Compiling vGLP onto GLP↩︎

vGLP needs no new machine. GLP already connects the program to the person: each agent’s first channel is to the person operating it; messages flowing toward the person are rendered by the runtime, and the person’s responses flow back as GLP messages [22], [23]. The volitional layer is implemented on that channel by compilation: a vGLP program becomes a GLP program — the agent, its volition-guarded clauses compiled to ordinary clauses receiving commands, and the mediator, escrowing pending reductions — and the person acts through the manifest’s constructs, each performing one grant. We first make the person’s side formal.

A grant is the person’s act: a construct’s tap or submission grants the command term it carries. Grants lie outside the domain of the equivalence. Cancel is local to a construct, so removing Change-Volitions have no image in the implementation, and need none: they carry no liveness obligation. Definitions 24 (proper run) and 33 (correct) apply to GLP with a person verbatim, grants leaving the resolvent unchanged. Each pending volition-guarded clause (Definition 30) is an ask; the asks are rendered per the manifest (Definition 34) — a respond clause’s ask as a card, its offer escrowed under a request identifier, a request clause’s as a form — and the construct’s grant carries the answer or the command; the pending table is in the mediator, not in the program.

The construction — the canonical compilation and its mapping — and the proof are in Appendix C of the supplementary material; the mapping takes a construct’s grant to the Change-Volition adding the willed volition, and the reduction consuming a granted command to the volition-guarded reduction fulfilling its volition.

The multiagent lift. The volitional layer and the compilation are per-agent: no cross-agent transaction reads a volitional state, and the person channel is local to its agent. The compilation therefore applies per agent to the vmaGLP transition system over \(P\) and \(M\), its Communicate and Cold-call transactions carried unchanged by the multiagent GLP runtime [22], [23].

The current implementation. The standard GLP implementation, extended with the two user-interface constructs, realises the compilation today, per platform, with no engine changes and no compiler — each vGLP program is compiled “manually” (by AI) into a GLP agent plus a per-platform mediator: pending reductions escrowed in a pending table under request identifiers, rendered as inbox cards; the person’s answers returned through command constructors routing the escrowed writer back to the agent; volitions fulfilled by construction. The composite — engine, mediator, and the Dart bridge rendering the constructs — is the platform’s implementation of vGLP. The source and its “manual” compilation into an agent and mediator (tested and deployed) exhibit it clause for clause, and Section 6 shows the before and after per platform.

We claim, informally, that the composite realises the compilation. A tap or submission on a construct is a grant: the granted command adds the volition, and cancel withholds it. An ask is an entry in the pending table: the mediator escrows each pending volition-guarded reduction under a request identifier that carries its question. A volition-guarded Reduce is the consumption of the escrowed answer: the command routes the escrowed writer back to the agent, and the clause the person chose reduces. An entry can be consumed only once, since its writer has a single reader.

6 Grassroots Platforms↩︎

This section specifies three grassroots platforms — the grassroots social graph, grassroots social network, and grassroots coins — each as volition-guarded transactions, as communicating volitional agents (Section 2.5), and as a vGLP program with its compilation to the deployed GLP implementation.

Appendix B of the supplementary material exhibits the “manual” compilation, verbatim, on the pay transaction and the swap offer; the full sources will be released in a public repository once the paper is deanonymised.

6.1 Grassroots Social Graph↩︎

In a grassroots social network [3], the social graph is stored distributively under the control of the people themselves, with each person storing the local neighbourhood pertaining to them, and no third-party having access unless explicitly granted. Each agent \(p\) maintains, as its local state, a finite set \(c_p\subseteq P\) recording the friends of \(p\); initially \(c_p = \emptyset\). Befriending adds \(q\) to \(c_p\) and \(p\) to \(c_q\); unfriending removes them.

For agents \(P \subset \Pi\) with local-states function \(S(P) := 2^P\) and initial state \(c_p := \emptyset\) for all \(p \in P\), the social graph volition-guarded transactions are:

Befriending requires both persons to be willing; unfriending can be initiated by either; an introduction, offered by a common friend \(p\), forms the friendship \(\mathrm{Befriend}(q,r)\) once both \(q\) and \(r\) are willing. The grassroots social graph and social network are introduced and analysed in [1], [3].

CVA realisation. As a CVA platform (Section 2.5), the social graph keeps the friend set \(c_p\) as its platform state and realises Befriend and Unfriend as unary platform transactions over CVA messages. Befriend, guarded in the specification by \(\{p,q\}\), decomposes into an offer by \(p\) and an accept by \(q\); Unfriend, guarded by either, is a single unilateral transaction; an introduction decomposes into an offer by the common friend \(p\) and an acceptance by each of \(q\) and \(r\). Five transactions are volitional — guarded by the acting person, and the volitions the UI elicits — and three are reactive:

The GLP implementation is an agent realising these platform transactions — the introduction’s channel-passing handshake among them (introduce, befriend_intro, accept_intro, reject_intro) — and a mediator, the UI that elicits the volitions. The epoch-encoded friendship lifecycle is given in [1].

vGLP realisation. The correspondence of Theorem [thm:realisation], transaction by transaction: Offer friend is the request clause *(Target); Accept friend the responder pair spawned on the arrived cold call, accept and decline binding the response; End friend the one-way *(Target) — guarded by either party, so no sibling and no decline; Offer introduction the clause *(P,Q); Accept introduction the responder pair spawned on the arrived intro; and the two Integrate transactions ordinary clauses. The vGLP source, “manually” compiled into an agent and mediator (tested and deployed), renders the four request clauses as the compose commands connect, unfriend, send, introduce, and the two responders as inbox cards escrowed under req(N). The introduction, the platform’s richest transaction, is exhibited in Appendix B of the supplementary material.

6.2 Grassroots Social Network↩︎

Groups extend the social network beyond bilateral communication. A group is a set of agents who can all communicate with each other; any agent may create a group. Adding a member requires both the creator and the member to be willing; removing a member or leaving a group can be initiated by either.

Group communication proceeds in two steps: a member posts a message to the group (a unary transaction, guarded by the member), and the message is then delivered to all members (an unguarded transaction).

We extend the grassroots social graph (Definition 37) with group memberships and group communication. Let \(N\) be a set of group names and \(X\) a set of message contents. A group identifier is a pair \(g = (a, n)\) where \(a \in P\) is the creator and \(n \in N\) is the name; we write \(\mathit{cr}(g) = a\) and let \(\mathcal{G}\) denote the set of all group identifiers.

The local state of each agent \(p\) is extended with a finite set \(\mu_p \subseteq \mathcal{G}\) of group memberships, with \(p\) being a member of \(g\) when \(g \in \mu_p\). For each \(g \in \mathcal{G}\), \(p\) also maintains a member output stream \(o_p^g \in (P \times X)^*\), a chat stream \(s_p^g \in (P \times X)^*\), and a delivery index \(\delta_p^g \in \mathbb{N}\). Initially \(\mu_p = \emptyset\), \(\delta_p^g = 0\), and \(o_p^g = s_p^g = \varepsilon\). The friend sets of Definition 37 are unchanged by the transactions below.

The grassroots social network transactions include all social graph transactions of Definition 37, together with the following:

Deliver-to-group is an abstraction of an atomic-broadcast primitive in the sense of [26]: a posted message is appended, by a single unguarded transaction, to the chat stream of every current member of the group.

A public feed created by agent \(a\) is defined to be a group \(g\) with \(\mathit{cr}(g) = a\) in which the post-to-group transaction is restricted to \(p = a\); all other members are followers.

A direct message channel between friends \(p\) and \(q\) is realised by \(p\) creating a group \(g\) with \(\mathit{cr}(g) = p\) and \(q\) joining it; once those transactions have been carried out, the members of \(g\) are \(\{p, q\}\). The guards of the join-group transaction (\(\{p, q\}\)) coincide with the befriend guards.

CVA realisation. The social network adds groups, hosted by their creator and realised as CVA platform transactions. Membership, like befriending, is an offer/accept pair; posting is a unary transaction whose delivery to members is reactive.

A public feed is a group in which only the creator posts, and a direct message channel a two-member group, so both reuse these transactions unchanged. The GLP implementation comprises an agent, the mediator, and the child agent, per the child-safe network [2].

vGLP realisation. The same correspondence carries over: Create group, Offer membership, Post, Leave, and Remove are request clauses *(...); Accept membership is a responder pair spawned on the arrived invite; Distribute and the Integrations are ordinary clauses. The vGLP source’s one-to-one messaging is verified clause for clause against the deployed agent; groups are specified, not yet deployed (Section 7).

6.3 Grassroots Currencies↩︎

Grassroots coins [4], [27] are units of debt that can be issued and traded digitally by any person. Each person’s coins are backed by the goods and services they offer, priced in their own currency, with liquidity arising from mutual credit via coin exchange among persons that know and trust each other. Grassroots bonds [5] extend grassroots coins with a maturity date, reframing grassroots coins—cash—as mature grassroots bonds. Coin-for-bond redemption generalises coin-for-coin redemption, allowing the lending of liquid coins in exchange for interest-bearing future-maturity bonds. Digital social contracts—voluntary agreements among persons, specified, fulfilled, and enforced digitally—can express the full gamut of financial instruments as the voluntary swap of grassroots bonds, including credit lines, loans, sale of debt, forward contracts, options, and escrow-based instruments [5].

The grassroots bonds volition-guarded atomic transactions are:

Minting, paying, and redeeming are guarded by the initiator; voluntary swap requires both parties to be willing; Advance-date is unguarded, since local time advances mechanically. In redemption, the redeemer chooses any bond held by the coin’s issuer—regardless of who issued the bond—generalising coin-for-coin redemption [4] to coin-for-bond redemption [5].

Grassroots coins and bonds are introduced and analysed in [4], [5].

CVA realisation. As a CVA platform (Section 2.5), each agent keeps its bond multiset \(c_p\) and local date \(d_p^*\) as platform state. Minting, paying, and redeeming are unilateral transactions guarded by the initiator; a voluntary swap is an offer/accept pair; advancing the local date is unguarded.

The GLP implementation comprises an agent, a mediator, and actors, with a secure variant. The full secure development is given in [1].

vGLP realisation. Mint, Pay, Redeem, and Propose swap are the request clauses *(K), *(Friend,Coin,Amt) (the worked example of Section 4), *(Friend,Amount), and *(Friend,GiveCoin,GiveAmt,WantCoin,WantAmt); Accept and Decline swap are the responder pair spawned on the arrived swap_propose, its accept declining itself when the want-coins are not held; fills, deliveries, and balances are ordinary clauses. The vGLP source of the coins agent, and its “manual” compilation into an agent and mediator — the worked before-and-after of Sections 4 and 5; its minimal request clause, Mint, is the opening exhibit of Section 1. Both sources place the request clauses last in the agent procedure, after the catch-alls.

7 The Grassroots App↩︎

The grassroots app is the working smartphone app the approach yields: the grassroots social graph, social network, and coins, each a vGLP program “manually” compiled to its agent and mediator (Section 6), rendered by one Dart interpreter as three panels of one app — Friends, Chats, and Coins — each reached by a bottom-bar icon badged with the panel’s pending asks (Figure 1). Every element of every panel is one of the manifest’s constructs (Definition 34): the cards of the platform’s respond clauses, the forms of its request clauses, and the screen (See Appendix B). The deployed build implements the social graph, one-to-one conversations, and coins among friends (Appendix A); groups and bonds, specified in Section 6, add no new constructs and will be implemented shortly.

Friends. The social graph. Its forms are the four request clauses — offer friendship, unfriend, message a friend, introduce two friends; its cards the two sibling pairs — a friend offer and an introduction, each accepted or declined; its screen the friends list, kept by connected, unfriended, and rejected.

Chats. The social network — one-to-one and group messaging, element for element the messaging app people already know (Table 1). The open conversation’s input is the persistent form of the tail-recursive send clause (Remark 2); the chat list and threads are the screen; the panel’s card is a group invitation, accepted before the group joins the chat list. A grassroots machine carries a message only to an established friend, so first contact is gated in Friends: what a commercial messenger lets land unbidden — a stranger’s first message, being added to a group — grassroots holds as a card until the person accepts.

Coins. Grassroots coins among friends (See Appendix A). Its forms are mint, pay, redeem, and propose a swap; its card the proposed swap, accepted or declined; its screen the balances, organised by friend — mutual credit is confined to the social graph, so the wallet lists the person’s friends, each drilling down to the coins they hold.

One interpreter. The manifest is declared in GLP: the compiled form of Definition 34 is the platform’s UserCmd type — one constructor per request clause, and per sibling pair the answers routing its req(N) — and its UserNotify type, the cards and the screen vocabulary. One Dart interpreter renders any manifest: everything crossing to Dart is a ground term or a request identifier; response writers and channels stay escrowed on the GLP side. A new platform declares its two types and gains a panel, an icon, and its alerts, with no platform-specific Dart; the balances view, keyed by holder and coin, is the one generic view coins added, reusable by any balance-bearing platform. The same interpreter, carrying only the platforms’ GLP sources, builds and runs unchanged on the desktop, the iPhone simulator, and the phone: the grassroots app is deployed as a native app on a physical smartphone.

8 Related Work↩︎

vGLP makes two independent contributions: it conditions a machine step on a person’s volition, and it derives the interface from the program’s semantics. The first relates to formal approaches to user interface semantics, in which the person is a source of input, an environment, a chooser, an editor, or a signer; we review these first, by the person’s role. The second relates to work that derives the interface automatically, but from an application’s data, object model, or tasks rather than from a semantics whose steps a person guards; and a further tradition predicts or verifies a given interface. In none does a person’s will guard a transaction, and in none is the interface derived from transaction semantics. Underlying these differences is what a human input is: in the languages that present a program to its user it is a command driving an otherwise-inert tool; in those that generate an interface from data or tasks it is a value completing a task; in vGLP it is a volition authorising an otherwise-ready machine transaction — a guard, not a command or a value.

Formal approaches to user interface semantics. Functional reactive programming gave interaction a denotational semantics with Fran [6]; Fudgets composed graphical interfaces from stream processors in a lazy functional language [7]; Elm gave a GUI language an operational semantics [8]; and Krishnaswami and Benton gave GUIs a denotational model in which the arbitrariness of user input is captured by a nondeterminism monad [9]. Task-oriented programming executes typed editors the person fills: iTasks [10], [28], and its formal core TopHat, whose labelled transitions consume user inputs [11]. iTasks derives those editors generically from the task’s data types, so an interface is derived — but from the data, where the inputs drive the workflow. Game semantics models a program against an Opponent whose strategy is the environment’s [14]; interaction trees represent impure programs whose events the environment answers [15]; interactive computation makes the environment part of the computational model [16]. Formal human-computer interaction modelled interactive systems directly: the PIE model [29], interactors [30], Petri-net interactive cooperative objects [31], statecharts [12], and the synchronous languages [13]. These works give the interface a semantics after it is designed. The concurrent logic languages connected keyboard and screen as stream-processing agents [32]; a message to the person could carry an unbound variable that the person’s response assigns. Ceptre’s interactive stages let the player select which enabled linear-logic rule fires [33]: the person resolves nondeterminism. Hazelnut gives an operational semantics to the person’s edit actions on programs [34]. Smart-contract semantics fire a transition only on a transaction signed by a key [35]. Beliefs, desires, and intentions in agent programming [36] are the software agent’s own, not a person’s, and the human-approval steps of contemporary AI-agent frameworks are architectural practice without semantics.

The interface derived from the program. Deriving the interface from the program, rather than authoring it separately, is an established idea, on bases distinct from ours. Naked objects presents a system’s domain objects directly and creates the interface entirely automatically from their definitions by reflection [37], [38], in a noun-verb style: the person views objects and invokes their methods, with no hand-written presentation layer. Model-based user-interface development derives interfaces from separate task and domain models — the CAMELEON reference framework [39], ConcurTaskTrees and model-based design [40], and description languages such as UIML [41] and UsiXML [42], surveyed in [43]; task-oriented programming (above) derives its editors generically from data types; and structure editors derive an editing interface from a grammar [44]. In each the interface follows from a description of the application’s data, objects, or tasks.

Command, value, or guard. A naked-objects application is a tool: nothing happens without the operator, so the input is the control flow. A task-oriented input is a datum the workflow consumes. vGLP’s reductions proceed on their own; a volition-guarded reduction is ready but withheld: its legitimacy requires the willingness of the party it binds — a transfer the payer’s, a friendship both parties’. Prior work derives the interface so the person can operate the program or supply values to it; vGLP derives it so the person can will its steps.

Predicting and verifying a given interface. Interface design is often treated as a craft outside formal computer science, yet two lines formalise it. Predictive engineering models estimate a design’s performance from the person’s elementary actions — the keystroke-level model and the GOMS family [45]–[47]. Formal methods for interactive systems specify and verify interfaces — from grammars for user interfaces [48] through the collected work of the field [49], [50], of which the dialogue models above are part.

To the best of our knowledge, vGLP is the first programming language whose operational semantics conditions transactions on a person’s volition — elicited, pending until willed, retractable, and fulfilled — with the interface derived from that semantics rather than from the application’s data or tasks.

9 Conclusion↩︎

We incorporated people in the operational semantics of a programming language: vGLP’s volition-guarded clauses are reducible only at their person’s will, the person’s change-volition transitions are their own, and a willed volition is fulfilled once its reduction is taken. The interface is derived from the semantics rather than designed: a program’s questions are its pending volition-guarded reductions, and the manifest reads each clause’s construct off its volition guard — its content the context, its fields the person inputs, its buttons the siblings — a card, a form, the persistent command-line box of a tail-recursive clause. The realisation proceeds from volition-guarded multiagent atomic transactions through communicating volitional agents to vGLP, and by compilation onto GLP with the user-interface constructs to the running grassroots app, deployed on a physical smartphone.

Future work: native support for the volitional runtime in the GLP engine, retiring the per-platform mediator; a vGLP-to-GLP compiler, replacing “manual” (AI) compilation; typed person inputs, subsuming the ground guards on the person’s data; and standing volitions — a person willing a class of goals rather than one reduction.

10 Coins Among Friends↩︎

This appendix gives the restricted model realised by the coins app of Section 7. It is the grassroots coins and bonds protocol \(\mathit{GCB}\) (Definition 42) under two simplifications: (i) drop maturity — there are no bonds, only coins, so the local date and Advance-date play no role; and (ii) confine holdings and transactions to the social graph (Section 6.1) — a person holds and trades only their friends’ coins. The full model, with bonds, maturity, and escrow-based instruments, is in Section 6.3 and [4], [5].

Dropping maturity simplifies Definition 41: every bond is mature, so a \(p\)-bond is simply a \(p\)-coin, denoted \(_p\), a unit of debt issued by \(p\). We let \(\mathcal{C}(P)=\{\text{\textcent}_q : q\in P\}\) be the coins of agents \(P\subset\Pi\). The friends restriction ties the holding graph to the social graph: mutual credit presupposes that the parties know and trust each other [4], and in a grassroots social network that relation is friendship. So the same connection that gates contact (Section 7) gates coin-holding: a person holds and transacts only their friends’ coins, and their own.

The guarded transactions of Section 6.3, restricted to coins among friends:

On redeem, the issuer \(q\) fills automatically [4]. The bond machinery of Section 6.3 — maturity, the local date, and Advance-date — is absent.

These volitions are elicited by the constructs of Section 7 exactly as the other platforms are. Mint, Pay, and Redeem are self-guarded request clauses; a swap is a request on the proposer’s side (Propose) and a respond on the counterparty’s (Accept). Balances are read by a standing request — the bare * balance-report clause of the agent — and rendered as the wallet’s values. The coins app is therefore another instance of the one interface (Section 7): its UserCmd/UserNotify types, declared in its mediator, yield a manifest the same interpreter renders — the test being whether a balance-bearing platform needs only a manifest, or a new generic view.

11 Code Fragments↩︎

This appendix exhibits the vGLP source of the social graph’s introduction, and the manual compilation of Section 5 on two fragments of the deployed sources of the grassroots app, verbatim: the pay transaction — a request clause, elicited by a form — and the swap offer — a respond pair, elicited by a card. Long clause heads are wrapped for the page; the sources are otherwise unchanged. The code appendices are included to preserve anonymity; the final paper will include a pointer to the public repository.

The introduction, a request clause and a respond pair. The social graph’s richest transaction (Section 6.1): the offer clause *(P,Q), the responder spawned on the arrived intro, and its accept and reject siblings:

*(P, Q)
agent(Id, UserIn, NetIn, Outs) :-
    ground(Id?), ground(P?), ground(Q?), ~(P? =?= Q?),
    new_channel(PQCh, QPCh) |
    send_friend(P?, msg(Id?, P?, intro(Q?, QPCh?)), Outs?, Outs1),
    send_friend(Q?, msg(Id?, Q?, intro(P?, PQCh?)), Outs1?, Outs2),
    agent(Id?, UserIn?, NetIn?, Outs2?).

agent(Id, UserIn, [msg(_From, Id1, intro(Other, Ch))|NetIn],
      Outs) :-
    Id? =?= Id1? |
    respond_intro(Id?, offer(Other?), Ch?, Ans),
    merge(Ans?, UserIn?, UserIn1),
    agent(Id?, UserIn1?, NetIn?, Outs?).

*(Answer=yes, Other?)
respond_intro(Id, offer(Other), Ch, Ans?) :-
    ground(Id?), ground(Other?),
    send(ack(Id?), Ch?, Ch1) |
    intro_await_peer(Other?, Ch1?, Result),
    inject_intro_result(Result?, [], Ans).

*(Answer=no, Other?)
respond_intro(_, offer(Other), ch(_ChIn, [nack|[]]), []) :-
    ground(Other?) | true.

Pay, a request clause. The vGLP pay clause is the worked example of Section 4. Its manual compilation: the command constructor pay(Constant, Constant, Integer) of the mediator’s UserCmd type, the mediator pass-through, and the agent clause matching the granted command:

ui_mediator(Id, AgentCh, UserCh, Ps, N) :-
    receive(pay(Friend, Coin, Amount), UserCh?, UserCh1),
    ground(Id?), ground(Friend?), ground(Coin?),
    integer(Amount?) |
    send(msg('_user', Id?, pay(Friend?, Coin?, Amount?)),
         AgentCh?, AgentCh1),
    ui_mediator(Id?, AgentCh1?, UserCh1?, Ps?, N?).

agent(Id, [msg('_user', Id1, pay(Friend, Coin, Amt))|UserIn],
      NetIn, Outs, Holdings) :-
    Id? =?= Id1?, ground(Friend?), ground(Coin?), integer(Amt?) |
    sub_coin(Coin?, Amt?, Holdings?, Status, Holdings1),
    do_pay(Status?, Id?, Friend?, Coin?, Amt?, Holdings1?,
           UserIn?, NetIn?, Outs?).

The swap offer, a respond pair. The arriving proposal spawns a responder carrying the offer and the response writer; the accept sibling injects its answer through the merge, and an ordinary agent clause carries it out on the agent’s current holdings; the decline sibling injects decline_swap:

agent(Id, UserIn,
      [msg(From, Id1, swap_propose(GiveCoin, GiveAmt,
                        WantCoin, WantAmt, SwapResp?))|NetIn],
      Outs, Holdings) :-
    Id? =?= Id1?, ground(From?), ground(GiveCoin?),
    integer(GiveAmt?), ground(WantCoin?), integer(WantAmt?) |
    respond_swap(offer(From?, GiveCoin?, GiveAmt?,
                       WantCoin?, WantAmt?), SwapResp, Ans),
    merge(Ans?, UserIn?, UserIn1),
    agent(Id?, UserIn1?, NetIn?, Outs?, Holdings?).

*(Answer=yes, From?, GiveCoin?, GiveAmt?, WantCoin?, WantAmt?)
respond_swap(offer(From, GiveCoin, GiveAmt,
                   WantCoin, WantAmt), SwapResp?,
    [accept_swap(From?, GiveCoin?, GiveAmt?,
                 WantCoin?, WantAmt?, SwapResp)]) :-
    ground(From?), ground(GiveCoin?), integer(GiveAmt?),
    ground(WantCoin?), integer(WantAmt?) | true.

agent(Id, [accept_swap(From, GiveCoin, GiveAmt, WantCoin,
                       WantAmt, SwapResp?)|UserIn],
      NetIn, Outs, Holdings) :-
    ground(From?), ground(GiveCoin?), integer(GiveAmt?),
    ground(WantCoin?), integer(WantAmt?) |
    sub_coin(WantCoin?, WantAmt?, Holdings?, Status, Holdings1),
    do_accept_swap(Status?, Id?, From?, GiveCoin?, GiveAmt?,
                   Holdings1?, SwapResp, UserIn?, NetIn?, Outs?).

Its manual compilation: the agent forwards the arrived proposal, response writer included, to the mediator; the mediator escrows the writer in the pending table under a fresh req(N) — the card — and the person’s answer routes it back to the agent:

agent(Id, UserIn,
      [msg(From, Id1, swap_propose(GiveCoin, GiveAmt,
                        WantCoin, WantAmt, SwapResp?))|NetIn],
      Outs, Holdings) :-
    Id? =?= Id1?, ground(From?), ground(GiveCoin?),
    integer(GiveAmt?), ground(WantCoin?), integer(WantAmt?) |
    lookup_send('_user',
        msg(agent, '_user', swap_offer(From?, GiveCoin?, GiveAmt?,
                              WantCoin?, WantAmt?, SwapResp)),
        Outs?, Outs1),
    agent(Id?, UserIn?, NetIn?, Outs1?, Holdings?).

ui_mediator(Id, AgentCh, UserCh, Ps, N) :-
    receive(msg(agent, '_user',
                swap_offer(From, GC, GA, WC, WA, Resp?)),
            AgentCh?, AgentCh1),
    ground(From?), ground(GC?), ground(GA?), ground(WC?),
    ground(WA?) |
    send(swap_offer(From?, GC?, GA?, WC?, WA?, req(N?)),
         UserCh?, UserCh1),
    N1 := N? + 1,
    ui_mediator(Id?, AgentCh1?, UserCh1?,
        [pending(req(N?), swap_pending(Resp, GC?, GA?, WC?, WA?))
         | Ps?], N1?).

ui_mediator(Id, AgentCh, UserCh, Ps, N) :-
    receive(accept_swap(From, ReqId), UserCh?, UserCh1),
    ground(Id?), ground(From?), ground(ReqId?) |
    lookup_pending(ReqId?, Pv, Ps?, Ps1),
    send(msg('_user', Id?, accept_swap(From?, Pv?)),
         AgentCh?, AgentCh1),
    ui_mediator(Id?, AgentCh1?, UserCh1?, Ps1?, N?).

12 Proofs↩︎

This appendix proves the theorems of Sections 4 and 5, and gives the canonical realisation and the canonical compilation with their mappings.

The Canonical Realisation↩︎

Fix a CVA platform (Section 2.5). For a platform transaction \(t\) with parameters \(X_1,\ldots,X_k\), write t(X1,...,Xk) for its term, pre_t for the guard testing its precondition, pre'_t for the restriction of that guard to the message and the state, and eff_t for the body kernel performing its effect — updating the state and appending its messages, each addressed by name, to the output stream. The state term s(Known,In,A,T) carries the known peers, the recorded messages, the platform state, and the local date; record(M) is the bookkeeping transaction adding M to In, with precondition true. All goals reach the state server on one merged channel and responder goals read its state stream, each through its own branch; split branches a channel or stream (a merge on the server side, a distributor on the state side, the standard stream techniques [22]), and drain closes a terminating goal’s remaining streams.

Every procedure is simple: a request or responder procedure has one volition-guarded clause, first, and every other procedure is ordinary. Every message on Outs is delivered by Cold-call.

An apply is in flight from the Reduce that sends it until the server Reduce that consumes it; the applies in flight at \(p\) are linearly ordered by their position on the merged server channel. The effective state of \(p\) is the state and output stream obtained from the server’s by serving the applies in flight, in order, per the server clauses.

The Canonical Compilation↩︎

The compilation replaces each volition-guarded clause of the canonical realisation \(M\) by ordinary clauses receiving the person’s granted terms, and adds the mediator. Per request procedure \(t\) its command is c_t(X1,...,Xk); per responder procedure \(t\) its answer is a_t(X1,...,Xk), granted by the person as a_t(X1,...,Xk,ReqId); an offer offer(Q,R) pairs a responder’s question with a fresh answer writer, and a card card(Q,req(N)) carries the question to the person under a request identifier. lookup consumes the pending entry of a request identifier (the deployed lookup_pending, Appendix B), and the body assignment := binds the escrowed writer.

References↩︎