pith. sign in

arxiv: 1907.07767 · v1 · pith:7YOGJR2Dnew · submitted 2019-07-12 · 💻 cs.LO · math.LO

Delta -- new logic programming language and Delta-methodology for p-computable programs on Turing Complete Languages

Andrey Nechesov This is my paper

Pith reviewed 2026-05-24 22:21 UTC · model grok-4.3

classification 💻 cs.LO math.LO
keywords logic programmingp-computable programsDelta languagelist-formulasdynamic modelsverifiable programssmart contracts
0
0 comments X

The pith

Delta treats programs as list-formulas whose truth is checked on dynamic models to achieve p-computability and translatability.

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

The paper presents Delta as a logic programming language built on a new definition of formulas. D-formulas are special list-formulas constructed iteratively from base formulas. Execution consists of checking the truth of such a formula on a dynamic model that records final variable values. The authors claim this setup makes Delta-programs p-computable and verifiable while allowing direct translation into languages such as Java, Python, and Solidity. They extend the approach into a methodology for creating such programs in high-level languages, with explicit attention to smart contracts and Internet of Things applications.

Core claim

Delta-programs are special list-formulas. The execution of a program is the process of checking truth of the D-formula on a dynamic model. Programs are created by iterations using simple base formulas on these models where final values of variables are saved when the formula is checked.

What carries the argument

D-formulas (Delta programs) defined as list-formulas, with execution as truth-checking on dynamic models that store final variable values.

If this is right

  • Delta-programs are p-computable by construction.
  • Delta-programs are verifiable through truth-checking on dynamic models.
  • Delta-programs can be translated into PHP, Java, JavaScript, C++, Python, Solidity and similar languages.
  • The Delta-methodology produces p-computable programs suitable for smart contracts and Internet of Things devices.

Where Pith is reading between the lines

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

  • If the translation step preserves p-computability, the same programs could run across multiple platforms without separate verification.
  • Dynamic models that record variable values might simplify debugging of contract logic by exposing intermediate states.
  • Iterative construction from base formulas could reduce the surface area for errors when generating IoT control code.

Load-bearing premise

Redefining formulas as list-formulas and execution as truth-checking on dynamic models automatically confers p-computability and verifiability without further constraints or proofs.

What would settle it

A concrete Delta-program expressed as a list-formula whose execution on a dynamic model either fails to terminate in polynomial time or cannot be translated into an equivalent program in one of the listed high-level languages.

read the original abstract

In paper describes the new logic programming language Delta, which have a many good properties. Delta-programs is p-computable, verifiable and can translation on other languages. Also we describe the Delta-methodology for constructing p-computable programs in high-level languages such as PHP, Java, JavaScript, C++, Pascal, Delphi, Python, Solidity and other. We would like to especially note the use of the Delta methodology for creating Smart Contracts and for Internet of things. We change the concept of the formula and define D-formulas(or Delta programs) are special list-formulas. Then we define the execution of a program how is the process of checking truth D-formula on a dynamic model. Main idea our paper consider program how list-formula from another formulas on dynamic models. And we created by iterations new Delta-programs use simple base formulas for this. Also we entered a dynamic models how models where we save final values of variables when check formula on this model.

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

2 major / 2 minor

Summary. The paper introduces the Delta logic programming language, defining D-formulas as special list-formulas whose execution consists of checking their truth on dynamic models built iteratively from base formulas. It claims that Delta-programs are p-computable and verifiable, translatable to other languages, and presents the Delta-methodology for constructing such programs in high-level languages including PHP, Java, JavaScript, C++, Pascal, Delphi, Python, and Solidity, with emphasis on applications to smart contracts and the Internet of Things.

Significance. If the central claims were supported by formal arguments, this work could represent a significant contribution by providing a definitional framework that guarantees p-computability for logic programs and their implementations in conventional languages. The emphasis on verifiability for smart contracts and IoT applications addresses practical needs in those domains. However, the manuscript offers no derivations, examples, or complexity analyses to substantiate these properties.

major comments (2)
  1. [Abstract] Abstract: The claim that Delta-programs are p-computable is asserted based on the redefinition of formulas as list-formulas and execution as truth-checking on dynamic models, but no derivation, asymptotic runtime analysis in terms of formula size, or reduction to a polynomial-time problem is provided. This is load-bearing for the central claim.
  2. [Introduction and definitions] Introduction and definitions: The properties of p-computability and verifiability are said to follow directly from the new definitions of D-formulas and dynamic models without external benchmarks, independent derivations, or comparison to existing logic programming systems such as Prolog or Datalog. This creates an internal circularity where the claimed properties are built into the redefinitions.
minor comments (2)
  1. [Abstract] Abstract: Grammatical issues include 'In paper describes' (should be 'The paper describes') and 'have a many good properties' (should be 'has many good properties').
  2. [Throughout] Throughout the manuscript: No concrete examples of D-formulas, dynamic models, or their iterative construction and truth-checking are supplied, making the concepts difficult to evaluate.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the report. We respond point-by-point to the major comments below.

read point-by-point responses

  1. Referee: [Abstract] Abstract: The claim that Delta-programs are p-computable is asserted based on the redefinition of formulas as list-formulas and execution as truth-checking on dynamic models, but no derivation, asymptotic runtime analysis in terms of formula size, or reduction to a polynomial-time problem is provided. This is load-bearing for the central claim.

    Authors: The manuscript asserts p-computability from the definitions but does not contain an explicit derivation, runtime analysis, or reduction. The iterative construction of dynamic models from base formulas is intended to bound the checking process by the length of the list-formula, but we agree this requires formalization. We will add a dedicated subsection with a simple inductive argument and example showing linearity in formula size. revision: yes

  2. Referee: [Introduction and definitions] Introduction and definitions: The properties of p-computability and verifiability are said to follow directly from the new definitions of D-formulas and dynamic models without external benchmarks, independent derivations, or comparison to existing logic programming systems such as Prolog or Datalog. This creates an internal circularity where the claimed properties are built into the redefinitions.

    Authors: We disagree that the argument is circular. The definitions of D-formulas (as list-formulas) and dynamic models (as structures that store final variable values after base-formula checks) are introduced as a distinct framework; p-computability is then derived from the fact that truth-checking proceeds by finite iterations over these lists rather than from an external oracle. This differs in structure from Prolog's SLD-resolution. No independent derivation is supplied because the properties are claimed to be internal consequences of the model, but a short comparison paragraph can be added for clarity. revision: no

Circularity Check

1 steps flagged

P-computability and verifiability asserted directly from redefinition of formulas as list-formulas and execution as dynamic-model truth-checking, with no independent bound or reduction shown

specific steps
  1. self definitional [Abstract]
    "We change the concept of the formula and define D-formulas(or Delta programs) are special list-formulas. Then we define the execution of a program how is the process of checking truth D-formula on a dynamic model. Main idea our paper consider program how list-formula from another formulas on dynamic models. ... Delta-programs is p-computable, verifiable"

    The manuscript claims p-computability follows from the redefinition of programs as list-formulas whose execution is truth-checking on dynamic models constructed iteratively from base formulas. No derivation, runtime bound in terms of formula size, or reduction to a known polynomial-time procedure is given; the property is taken to hold by the act of redefinition.

full rationale

The paper's central derivation defines D-formulas as list-formulas and program execution as iterative truth-checking on dynamic models, then states that these programs are p-computable and verifiable. No separate complexity analysis, reduction to a known P problem, or external benchmark is supplied; the claimed properties are presented as following from the definitions themselves. This matches the self-definitional pattern exactly.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claims rest on newly introduced definitions of D-formulas and dynamic models that are not derived from or benchmarked against established logic or computability theory.

axioms (1)
  • ad hoc to paper D-formulas are special list-formulas whose truth is checked on dynamic models to execute programs.
    This redefinition is introduced in the abstract without reference to prior formal systems.
invented entities (1)
  • Dynamic models no independent evidence
    purpose: Models that save final values of variables when checking a formula.
    New modeling construct introduced to support the execution definition.

pith-pipeline@v0.9.0 · 5697 in / 1167 out tokens · 19699 ms · 2026-05-24T22:21:36.269934+00:00 · methodology

discussion (0)

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