Volition Elicitation: Operational Semantics for People and Their Machines

arXiv:2607.14138 · cs.PL, cs.AI, cs.DC, cs.HC, cs.MA · Submitted 2026-07-10 · Read on arXiv

Listen

Transcript

Introduction to the show: ident: AI Radio. Generated commentary on the latest Artificial Intelligence papers.

Tom: Today's paper: "Volition Elicitation: Operational Semantics for People and Their Machines".

Jane: The gist The most prevalent distributed systems today include people and their personal machines (smartphones), and this paper defines volition-guarded GLP (vGLP) to elicit volitions from a person's head,

Tom: First, who's behind it and why it matters.

Title and authors: Jane: So, what exactly is this paper proposing as its core mechanism? What are they building to solve that manual UI problem?

Tom: They define something new called volition-guarded GLP, or vGLP. It extends the original GLP with these volition-guarded clauses <ref:2607.14138#pg3>. Think of a volition guard as a question, like (Xone=T1,..., Xi=Ti, Y1?,..., Yj?), where Xl are the writers and Yl? are the readers defining the context <ref:2607.14138#pg5>.

Lu: The operational semantics for vGLP are defined as an instance of Communicating Volitional Agents, or CVA <ref:2607.14138#pg5>. This means a volition-guarded clause can only reduce if the person wills that reduction and that will is fulfilled once it’s taken <ref:2607.14138#pg6>.

Meng: So, the core idea is making the machine's behavior conditional on the person's actual will, not just a command being sent to it <ref:2607.14138#pg3>. That sounds like a huge leap from standard programming where input just drives computation.

Jane: It does sound like it, and this leads into how they connect the formal language to what we actually see on a screen. How do you translate this abstract volition guard into something tangible?

Tom: They show that the UI is derived directly from these semantics <ref:2607.14138#pg6>. Specifically, a pending reduction determines the question posed and what answers are awaited, and it looks at sibling clauses where the person chooses <ref:2607.14138#pg6>.

Lalam: The manifest of a vGLP program assigns each volition-guarded clause a specific user interface construct based on its context, the writers of the guard, and buttons labeled by the ground term of its volition guard <ref:2607.14138#pg6>.

The paper's summary: Tom: So if we boil it down, they are proposing this vGLP to give AI a formal foundation so it can systematically develop the UI for those abstract grassroots platforms <ref:2607.14138#pg3>. They want to move away from that ad hoc UI design process entirely.

Jane: The paper summarizes that the goal is to have a single smartphone app, running this GLP engine, that can support multiple different grassroots platforms written in GLP <ref:2607.14138#pg3>. This means we don't need a separate UI for every new platform.

Lu: The paper is focused on getting the formal foundations right for unary volition-guarded transactions <ref:2607.14138#pg5>. They are trying to achieve mathematical elegance and completeness, but more importantly, they want something practical that AI can use to methodically develop the UI <ref:2607.14138#pg3>.

Meng: From a deployment standpoint, this sounds like it could be useful if we’re shipping complex applications where human choice is central, but I have to ask how much overhead this formal layer adds to the runtime <ref:2607.14138#pg6>. What does it cost to run this volition engine on a mobile device?

Tom: They address that with their implementation: they compile vGLP onto GLP, and the volitional layer is implemented on the channel by compilation itself <ref:2607.14138#pg6>. They use a mediator to escrow pending reductions in a pending table rendered as inbox cards <ref:2607.14138#pg6>.

The paper's improvements: Jane: So, what’s the real win here? What did they actually prove that makes this approach better than just guessing how to design a good interface?

Tom: They have some formal guarantees. Theorem five point three proves an elicitation completeness guarantee, which says that for every configuration, a volition over M is offered at p if and only if it is pending at p <ref:2607.14138#pg6>.

Lu: That means the UI will correctly present every choice the person needs to make <ref:2607.14138#pg6>. It formalizes what we mean by eliciting volitions from the person's head <ref:2607.14138#pg3>.

Meng: That sounds promising, but I need more than a proof for me to deploy it. Is there a guarantee on how well this maps to real-world user behavior?

Tom: They have Theorem four point one three, the Realisation theorem, which proves that every CVA platform has a correct implementation by the vmaGLP transition system over P and M with a simple vGLP program <ref:2607.14138#pg6>. It shows that the system is mathematically sound across all configurations <ref:2607.14138#pg6>.

Jane: So, they’re not just giving us a nice idea for design; they’re giving us a formal proof that if we build it this way, the resulting app will correctly implement the transaction defined by the people's wills <ref:2607.14138#pg2>.

Conclusion: Tom: So to wrap up, this paper introduces Volition Elicitation: Operational Semantics for People and Their Machines as a way to formally design user interfaces that can elicit volitions from people's heads <ref:2607.14138#pg3>. The key is defining vGLP and its operational semantics within CVA <ref:2607.14138#pg5>.

Jane: It seems the big implication is that AI can move from just processing inputs to actively designing interactions based on these formal rules, rather than relying on manual guesswork for every single platform <ref:2607.14138#pg4>.

Lu: The paper sets up the framework for taking abstract specifications and systematically deriving deployable apps from them, which is a major step in bridging the gap between high-level logic and user experience <ref:2607.14138#pg6>.

Meng: From my side, it suggests a way to standardize how we define what a 'transaction' means when human choice is involved, so at scale, things don't break because the underlying logic isn't clear <ref:2607.14138#pg6>.

Lalam: I’m fairly sure this direction is where the future of agent systems needs to go because it ties the human element directly into the core transaction structure of what these systems do <ref:2607.14138#pg2>.

Tom: We'll keep an eye on how they implement this on those actual grassroots platforms, which is where we’ll see if they can move from paper to a real working app <ref:2607.14138#pg6>.

London School of Economics · Weizmann Institute of Science

cs.PL, cs.AI, cs.DC, cs.HC, cs.MA

Submitted: 2026-07-10

Updated: 2026-10-15

License: http://creativecommons.org/licenses/by-nc-nd/4.0/

Importance score: 82/100

The gist: The gist The most prevalent distributed systems today include people and their personal machines (smartphones), and this paper defines volition-guarded GLP (vGLP) to elicit volitions from a person's

Key concepts

Volition-Guarded Multiagent Atomic Transactions: This is an abstract language for systems where actions are driven by people's will, like making a payment or befriending someone. A transaction succeeds only if both the machine states and the personal desires (volitions) of all participating agents are met.
Volition-Guarded GLP (vGLP): This is an extension of standard logic programming that incorporates 'volitional procedures.' These procedures pose interactive questions to a person, whose answers determine the next step in the program's execution. The goal is to make formal specifications interactive.
Communicating Volitional Agents (CVA): CVA defines how volitional agents interact. In this context, a volition-guarded clause can only be executed if the person wills it, and once willed, that volition is fulfilled. This operational semantics ensures that the system correctly models human choice within the computation.

Summary

The gist The most prevalent distributed systems today include people and their personal machines (smartphones), and this paper defines volition-guarded GLP (vGLP) to elicit volitions from a person's head, which is necessary for designing user interfaces that correctly implement abstract specifications of grassroots platforms<ref:2607.14138#pg6>.

Volition-Guarded Multiagent Atomic Transactions

Volition-guarded multiagent atomic transactions were proposed as an abstract specification language for systems where computations are driven by people’s volitions, such as a payment or befriending action<ref:2607.14138#pg2>. Each agent consists of a person and their machine, and a transaction can be guarded by both the machine states and the personal volitions of its participating agents<ref:2607.14138#pg3>. For example, child-safe online befriending is guarded by the volitions of the two children and one parent of each, and by the machines not recording them as friends<ref:2607.14138#pg6>. These transactions condition machine transitions on persons’ volitions, occurring only if their will is part of the person’s volitional state<ref:2607.14138#pg3>.

Grassroots Platforms and AI Derivation

A grassroots platform is practically a smartphone app with the ability to operate independently while interoperating, envisioned as an egalitarian alternative to dominant global platforms<ref:2607.14138#pg6>. To facilitate the use of AI to derive these platforms from abstract specifications, Grassroots Logic Programs (GLP) were designed, but AI implementations often required ad-hoc UI design because specifying the role of people in such formalisms was out-of-reach<ref:2607.14138#pg4>. The goal is to rationalize the design of a UI that can elicit volitions from the person’s head when needed<ref:2607.14138#pg3>.

Volition-Guarded GLP (vGLP) and Operational Semantics

The paper defines volition-guarded GLP (vGLP), which extends GLP with volition-guarded clauses, and defines its operational semantics as an instance of Communicating Volitional Agents (CVA)<ref:2607.14138#pg5>. A volition guard has the form of a question, e.g., (X1=T1,..., Xi=Ti, Y1?,..., Yj?), where Xl are writers and Yl? are readers defining the context<ref:2607.14138#pg5>. The operational semantics of vGLP is defined as an instance of CVA where a volition-guarded clause is reducible only if the person wills the reduction, and the willed volition is fulfilled once it is taken<ref:2607.14138#pg6>.

Elicitation and User Interface Derivation

The UI is derived from the semantics: a pending reduction determines the question posed, its answers awaited, and its sibling clauses among which the person chooses<ref:2607.14138#pg6>. The manifest of a vGLP program assigns each volition-guarded clause a user-interface construct based on its context, fields (the writers of the guard), and buttons labeled by the ground term of its volition guard<ref:2607.14138#pg6>. Theorem 5.3 proves that in every configuration, a volition over M is offered at p iff it is pending at p<ref:2607.14138#pg6>.

Implementation and Realisation

The implementation compiles vGLP onto GLP, where the volitional layer is implemented on the channel by compilation, and a mediator escrows pending reductions in a pending table rendered as inbox cards<ref:2607.14138#pg6>. The canonical realisation of a CVA platform is defined by procedures for the state server, request procedure, router, and responder procedure<ref:2607.14138#pg6>. Theorem 4.13 proves that every CVA platform has a correct implementation by the vmaGLP transition system over P and M with a simple vGLP program<ref:2607.14138#pg6>.

Grassroots Platforms Realisations

The paper demonstrates the approach on the grassroots social graph, social network, and currencies: each platform is a vGLP program generated by AI from volition-guarded multiagent atomic transactions<ref:2607.14138#pg6>. The grassroots app is the working smartphone app that renders these platforms as three panels—Friends, Chats, and Coins—each reached by a bottom-bar icon badged with its pending asks<ref:2607.14138#pg6>.

Conclusion

The approach yields a single working app deployed on a physical smartphone where the interface is derived from the semantics rather than designed<ref:2607.14138#pg6>. The paper claims that the composite realizes the compilation, with a tap or submission being a grant and cancel withholding it<ref:2607.14138#pg6>.

Future Work

Future work includes native support for the volitional runtime in the GLP engine, retiring the perplatform mediator, developing a vGLP-to-GLP compiler to replace manual compilation, and exploring standing volitions where a person wills a class of goals rather than one reduction<ref:2607.14138#pg6>.

References

[1] Marc Abrams, Constantinos Phanouriou, Alan L. Batongbacal, Stephen M. Williams, and Jonathan E. Shuster 2607.141385

[2] Pierre A. Akiki, Arosha K. Bandara, and Yijun Yu Adaptive model-driven user interface development systems 2607.141385

[3] Gérard Berry and Georges Gonthier The Esterel synchronous programming language Design, semantics, implementation 2607.141385

[4] Gaëlle Calvary, Joëlle Coutaz, David Thevenin Quentin Limbourg Laurent Bouillon and Jean Vanderdonckt A unifying reference framework for multi-target user interfaces 2607.141385

[5] Stuart K. Card Thomas P. Moran and Allen Newell The keystroke-level model for user performance time with interactive systems 2607.141385

[6] Stuart K. Card Thomas P. Moran and Allen Newell The Psychology of Human-Computer Interaction Lawrence Erlbaum Associates 2607.141385

[7] Mats Carlsson and Thomas Hallgren FUDGETS A graphical user interface in a lazy functional language 2607.141385

[8] Flaviu Cristian Houtan Aghili Ray Strong and Danny Dolev Atomic broadcast From simple message diffusion to byzantine agreement 2607.141385

[9] Evan Czaplicki and Stephen Chong Asynchronous functional reactive programming for GUIs 2607.141385

[10] Alan J. Dix Formal Methods for Interactive Systems Computers and People Series Academic Press 2607.141385

[11] David J. Duke and Michael D. Harrison Abstract interaction objects Computer Graphics Forum 2607.141385

[12] Conal Elliott and Paul Hudak Functional reactive animation In Proceedings of the 2nd ACM SIGPLAN International Conference on Functional Programming 2607.141385

[13] David Harel Statecharts A visual formalism for complex systems Science of Computer Programming 2607.141385

[14] J. M. E. Hyland and C.-H. Luke Ong On full abstraction for PCF I, II, and III Information and Computation 2607.141385

[15] Bonnie E. John David E. Kieras The GOMS family of user interface analysis techniques Comparison and contrast ACM Transactions on Computer-Human Interaction 2607.141385

[16] Neelakantan R. Krishnaswami and Nick Benton A semantic model for graphical user interfaces In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming 2607.141385

[17] Andrew Lewis-Pye Oded Naor and Ehud Shapiro Grassroots flash A payment system for grassroots cryptocurrencies arXiv preprint arXiv:2309.13191 2607.141385

[18] Andy Lewis-Pye and Ehud Shapiro Volitional multiagent atomic transactions Describing people and their machines arXiv preprint arXiv:2604.25596 2607.141385

[19] Quentin Limbourg Jean Vanderdonckt Benoît Michotte Laurent Bouillon and Víctor López-Jaquero USIXML A language supporting multi-path development of user interfaces In Engineering Human Computer Interaction and Interactive Systems EHCI-DSVIS volume 3425 of LNCS Springer 2607.

Improvements for AI systems

Bold header: Eliciting Volitions for Action

This capability allows AI systems to derive a user-interface construct from semantics, as the interface is derived from the semantics rather than from the application’s data or tasks. This means an AI can automatically design and implement a UI that elicits the necessary volitions, transforming abstract specifications into deployable applications.

Bold header: Formalizing Human Input as Guarded Reductions

The system conditions machine steps on a person’s volition, where a volition-guarded reduction is reducible only at their person’s will. This allows AI to model human choice not as a simple command, but as a guarded condition, ensuring that an action only proceeds when the required human will is expressed.

Bold header: Automated UI Derivation from Semantics

The paper proves that the interface is derived from the semantics, mapping each volition-guarded clause to a user-interface construct. This enables AI to automatically generate specific UI elements—such as an inbox card for an arrived offer or a compose form for a persistent request clause—based on the formal requirements of the underlying protocol.

Bold header: Elicitation Completeness Guarantee

The proof of Theorem 5.3 (Elicitation Completeness) ensures that a volition over M is offered at p iff it is pending at p. This provides a formal guarantee that the UI will correctly present all necessary choices to the user, fulfilling the rationale for designing a UI that can elicit volitions from the person’s head.

Bold header: Correct Implementation of Complex Protocols

The system ensures correctness by proving, Theorem 4.13 (Realisation), that Every CVA platform has, for every P ⊂ Π, a correct implementation by the vmaGLP transition system over P and M. This allows AI to generate implementations that are mathematically sound and correctly map every volition-guarded platform transaction realized by a volition-guarded clause.

Abstract

The most prevalent distributed systems today include people and their personal machines (smartphones), and computations in them are driven by people's volitions. Volition-guarded multiagent atomic transactions were proposed as an abstract specification language for such systems, in which a transaction has a precondition on the machine states of its participants and is guarded by the volitions of some of them. Here we develop an abstraction cascade that derives smartphone apps from such specifications and prove it correct down to the base programming language, GLP. The cascade consists of: (1) communicating volitional agents (CVA), which implement every local volition-guarded specification with simple guards, correctly, and completely for its strongly fair runs, by two-phase commit coordinated by the initiating agent; (2) volition-guarded GLP (vGLP), an extension of GLP with volitional procedures, whose goals put an interactively-typed question to the person, into which that implementation compiles; and (3) GLP, which implements vGLP by eliciting the person's answers through the widgets of their interactive types, correctly, and completely for complete widgets. We demonstrate the approach on three grassroots platforms --- a social graph, a social network, and currencies: a compiler carries the social graph and the currencies down the cascade to GLP programs that run with scripted persons, and earlier programs of the three run as mini-apps of one smartphone app.