A Linear Logic Programming Language for Concurrent Programming over Graph Structures

TL;DR

This paper introduces LM, a linear logic programming language designed for concurrent graph algorithms, combining classical and linear logic to enable expressive, node-level computation with inter-node communication.

Contribution

The paper presents the design, syntax, and semantics of LM, a novel logic programming language that supports concurrent programming over graph structures using linear logic.

Findings

LM enables declarative programming of graph algorithms.

The language supports natural concurrency through node-level facts.

Examples demonstrate LM's expressiveness and operational semantics.

Abstract

We have designed a new logic programming language called LM (Linear Meld) for programming graph-based algorithms in a declarative fashion. Our language is based on linear logic, an expressive logical system where logical facts can be consumed. Because LM integrates both classical and linear logic, LM tends to be more expressive than other logic programming languages. LM programs are naturally concurrent because facts are partitioned by nodes of a graph data structure. Computation is performed at the node level while communication happens between connected nodes. In this paper, we present the syntax and operational semantics of our language and illustrate its use through a number of examples.