pith. the verified trust layer for science. sign in

arxiv: 2602.06934 · v3 · submitted 2026-02-06 · 💻 cs.PL · cs.AI· cs.DC· cs.LO· cs.MA

Implementing Grassroots Logic Programs with Multiagent Transition Systems and AI

Ehud Shapiro This is my paper

Pith reviewed 2026-05-16 06:08 UTC · model grok-4.3

classification 💻 cs.PL cs.AIcs.DCcs.LOcs.MA
keywords Grassroots Logic ProgramsMultiagent systemsOperational semanticsLogic programmingConcurrent programmingSmartphone applicationsServerless platformsTransition systems
0
0 comments X p. Extension

The pith

Grassroots logic programs can be implemented correctly via deterministic multiagent transition systems using local links for shared variables.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper derives deterministic operational semantics dGLP and madGLP from the abstract nondeterministic semantics GLP and maGLP for Grassroots Logic Programs. It proves the deterministic versions correct with respect to the abstracts by showing that shared variables across agents can be realized as local variable pairs connected by global links. Correctness rests on disjoint substitution commutativity, which follows from the single-occurrence invariant of GLP programs together with substitution persistence. The work also establishes that both maGLP and madGLP satisfy the grassroots property, meaning they can execute in a fully decentralized manner. This supplies a formal basis for building serverless, smartphone-based multiagent platforms directly in languages such as Dart.

Core claim

The paper establishes that madGLP is a correct deterministic implementation of the multiagent abstract semantics maGLP, with shared-variable pairs spanning agents realized as local variable pairs joined by global links; correctness follows from the single-occurrence invariant guaranteeing that disjoint substitutions commute, together with persistence of substitutions, and both maGLP and madGLP are shown to be grassroots.

What carries the argument

Multiagent transition system in which shared variables spanning agents are replaced by local variable pairs connected by global links, justified by disjoint substitution commutativity from the single-occurrence invariant.

If this is right

  • dGLP serves as a formal specification that directly yields a workstation implementation of GLP in Dart.
  • madGLP serves as a formal specification that directly yields a smartphone-based multiagent implementation of GLP in Dart.
  • Because both madGLP and maGLP are grassroots, the resulting programs run without any central server or coordinator.
  • The implementation strategy extends the abstract semantics while preserving all observable behavior under the single-occurrence invariant.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same local-link technique could be applied to other concurrent logic languages to obtain decentralized mobile implementations.
  • Performance measurements on actual smartphone networks would test whether the link overhead remains acceptable under realistic agent counts.
  • The grassroots property opens the possibility of composing multiple independent GLP programs into larger serverless platforms without additional coordination layers.

Load-bearing premise

Every valid GLP program satisfies the single-occurrence invariant, which guarantees that substitutions on disjoint variables commute.

What would settle it

A concrete GLP program containing two agents whose shared variables produce different results under the local-link implementation than under the abstract shared-variable semantics, due to non-commuting substitutions.

read the original abstract

Grassroots Logic Programs (GLP) is a multiagent, concurrent, logic programming language designed for the implementation of smartphone-based, serverless, grassroots platforms. Here, we start from GLP and maGLP -- concurrent and multiagent abstract nondeterministic operational semantics for GLP, respectively -- and from them derive dGLP and madGLP -- implementation-ready deterministic operational semantics for both -- and prove them correct with respect to their abstract counterparts. dGLP was used by AI (Claude) as a formal specification from which it developed a workstation-based implementation of GLP in Dart; madGLP is being used by AI as a formal specification from which it develops a smartphone-based multiagent implementation of GLP in Dart. The key insight is that maGLP shared variable pairs spanning agents can be implemented as local variable pairs connected by global links, with correctness following from disjoint substitution commutativity (from GLP's single-occurrence invariant) and persistence. We prove that both madGLP and maGLP are grassroots.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The paper starts from abstract nondeterministic operational semantics GLP and maGLP for Grassroots Logic Programs and derives deterministic operational semantics dGLP and madGLP. It proves correctness of the deterministic versions with respect to the abstract ones, shows that shared-variable pairs spanning agents can be realized as local pairs plus global links, and proves that both madGLP and maGLP are grassroots. The proofs rely on language invariants (including single-occurrence) and persistence; the deterministic semantics are presented as formal specifications used by AI to generate Dart implementations.

Significance. If the correctness and grassroots proofs hold, the work supplies a rigorous path from abstract multiagent logic-programming semantics to concrete, implementable transition systems suitable for serverless smartphone platforms. The explicit use of AI to produce code from the deterministic semantics is a methodological contribution that could be replicated in other formal-language projects.

major comments (1)
  1. [Proof of madGLP correctness (relative to maGLP)] The correctness argument for madGLP simulating maGLP (and thereby the local-link implementation of shared variables) invokes disjoint substitution commutativity, which is derived from GLP's single-occurrence invariant. No lemma is supplied showing that this invariant is preserved by the madGLP transition rules, in particular the rules that update global links or perform substitutions across agent boundaries. If a reachable madGLP state can violate single-occurrence, commutativity fails and the simulation relation used for correctness does not hold.
minor comments (1)
  1. [Abstract] The abstract states that 'dGLP and madGLP are proved correct' but does not indicate the precise simulation or bisimulation relation employed; a short statement of the relation in the introduction would help readers locate the key technical claim.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments. We address the single major comment below.

read point-by-point responses

  1. Referee: [Proof of madGLP correctness (relative to maGLP)] The correctness argument for madGLP simulating maGLP (and thereby the local-link implementation of shared variables) invokes disjoint substitution commutativity, which is derived from GLP's single-occurrence invariant. No lemma is supplied showing that this invariant is preserved by the madGLP transition rules, in particular the rules that update global links or perform substitutions across agent boundaries. If a reachable madGLP state can violate single-occurrence, commutativity fails and the simulation relation used for correctness does not hold.

    Authors: We agree that an explicit lemma establishing preservation of the single-occurrence invariant under all madGLP rules is required. The revised manuscript will include a new lemma (by induction on the transition rules) proving that single-occurrence is maintained, including for global-link updates and cross-agent substitutions. This lemma will be inserted immediately before the simulation theorem, thereby closing the gap in the correctness argument. revision: yes

Circularity Check

0 steps flagged

No circularity: proofs rely on external language invariants

full rationale

The paper derives dGLP and madGLP from abstract GLP and maGLP, then claims correctness via disjoint substitution commutativity (from the single-occurrence invariant) and persistence. These invariants are presented as properties of the base GLP language, not redefined or fitted from the implementation semantics. No equations or steps reduce the claimed correctness to a self-referential definition, a fitted parameter renamed as prediction, or a self-citation chain that bears the entire load. The derivation is self-contained against the stated invariants and does not exhibit any of the enumerated circular patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claims rest on the single-occurrence invariant of GLP and the persistence of substitutions; no free parameters or new entities are introduced in the abstract.

axioms (2)
  • domain assumption GLP programs satisfy a single-occurrence invariant
    Invoked to justify disjoint substitution commutativity for the shared-variable implementation.
  • domain assumption Substitutions are persistent
    Used together with commutativity to establish correctness of the local-link implementation.

pith-pipeline@v0.9.0 · 5476 in / 1304 out tokens · 59639 ms · 2026-05-16T06:08:04.154394+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

24 extracted references · 24 canonical work pages · 1 internal anchor

  1. [1]

    The existence of refinement mappings.Theoretical Computer Science, 82(2):253–284, 1991.doi:10.1016/0304-3975(91)90224-P

    1 Martín Abadi and Leslie Lamport. The existence of refinement mappings.Theoretical Computer Science, 82(2):253–284, 1991.doi:10.1016/0304-3975(91)90224-P. 2 Paulo Sérgio Almeida and Ehud Shapiro. The blocklace: A byzantine-repelling and universal conflict-free replicated data type.arXiv preprint arXiv:2402.08068,

    work page doi:10.1016/0304-3975(91)90224-p 1991

  2. [2]

    4 Henry G

    doi:10.1145/ 1810891.1810910. 4 Henry G. Baker and Carl Hewitt. The incremental garbage collection of processes. In Proceedings of the 1977 Symposium on Artificial Intelligence and Programming Languages, pages 55–59. ACM, 1977.doi:10.1145/800228.806932. 5 Philip A. Bernstein, Vassos Hadzilacos, and Nathan Goodman.Concurrency Control and Recovery in Databa...

    work page doi:10.1145/800228.806932 1977

  3. [3]

    Statically contextualizing large language models with typed holes

    6 Andrew Blinn, Xiang Li, June Hyung Kim, and Cyrus Omar. Statically contextualizing large language models with typed holes. InProceedings of the ACM on Programming Languages (OOPSLA), volume 8, pages 1–29. ACM, 2024.doi:10.1145/3689746. 7 Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In Proceedings of the 21st Inter...

    work page doi:10.1145/3689746 2024

  4. [4]

    10 Ezra Cooper, Sam Lindley, Philip Wadler, and Jeremy Yallop

    doi:10.1145/2824815.2824816. 10 Ezra Cooper, Sam Lindley, Philip Wadler, and Jeremy Yallop. Links: Web programming without tiers. InProceedings of the 5th International Symposium on Formal Methods for Components and Objects (FMCO), volume 4709 ofLecture Notes in Computer Science, pages 266–296. Springer, 2006.doi:10.1007/978-3-540-74792-5_12. 11 Cormac Fl...

    work page doi:10.1145/2824815.2824816 2006

  5. [5]

    15Google

    doi: 10.1016/0304-3975(87)90045-4. 15Google. Dart programming language.https://dart.dev,

    work page doi:10.1016/0304-3975(87)90045-4

  6. [6]

    Herlihy and Jeannette M

    17 Maurice P. Herlihy and Jeannette M. Wing. Linearizability: A correctness condition for concurrent objects.ACM Transactions on Programming Languages and Systems, 12(3):463– 492, 1990.doi:10.1145/78969.78972. Ehud Shapiro 33 18 Joshua S. Hodas and Dale Miller. Logic programming in a fragment of intuitionistic linear logic.Information and Computation, 110...

    work page doi:10.1145/78969.78972 1990

  7. [7]

    Grassroots flash: A payment system for grassroots cryptocurrencies.arXiv preprint arXiv:2309.13191,

    23 Andrew Lewis-Pye, Oded Naor, and Ehud Shapiro. Grassroots flash: A payment system for grassroots cryptocurrencies.arXiv preprint arXiv:2309.13191,

    work page arXiv

  8. [8]

    Practical type inference based on success typings

    24 Tobias Lindahl and Konstantinos Sagonas. Practical type inference based on success typings. InProceedings of the 8th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP), pages 167–178. ACM, 2006.doi:10.1145/1140335. 1140356. 25 Sam Lindley and J. Garrett Morris. Lightweight functional session types.Behaviou...

    work page doi:10.1145/1140335 2006

  9. [9]

    Lynch and Mark R

    28 Nancy A. Lynch and Mark R. Tuttle. Hierarchical correctness proofs for distributed algorithms. InProceedings of the 6th Annual ACM Symposium on Principles of Distributed Computing (PODC), pages 137–151. ACM, 1987.doi:10.1145/41840.41852. 29 Nancy A. Lynch and Mark R. Tuttle. An introduction to input/output automata. Technical Report MIT/LCS/TM-373, Lab...

    work page doi:10.1145/41840.41852 1987

  10. [10]

    Lynch and Frits W

    30 Nancy A. Lynch and Frits W. Vaandrager. Forward and backward simulations: I. Untimed systems.Information and Computation, 121(2):214–233, 1995.doi:10.1006/inco.1995.1134. 31 NancyA.LynchandFritsW.Vaandrager. Forwardandbackwardsimulations: II.Timing-based systems.Information and Computation, 128(1):1–25, 1996.doi:10.1006/inco.1996.0060. 32 Nicholas D. M...

    work page doi:10.1006/inco.1995.1134 1995

  11. [11]

    36 Rob Pike

    Available athttps://arxiv.org/ abs/2504.09246. 36 Rob Pike. Go at Google: Language design in the service of software engineering. Keynote at SPLASH 2012,

    work page arXiv 2012

  12. [12]

    37 Klaas Pruiksma and Frank Pfenning

    Available athttps://go.dev/talks/2012/splash.article. 37 Klaas Pruiksma and Frank Pfenning. Back to futures.Journal of Functional Programming, 32:e4, 2022.doi:10.1017/S0956796822000016. 34 Implementing Grassroots Logic Programs 38 Davide Sangiorgi. On the bisimulation proof method.Mathematical Structures in Computer Science, 8(5):447–479, 1998.doi:10.1017...

    work page doi:10.1017/s0956796822000016 2012

  13. [13]

    40 Ehud Shapiro

    doi:10.1145/99583.99627. 40 Ehud Shapiro. A subset of concurrent prolog and its interpreter.ICOT Technical Report, TR-003,

    work page doi:10.1145/99583.99627

  14. [14]

    Multiagent transition systems: Protocol-stack mathematics for distributed computing.arXiv preprint arXiv:2112.13650,

    42 Ehud Shapiro. Multiagent transition systems: Protocol-stack mathematics for distributed computing.arXiv preprint arXiv:2112.13650,

    work page arXiv

  15. [15]

    Grassroots distributed systems: Concept, examples, implementation and applications (brief announcement)

    43 Ehud Shapiro. Grassroots distributed systems: Concept, examples, implementation and applications (brief announcement). In37th International Symposium on Distributed Computing (DISC 2023). (Extended version: arXiv:2301.04391), pages 47:1, 47:7, Italy,

    work page arXiv 2023

  16. [16]

    45 Ehud Shapiro

    doi:10.1145/3599696.3612898. 45 Ehud Shapiro. Grassroots currencies: Foundations for grassroots digital economies.arXiv preprint arXiv:2202.05619,

    work page doi:10.1145/3599696.3612898

  17. [17]

    Glp: A grassroots, multiagent, concurrent, logic programming language.arXiv preprint arXiv:2510.15747,

    46 Ehud Shapiro. Glp: A grassroots, multiagent, concurrent, logic programming language.arXiv preprint arXiv:2510.15747,

    work page arXiv

  18. [18]

    doi: 10.1145/3772290.3772309

    arXiv preprint arXiv:2502.11299. doi: 10.1145/3772290.3772309. 49Ehud Shapiro. Types for grassroots logic programs.arXiv preprint arXiv:2601.17957,

    work page doi:10.1145/3772290.3772309

  19. [19]

    Grassroots Federation: Fair Democratic Governance at Scale

    In preparation. 51 Ehud Shapiro and Nimrod Talmon. Grassroots federation: Fair governance of large-scale, decentralized, sovereign digital communities.arXiv preprint arXiv:2505.02208,

    work page internal anchor Pith review Pith/arXiv arXiv

  20. [20]

    Conflict-free replicated data types

    52 Marc Shapiro, Nuno Preguiça, Carlos Baquero, and Marek Zawirski. Conflict-free replicated data types. InStabilization, Safety, and Security of Distributed Systems: 13th International Symposium, SSS 2011, Grenoble, France, October 10-12,

    work page 2011

  21. [21]

    Higher-order processes, functions, and sessions: A monadic integration

    53 Bernardo Toninho, Luís Caires, and Frank Pfenning. Higher-order processes, functions, and sessions: A monadic integration. InProceedings of the 22nd European Symposium on Programming (ESOP), volume 7792 ofLecture Notes in Computer Science, pages 350–369. Springer, 2013.doi:10.1007/978-3-642-37036-6_20. 54 Kazunori Ueda. Guarded horn clauses. InLogic Pr...

    work page doi:10.1007/978-3-642-37036-6_20 2013

  22. [22]

    Resource-passing concurrent programming.Proceedings of TACS 2001, pages 95–126,

    56 Kazunori Ueda. Resource-passing concurrent programming.Proceedings of TACS 2001, pages 95–126,

    work page 2001

  23. [23]

    A taste of linear logic.Mathematical Structures in Computer Science, 3(4):367– 392, 1993.doi:10.1017/S0960129500000268

    58 Philip Wadler. A taste of linear logic.Mathematical Structures in Computer Science, 3(4):367– 392, 1993.doi:10.1017/S0960129500000268. Ehud Shapiro 35 59 Philip Wadler. Propositions as sessions. InProceedings of the 17th ACM SIGPLAN In- ternational Conference on Functional Programming (ICFP), pages 273–286. ACM,

    work page doi:10.1017/s0960129500000268 1993

  24. [24]

    60 Philip Wadler

    doi:10.1145/2364527.2364568. 60 Philip Wadler. Propositions as sessions.Journal of Functional Programming, 24(2–3):384–418, 2014.doi:10.1017/S095679681400001X. A Detailed madGLP Example Traces This appendix provides complete formal traces for three madGLP examples: the client- monitor example (Program 5.2), the friend-mediated introduction scenario (Bob s...

    work page doi:10.1145/2364527.2364568 2014