Implementing Grassroots Logic Programs with Multiagent Transition Systems and AI

TL;DR

This paper develops formal semantics and implementations for Grassroots Logic Programs, enabling multiagent, serverless platforms on smartphones, with verified correctness and practical Dart-based implementations.

Contribution

It introduces deterministic operational semantics for GLP, derives implementation-ready versions, and proves their correctness, facilitating multiagent grassroots platform development.

Findings

dGLP and madGLP are correct implementations of GLP semantics.

dGLP was used to develop a workstation-based GLP in Dart.

madGLP is used for smartphone-based multiagent GLP in Dart.

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.