Horn Linear Logic and Minsky Machines

TL;DR

This paper establishes a detailed correspondence between linear logic derivations and Minsky machine computations, demonstrating how proofs can be systematically transformed into computational processes.

Contribution

It provides a rigorous proof that linear logic derivations for Horn sequents can be converted into Minsky machine computations, integrating proof-theoretic and computational methods.

Findings

Proof of transformation from linear logic derivations to Minsky computations

Methodology distributing complex points across independent parts

Establishment of a systematic translation process

Abstract

Here we give a detailed proof for the crucial point in our Minsky machine simulation - that any linear logic derivation for a specific Horn sequent can be transformed into a Minsky computation leading from an initial configuration to the halting configuration. Among other things, the presentation advantage of the 3-step program is that the non-trivial tricky points are distributed between the independent parts each of which we justify following its own intrinsic methodology (to say nothing of the induction used in the opposite directions): (1) From LL to HLL - we use purely proof-theoretic arguments. (2) From HLL to Horn programs - we translate trees (HLL derivations) into another trees (Horn programs)of the same shape, almost. (3) From Horn programs to Minsky computations - we use purely computational arguments.