pith. sign in

arxiv: 2505.07103 · v3 · submitted 2025-05-11 · 💻 cs.LO

The K_infty Homotopy λ-Model

Daniel O. Mart\'inez-Rivillas , Ruy J.G.B. de Queiroz This is my paper

Pith reviewed 2026-05-22 16:10 UTC · model grok-4.3

classification 💻 cs.LO
keywords lambda calculusScott modelD_inftyKan complexbeta-eta conversionhomotopy modelweakly ordered setdomain theory
0
0 comments X

The pith

Extending Scott's D_infty to a weakly ordered Kan complex K_infty makes interpretations of some higher beta-eta conversions of lambda terms non-equivalent.

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

The paper constructs an extension of Dana Scott's classic complete ordered set D_infty for modeling the lambda calculus. It replaces the ordered set with a complete weakly ordered Kan complex named K_infty that retains the original completeness properties while adding structure to keep certain higher-order conversions distinct. The construction is chosen so that the semantic interpretations of some beta-eta convertible lambda terms at higher levels remain non-equivalent. A reader would care because this yields a finer model that can separate terms traditional domain models collapse, opening a route to homotopy-aware semantics for lambda calculus.

Core claim

We extend the complete ordered set Dana Scott's D_infty to a complete weakly ordered Kan complex K_infty, with properties that guarantee the non-equivalence of the interpretation of some higher conversions of beta eta-conversions of lambda-terms.

What carries the argument

K_infty, a complete weakly ordered Kan complex extending D_infty that adds weak ordering and Kan complex structure to enforce distinct interpretations for higher beta-eta conversions while preserving completeness.

If this is right

  • Some lambda terms that are beta-eta equivalent at higher orders receive distinct semantic values in K_infty.
  • The model remains a complete domain in the sense of Scott while incorporating weak homotopy structure.
  • Interpretations of lambda terms can now distinguish conversions that collapse in the original D_infty.
  • The construction supplies a concrete semantic setting in which higher conversions are not forced to be equivalent.

Where Pith is reading between the lines

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

  • The approach suggests that classical domain models can be refined by homotopy data without sacrificing the ability to interpret all lambda terms.
  • If the extension works, similar weak-order Kan complex constructions might be applied to other domain-theoretic models to obtain finer distinctions.
  • One could test the model on small lambda terms with known higher conversions to measure the actual separation achieved.

Load-bearing premise

A complete weakly ordered Kan complex extending D_infty can be built with exactly the properties needed to keep interpretations of higher conversions non-equivalent.

What would settle it

Explicit construction of K_infty followed by direct computation showing that two specific higher-order beta-eta convertible lambda terms receive identical interpretations under the model, or that the Kan complex axioms fail to hold.

read the original abstract

We extend the complete ordered set Dana Scott's $D_\infty$ to a complete weakly ordered Kan complex $K_\infty$, with properties that guarantee the non-equivalence of the interpretation of some higher conversions of $\beta\eta$-conversions of $\lambda$-terms.

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 manuscript constructs a complete weakly ordered Kan complex K_∞ extending Dana Scott's D_∞ and claims that this structure interprets λ-terms such that certain higher-order βη-conversions remain non-equivalent.

Significance. A successful construction would supply a homotopy-theoretic model for the untyped λ-calculus that distinguishes conversions typically collapsed in domain-theoretic semantics, potentially informing work on higher equivalences in homotopy type theory and denotational semantics.

major comments (2)
  1. [§3] §3 (Construction of the simplicial structure): the horn-filling operations must be shown to respect the weak order so that they do not force homotopies identifying interpretations that the order is intended to keep distinct; without an explicit verification that chosen fillers preserve the non-equivalence property for higher βη-conversions, the central claim cannot be assessed.
  2. [§4] Definition of completeness for the weakly ordered Kan complex (likely in §4): it is unclear how the extension of D_∞ simultaneously satisfies the Kan condition, the weak order, and completeness while retaining the distinctions needed for the non-equivalence result; this compatibility is load-bearing for the model property.
minor comments (2)
  1. [Abstract] The abstract would benefit from naming at least one concrete higher conversion whose non-equivalence is guaranteed by the model.
  2. [§3] Notation for the face and degeneracy maps of K_∞ should be introduced explicitly before their use in the verification of the Kan condition.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and valuable comments on our manuscript. The points raised highlight areas where additional explicit verification would strengthen the presentation. We address each major comment below and will revise the manuscript accordingly to incorporate the suggested clarifications.

read point-by-point responses

  1. Referee: [§3] §3 (Construction of the simplicial structure): the horn-filling operations must be shown to respect the weak order so that they do not force homotopies identifying interpretations that the order is intended to keep distinct; without an explicit verification that chosen fillers preserve the non-equivalence property for higher βη-conversions, the central claim cannot be assessed.

    Authors: We agree that an explicit verification strengthens the argument. The horn-filling operations in the construction of K_∞ are defined by extending the order-preserving maps from the approximating D_n spaces, selecting fillers that are minimal with respect to the weak order. This ensures that if two simplices represent interpretations of λ-terms distinguished by higher-order βη-conversions, the chosen fillers do not introduce homotopies collapsing them. We will add a dedicated lemma in §3 proving that the fillers preserve these distinctions, including a check that the weak order relations are maintained under the simplicial operations. revision: yes

  2. Referee: [§4] Definition of completeness for the weakly ordered Kan complex (likely in §4): it is unclear how the extension of D_∞ simultaneously satisfies the Kan condition, the weak order, and completeness while retaining the distinctions needed for the non-equivalence result; this compatibility is load-bearing for the model property.

    Authors: The construction proceeds via an inverse limit of finite approximations, each of which is a complete weakly ordered Kan complex. The Kan condition holds by the simplicial enrichment of the function space in the homotopy category, the weak order is the pointwise lifting of the order on D_∞, and completeness is inherited from the directed suprema in each finite stage. Distinctions for non-equivalent βη-conversions are retained because the order is strict on the underlying interpretations and homotopies are only quotiented for provably equivalent terms. We will expand §4 with a theorem explicitly stating and proving this simultaneous compatibility. revision: yes

Circularity Check

0 steps flagged

No circularity detected; construction presented as independent extension

full rationale

The abstract claims an extension of Scott's D_infty to a complete weakly ordered Kan complex K_infty whose properties guarantee non-equivalence of certain higher beta-eta interpretations. No equations, explicit derivations, self-citations, or load-bearing assumptions are visible in the provided text that reduce the claimed guarantee to a definitional fit or prior self-result. The central step is the existence of a construction satisfying both Kan conditions and the weak order while preserving distinctions; absent any quoted reduction showing that the non-equivalence property is inserted by fiat or by renaming an input, the derivation chain does not exhibit circularity. This is the expected outcome when only high-level claims are available and no internal steps collapse to their own premises.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review provides no explicit free parameters, axioms, or invented entities beyond the high-level claim of extending D_infty; full paper needed to audit.

pith-pipeline@v0.9.0 · 5566 in / 957 out tokens · 33185 ms · 2026-05-22T16:10:04.476145+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Recursive Completion in Higher K-Models: Front-Seed Semantics, Proof-Relevant Witnesses, and the K-Infinity Model

    cs.LO 2026-04 conditional novelty 6.0 full

    A reduced front-seed coherence package (WL, WR) plus one pentagon contraction recovers associator, pentagon, and bridge theorems, while explicit coordinatewise reify/reflect formulas are given for K-infinity, all Lean...

Reference graph

Works this paper leans on

21 extracted references · 21 canonical work pages · cited by 1 Pith paper · 1 internal anchor

  1. [1]

    Hindley, J

    J. Hindley, J. Seldin, Lambda-Calculus and Combinators, an Introduction, Cambridge University Press, New York, 2008

    work page 2008

  2. [2]

    Martínez-Rivillas, R

    D. Martínez-Rivillas, R. de Queiroz, The∞-groupoid generated by an arbi- trary topologicalλ-model, Logic Journal of the IGPL 30 (3) (2022) 465–488 https://doi.org/10.1093/jigpal/jzab015, (also arXiv:1906.05729)

    work page doi:10.1093/jigpal/jzab015 2022

  3. [3]

    Abramsky, A

    S. Abramsky, A. Jung, Domain theory, In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3, pages 1–168, Clarendon Press, 1994

    work page 1994

  4. [4]

    Asperti, G

    A. Asperti, G. Longo, Categories, Types and Structures: An Introduction to Category Theory for the working computer scientist, Foundations of Computing Series, M.I.T Press, 1991

    work page 1991

  5. [5]

    Martínez-Rivillas, R

    D. Martínez-Rivillas, R. de Queiroz, Towards a homotopy domain theory, Archive for Mathematical Logic (also arXiv 2007.15082). URLhttps://doi.org/10.1007/s00153-022-00856-0 39

    work page doi:10.1007/s00153-022-00856-0 2007

  6. [6]

    Martínez-Rivillas, R

    D. Martínez-Rivillas, R. de Queiroz, Solving homotopy domain equations, arXiv:2104.01195. URLhttps://arxiv.org/abs/2104.01195

    work page arXiv

  7. [7]

    The CMS experiment at the CERN LHC

    D. Martínez-Rivillas, Towards a homotopy domain theory, Tese doutoral, Centro de Informática (CIn), Universidade Federal de Pernambuco (UFPE), Recife, BR (2022). URLhttps://repositorio.ufpe.br/handle/123456789/49221

    work page arXiv 2022

  8. [8]

    Boardman, R

    J. Boardman, R. Vogt, Homotopy invariant algebraic structures on topo- logical spaces, Lecture Notes in Mathematics, 347, Berlin, New York: Springer-Verlag, 1973

    work page 1973

  9. [9]

    Joyal, Quasi-categories and kan complexes, Journal of Pure and Applied Algebra 175 (1) (2002) 207–222

    A. Joyal, Quasi-categories and kan complexes, Journal of Pure and Applied Algebra 175 (1) (2002) 207–222

    work page 2002

  10. [10]

    Joyal, M

    A. Joyal, M. Tierney, Quasi-categories vs segal spaces, Categories in al- gebra, geometry and mathematical physics, Contemp. Math. 431 (2008) 277–326

    work page 2008

  11. [11]

    Lurie, Higher Topos Theory, Princeton University Press, Princeton and Oxford, 2009

    J. Lurie, Higher Topos Theory, Princeton University Press, Princeton and Oxford, 2009

    work page 2009

  12. [12]

    Lurie, Kerodon,https://kerodon.net(2025)

    J. Lurie, Kerodon,https://kerodon.net(2025)

    work page 2025

  13. [13]

    Lurie, Higher Algebra, Harvard University, 2017

    J. Lurie, Higher Algebra, Harvard University, 2017

    work page 2017

  14. [14]

    Goerss, J

    P. Goerss, J. Jardine, Simplicial Homotopy Theory, Birkhäuser Basel, Springer Nature Switzerl and AG, 2009

    work page 2009

  15. [15]

    Friedman, An elementary illustrated introduction to simplicial sets, Rocky Mountain J

    G. Friedman, An elementary illustrated introduction to simplicial sets, Rocky Mountain J. Math. 42 (2) (2012) 353–423

    work page 2012

  16. [16]

    Cisinski, Higher Categories and Homotopical Algebra, Cambridge University Press, 2019

    D.-C. Cisinski, Higher Categories and Homotopical Algebra, Cambridge University Press, 2019. 40

    work page 2019

  17. [17]

    Rezk, Introduction to Quasicategories, Lecture Notes for course at Uni- versity of Illinois at Urbana-Champaign, 2022

    C. Rezk, Introduction to Quasicategories, Lecture Notes for course at Uni- versity of Illinois at Urbana-Champaign, 2022. URLhttps://faculty.math.illinois.edu/~rezk/quasicats.pdf

    work page 2022

  18. [18]

    Rezk, Stuff about quasicategories, Lecture Notes for course at University of Illinois at Urbana-Champaign, 2017

    C. Rezk, Stuff about quasicategories, Lecture Notes for course at University of Illinois at Urbana-Champaign, 2017

    work page 2017

  19. [19]

    A short course on $\infty$-categories

    M. Groth, A short course on∞-categories, 2015. URLhttps://arxiv.org/abs/1007.2925

    work page internal anchor Pith review Pith/arXiv arXiv 2015

  20. [20]

    Martínez-Rivillas, R

    D. Martínez-Rivillas, R. de Queiroz, The theory of an arbitrary higherλ-model, Bulletin of the Section of Logic 52 (1) (2023) 39–58 https://doi.org/10.18778/0138–0680.2023.11, (also arXiv 2111.07092)

    work page doi:10.18778/0138 2023

  21. [21]

    Hatcher, Algebraic Topology, Cambridge University Press, New York, NY, 2001

    A. Hatcher, Algebraic Topology, Cambridge University Press, New York, NY, 2001. 41

    work page 2001