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.

翻译：基层逻辑程序（GLP）是一种面向智能手机、无服务器基层平台实现的多智能体并发逻辑编程语言。本文从GLP及其并发与多智能体抽象非确定性操作语义maGLP出发，分别推导出面向实现的确定性操作语义dGLP与madGLP，并证明其与对应抽象语义的等价性。人工智能（Claude）将dGLP作为形式规约，据此开发了基于工作站的GLP Dart实现；madGLP正被人工智能作为形式规约，用于开发基于智能手机的GLP多智能体Dart实现。核心思想在于：跨越智能体的maGLP共享变量对可通过全局链路连接的局部变量对实现，其正确性源于不相交替换可交换性（基于GLP的单次出现不变性）与持久性。我们证明madGLP与maGLP均具有基层特性。