pith. sign in

arxiv: 2606.30703 · v1 · pith:JP6FP6Z2new · submitted 2026-06-29 · 💻 cs.PL

NSynC: Normalised Synthesis of Computation

Zoey Shepherd (1) , Ohad Kammar (1) , Elizabeth Polgreen (1) ((1) University of Edinburgh , Edinburgh , UK) This is my paper

Pith reviewed 2026-07-01 01:48 UTC · model grok-4.3

classification 💻 cs.PL
keywords program synthesissimply-typed lambda calculusnormal formstype-directed synthesissemantic uniquenessinductive program synthesissums
0
0 comments X

The pith

NSynC enumerates normal forms of the simply-typed lambda calculus with sums to generate only semantically unique programs.

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

The paper introduces a synthesis method that builds candidate programs directly from the normal forms of the target language instead of generating and filtering syntactic expressions. This change ensures every program examined during search has a distinct meaning, so evaluation effort is never spent rejecting duplicates. The approach relies on a top-down type-directed algorithm that traverses the space of those normal forms. On a suite of synthetic benchmarks the method produces a geometric mean speedup of 8.93 times relative to unrestricted syntactic enumeration.

Core claim

Enumerating the semantics of the target language directly by searching its normal forms guarantees that each candidate program is semantically unique and that each evaluation of a candidate is meaningful.

What carries the argument

A top-down type-directed algorithm that searches the space of normal forms of the simply-typed lambda calculus with sums.

If this is right

  • Every evaluated candidate contributes new semantic information.
  • The search space size equals the number of distinct behaviors rather than the number of expressions.
  • Synthesis time scales with semantic variety instead of syntactic redundancy.
  • The same normal-form enumeration can be reused across different specifications for the same language.

Where Pith is reading between the lines

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

  • The technique could be lifted to richer type systems or languages with additional constructs if corresponding normal-form generators are derived.
  • Synthesis tools that already perform equivalence checking might replace those checks with the upfront normal-form restriction.
  • The speedup may vary with the proportion of semantic duplicates present in a given language or benchmark set.

Load-bearing premise

The normal forms produced by the algorithm are exactly the semantically distinct programs expressible in the language, with no omissions and without extra overhead that would erase the observed speedup.

What would settle it

Two distinct normal forms that compute the same function on every input, or a benchmark run in which the normal-form search is slower than the syntactic baseline.

Figures

Figures reproduced from arXiv: 2606.30703 by Edinburgh, Elizabeth Polgreen (1) ((1) University of Edinburgh, Ohad Kammar (1), UK), Zoey Shepherd (1).

Figure 1
Figure 1. Figure 1: Log-scaled cactus plot showing the number of benchma [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Grammar for types (upper left) and terms (right) of ST [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Typing rules for STLC+. · ⊢ v : τ v →∗ v EvalValue t1 →∗ λ(x : τ ).t′ t ′ [t2/x] →∗ v t1 t2 →∗ v EvalApp t1 →∗ v1 t1 →∗ v2 ht1, t2i →∗ hv1, v2i EvalPair t →∗ hv1, v2i π1t →∗ v1 EvalFst t →∗ hv1, v2i π2t →∗ v2 EvalSnd t →∗ v inτ1+τ2 L t →∗ inτ1+τ2 L v EvalInL t →∗ v inτ1+τ2 R t →∗ inτ1+τ2 R v EvalInR t →∗ inτ1+τ2 L (v ′ ) t1[v ′ /x1] →∗ v δ(t, x1.t1, x2.t2) →∗ v EvalMatchL t →∗ inτ1+τ2 R (v ′ ) t2[v ′ /x2] … view at source ↗
Figure 4
Figure 4. Figure 4: Operational semantics of STLC+ [PITH_FULL_IMAGE:figures/full_fig_p006_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: An equational theory for STLC+. A.1 Semantic Equality We write Γ ⊢ t1 ≃τ t2 to mean that t1 and t2 are semantically equal at type τ in context Γ; we may choose to omit the type for brevity. The operational semantics above satisfies this equational theory: if Γ ⊢ t1 ≃τ t1, then for all environments Γ ⊢ σ assigning to each variable in Γ a value of the appropriate type, t1[σ] →∗ v1 and t2[σ] →∗ v2 s.t. v1 = v… view at source ↗
Figure 6
Figure 6. Figure 6: Grammar for normal forms of STLC+ [4]. x : τ ∈ Γ Γ ⊢M x : τ NFVar Γ ⊢M M : τ1 → τ Γ ⊢P P : τ1 Γ ⊢M M P : τ NFApp Γ ⊢M M : τ1 × τ2 Γ ⊢M π1M : τ1 NFFst Γ ⊢M M : τ1 × τ2 Γ ⊢M π2M : τ2 NFSnd ∃i.Γ ⊢M M : θi Γ ⊢P M : θi NFNeutral Γ ⊢P hi : 1 NFUnit Γ, x : τ1 ⊢N N : τ ∀C ∈ Guards(N).x ∈ F V (C) Γ ⊢P λ(x : τ1).N : τ1 → τ NFAbs* Γ ⊢P P1 : τ1 Γ ⊢P P2 : τ2 Γ ⊢P hP1, P2i : τ1 × τ2 NFPair Γ ⊢P P : τ1 Γ ⊢P inτ1+τ2 L (P)… view at source ↗
Figure 7
Figure 7. Figure 7: Normal form rules for STLC+ [4]. F V (t) denotes the free variables that appear in a term t [PITH_FULL_IMAGE:figures/full_fig_p009_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Rules for our ordering relations [PITH_FULL_IMAGE:figures/full_fig_p011_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Our modified normal form rules, with our ordering on sc [PITH_FULL_IMAGE:figures/full_fig_p012_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Enumeration rules for M-guess. Say we choose a. We then define the two new example sets, X1 and X2: X1 =  [ True/a, True/b hi/x1 ] 7→ True, [ True/a, False/b hi/x1 ] 7→ False X2 =  [ False/a, True/b hi/x2 ] 7→ False, [ False/a, False/b hi/x2 ] 7→ False  . Neither is empty, so we try to synthesise branches. Starting with the left branch, we want N1 s.t. X1 : Ex[Γ, x1 : 1; Bool],(a ⊏) N N1. Our example … view at source ↗
Figure 11
Figure 11. Figure 11: Refinement rules for P-refine. X : Ex[Γ; τ ] P P X : Ex[Γ; τ ], c N P NRefinePure [Γ; τ1 + τ2], c M M X1 , {σ · [v ′ /x1] 7→ v | σ 7→ v ∈ X, M[σ] →∗ inτ1+τ2 L (v ′ )} X2 , {σ · [v ′ /x2] 7→ v | σ 7→ v ∈ X, M[σ] →∗ inτ1+τ2 R (v ′ )} ∀i ∈ {1, 2}. Xi 6= ∅ ∧ Xi : Ex[Γ, xi : τi; τ ], (M ⊏) N Ni x1 ∈/ F V (N1) ∧ x2 ∈/ F V (N2) =⇒ N1 6= N2 X : Ex[Γ; τ ], c N δ(M, x1.N1, x2.N2) NRefineMatch [PITH_FULL_IMAGE:figu… view at source ↗
Figure 12
Figure 12. Figure 12: Refinement rules for N-refine [PITH_FULL_IMAGE:figures/full_fig_p015_12.png] view at source ↗
read the original abstract

Inductive program synthesis algorithms search a space of programs to find one that meets some specification. Enumerating according to the syntax of a programming language leads to a large search space, and hence slow synthesis, due in large part to semantic duplication. A synthesiser may have to evaluate -- and reject -- multiple semantically identical but syntactically different programs, wasting resources. To avoid this duplication, we present NSynC, a synthesis-by-semantics approach. By enumerating the semantics of the target language directly, we guarantee that each candidate program is semantically unique and that each evaluation of a candidate is meaningful. Specifically, we search the space of normal forms for the simply-typed lambda calculus with sums using a top-down, type-directed synthesis algorithm. Our preliminary results show a geomean speedup of 8.93x on a synthetic benchmark suite over the unrestricted algorithm.

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 / 1 minor

Summary. The paper presents NSynC, a synthesis-by-semantics approach for inductive program synthesis that enumerates normal forms of the simply-typed lambda calculus with sums via a top-down type-directed algorithm. This is intended to guarantee semantic uniqueness of candidate programs and avoid evaluating semantically duplicate programs, with a reported geomean speedup of 8.93x over an unrestricted syntax-based enumerator on a synthetic benchmark suite.

Significance. If the enumeration is shown to be complete with respect to all semantically distinct programs and the empirical results are robust, the method could meaningfully reduce wasted evaluations in program synthesis by directly searching the space of normal forms rather than the larger space of syntax trees.

major comments (2)
  1. [Abstract] Abstract: The central claim that the top-down type-directed algorithm enumerates the space of normal forms (thereby guaranteeing semantic uniqueness) lacks any completeness argument, proof, or verification that every normal form of STLC+sums is reached without omissions; an incomplete enumeration would mean the reported speedup compares an incomplete search against a complete one rather than demonstrating the benefit of duplication-free enumeration.
  2. [Abstract] Abstract: The geomean speedup of 8.93x is presented without any description of the synthetic benchmark suite, the implementation of either algorithm, the number of benchmarks, or controls confirming that the normal-form set equals the set of all semantically distinct programs; these details are required to assess whether the speedup supports the central claim.
minor comments (1)
  1. [Abstract] The abstract refers to 'preliminary results' but supplies no quantitative details on variance, individual benchmark speedups, or failure cases, which would help evaluate the reliability of the 8.93x figure.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback. The two major comments correctly identify omissions in the abstract regarding completeness and experimental details. We respond to each below and will revise the manuscript to address them.

read point-by-point responses

  1. Referee: [Abstract] Abstract: The central claim that the top-down type-directed algorithm enumerates the space of normal forms (thereby guaranteeing semantic uniqueness) lacks any completeness argument, proof, or verification that every normal form of STLC+sums is reached without omissions; an incomplete enumeration would mean the reported speedup compares an incomplete search against a complete one rather than demonstrating the benefit of duplication-free enumeration.

    Authors: We agree that the abstract (and current manuscript) lacks a completeness argument or proof for the top-down type-directed enumeration of normal forms. Without this, it is not possible to confirm that the reported speedup arises from avoiding semantic duplicates rather than from an incomplete search. We will add a formal completeness argument or proof sketch (e.g., by induction on types or a verification that all normal forms are generated) to the revised manuscript. revision: yes

  2. Referee: [Abstract] Abstract: The geomean speedup of 8.93x is presented without any description of the synthetic benchmark suite, the implementation of either algorithm, the number of benchmarks, or controls confirming that the normal-form set equals the set of all semantically distinct programs; these details are required to assess whether the speedup supports the central claim.

    Authors: We acknowledge that the abstract provides no description of the synthetic benchmark suite, number of benchmarks, implementations, or explicit controls for semantic uniqueness. The manuscript text only refers to 'a synthetic benchmark suite' without further detail. We will revise the abstract to include a brief description of the suite, the number of benchmarks, and note that both enumerators are evaluated on identical specifications with the normal-form approach guaranteeing uniqueness by construction. This will be supported by the added completeness argument. revision: yes

Circularity Check

0 steps flagged

No circularity; empirical speedup and normal-form enumeration are independent of fitted inputs or self-referential definitions

full rationale

The paper claims that enumerating normal forms of STLC+sums via a top-down type-directed algorithm yields semantically unique candidates and reports an empirical geomean speedup of 8.93x. No equations, parameters, or derivations appear; the speedup is presented as a benchmark observation rather than a quantity computed from quantities defined by the result itself. No self-citations, ansatzes, or uniqueness theorems are invoked as load-bearing steps. The central guarantee (semantic uniqueness via direct enumeration) is an algorithmic property whose completeness is a separate verification question, not a reduction of the claimed result to its own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review reveals no free parameters, axioms, or invented entities; the approach rests on the standard definition of normal forms in the simply-typed lambda calculus with sums.

pith-pipeline@v0.9.1-grok · 5689 in / 1063 out tokens · 42219 ms · 2026-07-01T01:48:43.043200+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

13 extracted references

  1. [1]

    In: Proceedi ngs of the 2013 ACM SIGPLAN Workshop on Dependently-typed Programming

    Allais, G., McBride, C., Boutillier, P.: New equations fo r neutral terms: a sound and complete decision procedure, formalized. In: Proceedi ngs of the 2013 ACM SIGPLAN Workshop on Dependently-typed Programming. pp. 13 –24 (2013)

    2013

  2. [2]

    In: Proceedings 16th Annual IEEE Symposium on Logic in Computer Science

    Altenkirch, T., Dybjer, P., Hofmann, M., Scott, P.: Norma lization by evaluation for typed lambda calculus with coproducts. In: Proceedings 16th Annual IEEE Symposium on Logic in Computer Science. pp. 303–310. IEEE (2 001)

  3. [3]

    In: 2013 Formal Methods in Computer-Aided Design

    Alur, R., Bodik, R., Juniwal, G., Martin, M.M., Raghotham an, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax- guided synthesis. In: 2013 Formal Methods in Computer-Aided Design. pp. 1–8. IEEE (2013)

    2013

  4. [4]

    ACM SIGPLAN Notices 39(1), 64–76 (2004)

    Balat, V., Di Cosmo, R., Fiore, M.: Extensional normalisa tion and type-directed partial evaluation for typed lambda calculus with sums. ACM SIGPLAN Notices 39(1), 64–76 (2004)

    2004

  5. [5]

    Proceedings of the ACM on Programming Languages 5(POPL), 1–32 (2021)

    Kim, J., Hu, Q., D’Antoni, L., Reps, T.: Semantics-guided synthesis. Proceedings of the ACM on Programming Languages 5(POPL), 1–32 (2021)

    2021

  6. [6]

    IEEE Transactions on Software Engineering 18(08), 674–704 (1992)

    Manna, Z., Waldinger, R.: Fundamentals of deductive prog ram synthesis. IEEE Transactions on Software Engineering 18(08), 674–704 (1992)

    1992

  7. [7]

    ACM SIGPLAN Notices 50(6), 619–630 (2015)

    Osera, P.M., Zdancewic, S.: Type-and-example-directed program synthesis. ACM SIGPLAN Notices 50(6), 619–630 (2015)

    2015

  8. [8]

    In: Proceedings of the 12th in ternational conference on Architectural support for programming languages and ope rating systems

    Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Sara swat, V.: Combinatorial sketching for finite programs. In: Proceedings of the 12th in ternational conference on Architectural support for programming languages and ope rating systems. pp. 404–415 (2006)

    2006

  9. [9]

    ACM SIGPLAN Notices 48(6), 287–296 (2013)

    Udupa, A., Raghavan, A., Deshmukh, J.V., Mador-Haim, S., Martin, M.M., Alur, R.: Transit: specifying protocols with concolic snippets. ACM SIGPLAN Notices 48(6), 287–296 (2013)

    2013

  10. [10]

    pure neutral

    Yallop, J., Von Glehn, T., Kammar, O.: Partially-static data as free extension of algebras. Proceedings of the ACM on Programming Language s 2(ICFP), 1–30 (2018) NSynC: Normalised Synthesis of Computation 5 τ ::= θi base types | 1 unit type | τ→ τ function types | τ× τ product types | τ + τ sum types Bool = 1 + 1 True = inBool L ⟨⟩ False = inBool R ⟨⟩ if ...

    2018

  11. [11]

    If NSynC(X : Ex[Γ; τ], (nM , n δ, d ), step) = N , then N satis- fies X

    Soundness. If NSynC(X : Ex[Γ; τ], (nM , n δ, d ), step) = N , then N satis- fies X

  12. [12]

    If any function of NSynC enumerates a term, it does not enumerate the same term except as part of a different fun ction call

    Semantic Optimality. If any function of NSynC enumerates a term, it does not enumerate the same term except as part of a different fun ction call

  13. [13]

    If there are any Γ ⊢ N N : τ with no branching arguments that satisfy X, then there is one s.t

    Bounded Completeness. If there are any Γ ⊢ N N : τ with no branching arguments that satisfy X, then there is one s.t. NSynC(X : Ex[Γ; τ], (nM , n δ, d ), step) = N Proof sketch. We assume (since we omit its definition) correctness of the su cces- sor function and take correctness of MGuessSum and MGuessBase as base cases for our induction. In each case, we...