pith. sign in

arxiv: 2606.20944 · v1 · pith:PRRH652Knew · submitted 2026-06-18 · 💻 cs.PL

Big-step and small-step Horn clause derivations applied to operational semantics

John P. Gallagher , Manuel Hermenegildo , Jos\'e Morales , Pedro Lopez-Garcia , Louis Rustenholz This is my paper

Pith reviewed 2026-06-26 14:42 UTC · model grok-4.3

classification 💻 cs.PL
keywords Horn clausesbig-step semanticssmall-step semanticsoperational semanticsinterpreter specializationprogram transformationequivalence of derivations
0
0 comments X

The pith

Horn clause sets can be transformed into provably equivalent versions that follow either big-step or small-step derivation rules through interpreter specialization.

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

The paper establishes that big-step derivations are equivalent to two forms of small-step derivations when applied to Horn clauses. It shows that specializing an interpreter implementing one of these strategies produces a new Horn clause program whose behavior exactly matches the original under the chosen derivation style. As a direct result, operational semantics written in big-step style as Horn clauses can be converted automatically into equivalent small-step versions. A reader would care because this gives a uniform, provable method to relate and rewrite semantic definitions without ad-hoc manual changes. Experiments on several programming languages confirm the transformation works in practice.

Core claim

We prove equivalence between big-step derivations and two versions of small-step derivations for Horn clauses. By specialising interpreters for these derivation strategies, any set of Horn clauses can be transformed into a provably equivalent set of clauses that inherits the behaviour of a given (big- or small-step) Horn clause interpreter. As a special case of this transformation, big-step semantics for any programming language, expressed directly as Horn clauses, can be transformed into equivalent small-step semantics.

What carries the argument

Specialization of interpreters that encode big-step or small-step derivation strategies, which rewrites any input Horn clause set into one that follows the target derivation style while preserving equivalence.

If this is right

  • Big-step operational semantics expressed as Horn clauses become convertible to equivalent small-step semantics.
  • The output clauses inherit exactly the derivation behavior of the chosen interpreter.
  • The same transformation applies uniformly to any set of Horn clauses, not only language semantics.
  • Equivalence between the derivation styles holds after transformation.

Where Pith is reading between the lines

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

  • One could start from a single Horn clause definition and generate multiple equivalent semantic presentations in different derivation styles.
  • Properties easier to prove in one style might be established by transforming the clauses and reusing the proof in the other style.
  • The approach might extend to deriving interpreters that mix big-step and small-step steps within one program.

Load-bearing premise

Specialization of the derivation-strategy interpreters produces equivalent clauses for arbitrary Horn clause sets without extra side conditions on the clauses or interpreters.

What would settle it

A Horn clause program for which the specialized clauses produce different computed answers, different termination behavior, or different derivation trees compared with the original under the corresponding big-step or small-step interpreter.

read the original abstract

The concepts of big-step and small-step derivations are familiar from the operational semantics of programming languages. These concepts are applicable in the more general setting of Horn clause derivations. We prove equivalence between big-step derivations and two versions of small-step derivations for Horn clauses. By specialising interpreters for these derivation strategies, any set of Horn clauses can be transformed into a provably equivalent set of clauses that inherits the behaviour of a given (big- or small-step) Horn clause interpreter. As a special case of this transformation, big-step semantics for any programming language, expressed directly as Horn clauses, can be transformed into equivalent small-step semantics. Experiments with a variety of programming languages are reported.

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

0 major / 2 minor

Summary. The paper proves equivalence between big-step derivations and two versions of small-step derivations for Horn clauses. By specializing interpreters for these derivation strategies, any set of Horn clauses can be transformed into a provably equivalent set that inherits the behavior of a given (big- or small-step) Horn clause interpreter. As a special case, big-step semantics for any programming language, expressed directly as Horn clauses, can be transformed into equivalent small-step semantics. Experiments with a variety of programming languages are reported.

Significance. If the equivalence proofs and transformations hold, this provides a formal, general method for relating big-step and small-step operational semantics in a Horn-clause setting and for deriving one from the other via interpreter specialization. The formal proof (rather than an informal argument) and the lack of additional side conditions on clause sets are strengths. The reported experiments supply concrete validation across multiple languages.

minor comments (2)
  1. [Abstract] The abstract would be clearer if it briefly named the two versions of small-step derivations.
  2. A short table or diagram contrasting the three derivation strategies (big-step and the two small-step variants) would help readers track the equivalences proved in the main body.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive review, the recognition of the formal equivalence proofs without side conditions, and the recommendation to accept. We appreciate the acknowledgment of the experimental validation across multiple languages.

Circularity Check

0 steps flagged

No significant circularity; derivation is a direct formal proof

full rationale

The paper's central claim is a formal proof of equivalence between big-step derivations and two small-step variants for arbitrary Horn clause sets, followed by a semantics-preserving transformation obtained by specializing the corresponding interpreters. This is established through explicit construction and proof rather than parameter fitting, self-definition, or load-bearing self-citation chains. No equation or step reduces the claimed result to its own inputs by construction; the equivalence is shown independently for any set of Horn clauses without additional side conditions. The derivation chain is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract describes a proof and transformation with no free parameters, invented entities, or non-standard axioms mentioned.

pith-pipeline@v0.9.1-grok · 5650 in / 935 out tokens · 21499 ms · 2026-06-26T14:42:33.525273+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

43 extracted references · 28 canonical work pages

  1. [1]

    In: Proc

    Ager, M.S.: From natural semantics to abstract machines. In: Proc. LOPSTR 2004. LNCS, vol. 3573, pp. 245–261. Springer (2004). https://doi.org/10.1007/11506676 16

    work page doi:10.1007/11506676 2004

  2. [2]

    In: Proc

    Ambal, G., Lenglet, S., Schmitt, A., Noˆ us, C.: Certified derivation of small-step from big-step skeletal semantics. In: Proc. PPDP 2022. pp. 11:1–11:48. ACM (2022). https://doi.org/10.1145/3551357.3551384

    work page doi:10.1145/3551357.3551384 2022

  3. [3]

    Apt, K.R., van Emden, M.H.: Contributions to the theory of logic programming. J. ACM29(3), 841–862 (1982). https://doi.org/10.1145/322326.322339

    work page doi:10.1145/322326.322339 1982

  4. [4]

    Beckman, L., Haraldson, A., Oskarsson, ¨O., Sandewall, E.: A partial evalua- tor, and its use as a programming tool. Artif. Intell.7(4), 319–357 (1976). https://doi.org/10.1016/0004-3702(76)90011-4

    work page doi:10.1016/0004-3702(76)90011-4 1976

  5. [5]

    In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W

    Bjørner, N., Gurfinkel, A., McMillan, K.L., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24–51. Springer (2015). https://doi.org/10.1007/978-3-319-23534- 9 2

    work page doi:10.1007/978-3-319-23534- 2015

  6. [6]

    Journal of Logic Programming6(2–3), 135–162 (1989)

    Bruynooghe, M., De Schreye, D., Krekels, B.: Compiling control. Journal of Logic Programming6(2–3), 135–162 (1989)

    1989

  7. [7]

    In: Felleisen, M., Gardner, P

    Chargu´ eraud, A.: Pretty-big-step semantics. In: Felleisen, M., Gardner, P. (eds.) Proceedings of ESOP 2013. pp. 41–60. Lecture Notes in Computer Science, Springer (2013). https://doi.org/10.1007/978-3-642-37036-6 3

    work page doi:10.1007/978-3-642-37036-6 2013

  8. [8]

    Communications of the A.C.M

    Colmerauer, A.: An introduction to Prolog III. Communications of the A.C.M. (July 1990)

    1990

  9. [9]

    Gallagher, Manuel V

    De Angelis, E., Fioravanti, F., Gallagher, J.P., Hermenegildo, M.V., Pettorossi, A., Proietti, M.: Analysis and transformation of constrained Horn clauses for Big-step and small-step Horn clause derivations applied to operational semantics31 program verification. Theory Pract. Log. Program.22(6), 974–1042 (2022). https://doi.org/10.1017/S1471068421000211

    work page doi:10.1017/s1471068421000211 2022

  10. [10]

    In: Semantics of Data Types

    Despeyroux, T.: Executable specification of static semantics. In: Semantics of Data Types. LNCS, vol. 173, p. 215–233. Springer-Verlag (1984)

    1984

  11. [11]

    Ershov, A.P.: On the partial computation principle. Inf. Process. Lett.6(2), 38–41 (1977). https://doi.org/10.1016/0020-0190(77)90078-3

    work page doi:10.1016/0020-0190(77)90078-3 1977

  12. [12]

    Systems, Computers, Controls2(5), 45–50 (1971)

    Futamura, Y.: Partial evaluation of computation process - an approach to a compiler-compiler. Systems, Computers, Controls2(5), 45–50 (1971)

    1971

  13. [13]

    In: Pro- ceedings PEPM’93

    Gallagher, J.P.: Specialisation of logic programs: A tutorial. In: Pro- ceedings PEPM’93. pp. 88–98. ACM Press, Copenhagen (June 1993). https://doi.org/10.1145/154630.154640

    work page doi:10.1145/154630.154640 1993

  14. [14]

    In: Proc

    Gallagher, J.P.: Transforming logic programs by specialising interpreters. In: Proc. ECAI-86. pp. 109–122 (1986)

    1986

  15. [15]

    In: Gl¨ uck, R., Kafle, B

    Gallagher, J.P., Hermenegildo, M.V., Morales, J.F., L´ opez-Garc´ ıa, P.: Transform- ing big-step to small-step semantics using interpreter specialisation. In: Gl¨ uck, R., Kafle, B. (eds.) Proceedings LOPSTR 2023. pp. 28–38. Lecture Notes in Computer Science, Springer (2023). https://doi.org/10.1007/978-3-031-45784-5 3

    work page doi:10.1007/978-3-031-45784-5 2023

  16. [16]

    In: PEPM

    Giacobazzi, R., Jones, N.D., Mastroeni, I.: Obfuscation by partial eval- uation of distorted interpreters. In: PEPM. pp. 63–72. ACM (2012). https://doi.org/10.1145/2103746.2103761

    work page doi:10.1145/2103746.2103761 2012

  17. [17]

    Gl¨ uck, R.: On the generation of specializers. J. Funct. Program.4(4), 499–514 (1994). https://doi.org/10.1017/S0956796800001167

    work page doi:10.1017/s0956796800001167 1994

  18. [18]

    In: Charlier, B.L

    Gl¨ uck, R., Jørgensen, J.: Generating transformers for deforestation and super- compilation. In: Charlier, B.L. (ed.) Proc. SAS’94. LNCS, vol. 864, pp. 432–448. Springer (1994). https://doi.org/10.1007/3-540-58485-4 57

    work page doi:10.1007/3-540-58485-4 1994

  19. [19]

    In: Walker, D.E., Norton, L.M

    Green, C.C.: Application of theorem proving to problem solving. In: Walker, D.E., Norton, L.M. (eds.) Proceedings of the 1st International Joint Conference on Artificial Intelligence. pp. 219–240. William Kaufmann (1969)

    1969

  20. [20]

    In: Kameyama, Y., Xie, N

    Harbo, S.K.R., H¨ uttel, H.: Computation-tree semantics: An algorithmic approach to structurally defined relations. In: Kameyama, Y., Xie, N. (eds.) Proceedings of PEPM 2026. pp. 2–16. ACM (2026). https://doi.org/10.1145/3779209.3779534

    work page doi:10.1145/3779209.3779534 2026

  21. [21]

    Hill, P.M., Gallagher, J.P.: Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 5, chap. Meta-Programming in Logic Programming, pp. 421–

  22. [22]

    Oxford University Press (1998)

    1998

  23. [23]

    Journal of Symbolic Logic16(1), 14–21 (1951)

    Horn, A.: On sentences which are true of direct unions of algebras. Journal of Symbolic Logic16(1), 14–21 (1951). https://doi.org/10.2307/2268661

    work page doi:10.2307/2268661 1951

  24. [24]

    In: Concurrency, Compositionality, and Correctness

    Huizing, C., Koymans, R., Kuiper, R.: A small step for mankind. In: Concurrency, Compositionality, and Correctness. LNCS, vol. 5930, pp. 66–73. Springer (2010). https://doi.org/10.1007/978-3-642-11512-7 5

    work page doi:10.1007/978-3-642-11512-7 2010

  25. [26]

    Jones, N.D.: Transformation by interpreter specialisation. Sci. Comput. Program. 52, 307–339 (2004). https://doi.org/10.1016/j.scico.2004.03.010

    work page doi:10.1016/j.scico.2004.03.010 2004

  26. [27]

    In: Brandenburg, F., Vidal-Naquet, G., Wirs- ing, M

    Kahn, G.: Natural semantics. In: Brandenburg, F., Vidal-Naquet, G., Wirs- ing, M. (eds.) Proc. STACS 87. LNCS, vol. 247, pp. 22–39. Springer (1987). 32Big-step and small-step Horn clause derivations applied to operational semantics https://doi.org/10.1007/BFb0039592

    work page doi:10.1007/bfb0039592 1987

  27. [28]

    Theory Pract

    K¨ orner, P., Leuschel, M., Barbosa, J., Costa, V.S., Dahl, V., Hermenegildo, M.V., Morales, J.F., Wielemaker, J., Diaz, D., Abreu, S.: Fifty years of Prolog and beyond. Theory Pract. Log. Program.22(6), 776–858 (2022). https://doi.org/10.1017/S1471068422000102

    work page doi:10.1017/s1471068422000102 2022

  28. [29]

    In: Rosenfeld, J.L

    Kowalski, R.A.: Predicate logic as programming language. In: Rosenfeld, J.L. (ed.) Information Processing, Proceedings of the 6th IFIP Congress 1974, Stockholm, Sweden, August 5-10, 1974. pp. 569–574. North-Holland (1974)

    1974

  29. [30]

    In: European Confer- enceonComputerVision(ECCV)(2022).https://doi.org/10.1007/978-3-031- 19842- 7_7,https://www.ecva.net/papers/eccv_2022/papers_ECCV/papers/ 136990106.pdf

    Lami, P., Lanese, I., Stefani, J.: A small-step semantics for Janus. In: Mogensen, T.Æ., Mikulski, L. (eds.) Reversible Computation RC 2024. pp. 105–123. Lecture Notes in Computer Science, Springer (2024). https://doi.org/10.1007/978-3-031- 62076-8 8

    work page doi:10.1007/978-3-031- 2024

  30. [31]

    Leuschel, M., Jørgensen, J.: Efficient specialisation in Prolog using the hand- written compiler generator LOGEN. Elec. Notes Theor. Comp. Sci.30(2)(1999). https://doi.org/10.1017/S1471068403001662

    work page doi:10.1017/s1471068403001662 1999

  31. [32]

    Springer-Verlag (1987)

    Lloyd, J.: Foundations of Logic Programming: 2nd Edition. Springer-Verlag (1987). https://doi.org/10.1007/978-3-642-83189-8

    work page doi:10.1007/978-3-642-83189-8 1987

  32. [33]

    Lombardi, L.A.: Incremental computation: The preliminary design of a pro- gramming system which allows for incremental data assimilation in open- ended man-computer information systems. Adv. Comput.8, 247–333 (1967). https://doi.org/10.1016/S0065-2458(08)60698-1

    work page doi:10.1016/s0065-2458(08)60698-1 1967

  33. [34]

    In: Mes- nard, F., Stuckey, P.J

    Nys, V., Schreye, D.D.: Compiling control as offline partial deduction. In: Mes- nard, F., Stuckey, P.J. (eds.) Proc. LOPSTR. LNCS, vol. 11408, pp. 115–131. Springer (2018). https://doi.org/10.1007/978-3-030-13838-7 7

    work page doi:10.1007/978-3-030-13838-7 2018

  34. [35]

    Aliprantis and Kim C

    St¨ ark, R.F.: A direct proof for the completeness of SLD-resolution. In: B¨ orger, E., B¨ uning, H.K., Richter, M.M. (eds.) CSL ’89, Proceedings. Lecture Notes in Com- puter Science, vol. 440, pp. 382–383. Springer (1989). https://doi.org/10.1007/3- 540-52753-2 52

    work page doi:10.1007/3- 1989

  35. [36]

    BIT17(2), 215–226 (1977)

    T¨ arnlund, S.: Horn clause computability. BIT17(2), 215–226 (1977)

    1977

  36. [37]

    In: Ganzinger, H., Jones, N.D

    Turchin, V.F.: Program transformation by supercompilation. In: Ganzinger, H., Jones, N.D. (eds.) Programs as Data Objects. LNCS, vol. 217, pp. 257–281. Springer (1985). https://doi.org/10.1007/3-540-16446-4 15

    work page doi:10.1007/3-540-16446-4 1985

  37. [38]

    Observational and Physical Classification of Supernovae

    Vesely, F., Fisher, K.: One step at a time - A functional derivation of small- step evaluators from big-step counterparts. In: Caires, L. (ed.) Proc. ESOP 2019. LNCS, vol. 11423, pp. 205–231. Springer (2019). https://doi.org/10.1007/978-3- 030-17184-1 8

    work page doi:10.1007/978-3- 2019

  38. [39]

    In: Ramalingam, G., Visser, E

    Yokoyama, T., Gl¨ uck, R.: A reversible programming language and its invertible self-interpreter. In: Ramalingam, G., Visser, E. (eds.) Proceedings of PEPM 2007. pp. 144–153. ACM (2007). https://doi.org/10.1145/1244381.1244404 Big-step and small-step Horn clause derivations applied to operational semantics33 Appendix A Proofs of Theorems A runR 1 ⇒∗R ′ is...

    work page doi:10.1145/1244381.1244404 2007

  39. [40]

    IfB 2 ⇒R 1 thenR 1 is a foldable conjunction ortrue

  40. [41]

    With the notation just introduced, we can combine the two cases of the Lemma

    IfR 2 ⇒R 1 thenR 1 is a foldable conjunction ortrue. With the notation just introduced, we can combine the two cases of the Lemma. Let atom or foldable(R). Then • IfR 2 ⇒R 1 thenR 1 is a foldable conjunction ortrue. ProofLetP suff be the set of suffix clauses forP. The proof is by induction on the height m≥1 of the derivation. • m= 1: The derivation isB 2...

  41. [42]

    letfold(R k) =B, B←B ′ ∧R 3 ∈k [P∪P suff] henceR=R 4 ∧R 3 whereatom or foldable(R4) and letfold(R k

  42. [43]

    =fold(fold(R k2 2 )∧R 3)k) →B 1 3 ⇒fold(R k2 2 ) premise of [FOLD1] →R 4 2 ⇒R 2 by ind. hyp. eitherB ′ =fold(R 4) orR 4 =B ′ →R 4 ∧R 3 2 ⇒R 2 ∧R 3 using [CONJ1] →R 2 ⇒R 1 sinceR=R 4 ∧R 3, R1 =R 2 ∧R 3 □ Lemma 12.LetPbe a set of big-step rules satisfying the final value condition (Definition 2). Let (⟨s1, ρ1⟩ ⇓v 1) 3 ⇒(⟨s 2, ρ2⟩ ⇓v 2) be derived using the ...

  43. [44]

    ProofThe shortest proof of (⟨s 1, ρ1⟩ ⇓v 1) 3⇒(⟨s 2, ρ2⟩ ⇓v 2) using the rules in Figure 5 has height 2, using rules [FOLD0] and [UNF0]

    Thenv 1 =v 2. ProofThe shortest proof of (⟨s 1, ρ1⟩ ⇓v 1) 3⇒(⟨s 2, ρ2⟩ ⇓v 2) using the rules in Figure 5 has height 2, using rules [FOLD0] and [UNF0]. The proof is by induction on derivations of height k≥2. • k= 2: Using [FOLD0], there are clauses; (⟨s, ρ⟩ ⇓v 1)←(⟨s 2, ρ2⟩ ⇓v 2), R2. (⟨s′, ρ′⟩ ⇓v 2)←R 2. If the premise of [FOLD0], (⟨s2, ρ2⟩ ⇓v 2) 3 ⇒trues...

    2024