HEXAGONbeta

Expressiveness, Verifiability, Tractability: Toward a Computational Thermodynamics

A mix of human-written and AI-generated textHuman understanding: all partscs.LO — Logic in Computer Sciencemath.CT — Category Theorycs.SC — Symbolic Computation

Contributed by Benjamin Kaminsky ↗

Version 1 / Nov 12, 2026 / CC BY 4.0

Abstract

An investigation into the existence of a conservation law governing computational behaviour, in the form of the Expressiveness, Verifiability, Tractability (EVT) Hypothesis, is undertaken. The hypothesis is motivated by a simple observation: mechanisms that increase what a system can directly express, powerful control, effects, reflection, meta-programming, and self-interpretation, tend to undermine what can be verified uniformly and mechanically, while regimes that maximize static guarantees typically do so by restricting expressiveness or relocating effort into compilers, proof artifacts, or human interpretation. We analyze canonical failure modes that arise when one attempts to push beyond this frontier, distinguishing collapse of correctness, collapse of compilability, and collapse of comprehensibility. We then develop an order-theoretic model for comparing languages and verification disciplines and define an “E/V boundary” as a Pareto frontier in a partially ordered design space. Finally, we sketch how analogous tradeoffs appear in other computational domains, suggesting that “thermodynamic” boundary behaviour may be a recurring feature of expressive formalisms that demand strong global guarantees and within physical methods of information processing.

References

  1. Abramsky, Samson; Brandenburger, Adam. The Sheaf-Theoretic Structure of Non-Locality and Contextuality. New Journal of Physics, vol. 13, pp. 113036. 2011DOI
  2. Abramsky, Samson; Coecke, Bob. A Categorical Semantics of Quantum Protocols. Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, pp. 415–425. 2004DOI
  3. Arkani-Hamed, Nima; Trnka, Jaroslav. The Amplituhedron. Journal of High Energy Physics, vol. 2014, no. 10, pp. 030. 2014. arXiv:1312.2007arXivDOI
  4. Abramsky, Samson; Jagadeesan, Radha; Malacaria, Pasquale. Full Abstraction for PCF. Information and Computation, vol. 163, no. 2, pp. 409–470. 2000DOI
  5. Barendregt, Henk P. The Lambda Calculus: Its Syntax and Semantics. North-Holland. 1984
  6. Barras, Bruno. The Guard Condition of Coq. 2006. Slides/technical note
  7. Baxter, Rodney J. Exactly Solved Models in Statistical Mechanics. Academic Press. 1982
  8. Blum, Manuel. A Machine-Independent Theory of the Complexity of Recursive Functions. Journal of the ACM, vol. 14, no. 2, pp. 322–336. 1967DOI
  9. Bawden, Alan; Moon, David; Weinreb, Daniel. LISP Machine Progress Report. no. AIM-444. 1977. AI Memo 444
  10. Brady, Edwin. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming, vol. 23, no. 5, pp. 552–593. 2013DOI
Show all 67 referencesShow fewer references
  1. Courant, Richard; Friedrichs, Kurt; Lewy, Hans. Über die partiellen Differenzengleichungen der mathematischen Physik. Mathematische Annalen, vol. 100, pp. 32–74. 1928DOI
  2. Coecke, Bob; Fritz, Tobias; Spekkens, Robert W. A Mathematical Theory of Resources. Information and Computation, vol. 250, pp. 59–86. 2016DOI
  3. Conrado, Giovanna Kobus; Goharshady, Amir Kafshdar; Lam, Chun Kit. The Bounded Pathwidth of Control-Flow Graphs. Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA2, pp. 292–317. 2023DOI
  4. Coquand, Thierry; Huet, Gérard. The Calculus of Constructions. Information and Computation, vol. 76, no. 2–3, pp. 95–120. 1988DOI
  5. Church, Alonzo. An Unsolvable Problem of Elementary Number Theory. American Journal of Mathematics, vol. 58, no. 2, pp. 345–363. 1936DOI
  6. Coquand, Thierry. An Analysis of Girard's Paradox. Proceedings of the Symposium on Logic in Computer Science (LICS), pp. 227–236. 1986
  7. Cubitt, Toby S.; Pérez-García, David; Wolf, Michael M. Undecidability of the spectral gap. Nature, vol. 528, pp. 207–211. 2015DOI
  8. Curry, Haskell B. The Inconsistency of Certain Formal Logics. The Journal of Symbolic Logic, vol. 7, no. 3, pp. 115–117. 1942DOI
  9. Crary, Karl; Weirich, Stephanie. Resource Bound Certification. Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2000), pp. 184–198. 2000DOI
  10. Dal Lago, Ugo. Implicit computation complexity in higher-order programming languages: A Survey in Memory of Martin Hofmann. Mathematical Structures in Computer Science, vol. 32, no. 6, pp. 760–776. 2022DOI
  11. Danner, Norman; Licata, Daniel R.; Ramyaa, Ramyaa. Denotational cost semantics for functional languages with inductive types. Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), pp. 140–151. 2015DOI
  12. Dybvig, R. Kent; Peyton Jones, Simon; Sabry, Amr. A Monadic Framework for Delimited Continuations. Journal of Functional Programming, vol. 17, no. 6, pp. 687–730. 2007DOI
  13. Felleisen, Matthias. On the Expressive Power of Programming Languages. Science of Computer Programming, vol. 17, no. 1–3, pp. 35–75. 1991DOI
  14. Floridi, Luciano. A Conjecture on a Fundamental Trade-Off Between Certainty and Scope in Symbolic and Generative AI. Philosophy & Technology, vol. 38, pp. 93. 2025DOI
  15. Futamura, Yoshihiko. Partial Evaluation of Computation Process–An Approach to a Compiler-Compiler. Higher-Order and Symbolic Computation, vol. 12, no. 4, pp. 381–391. 1999DOI
  16. Giménez, Eduardo. Codifying Guarded Definitions with Recursive Schemes. Types for Proofs and Programs (TYPES 1994), vol. 996, pp. 39–59. 1995DOI
  17. Girard, Jean-Yves. Interprétation Fonctionnelle et Élimination des Coupures de l'Arithmétique d'Ordre Supérieur. PhD thesis, Université Paris VII. 1972. Foundational work on strong normalization for typed lambda calculi
  18. Gilbert, Seth; Lynch, Nancy. Brewer's Conjecture and the Feasibility of Consistent, Available, Partition-Tolerant Web Services. SIGACT News, vol. 33, no. 2, pp. 51–59. 2002DOI
  19. Green, Thomas R. G.; Petre, Marian. Usability Analysis of Visual Programming Environments: A 'Cognitive Dimensions' Framework. Journal of Visual Languages and Computing, vol. 7, no. 2, pp. 131–174. 1996DOI
  20. Greenblatt, Richard D. A LISP Machine. SIGARCH Computer Architecture News, vol. 8, no. 3. 1980DOI
  21. Hoffmann, Jan; Aehlig, Klaus; Hofmann, Martin. Resource Aware ML. Computer Aided Verification (CAV 2012), vol. 7358, pp. 781–786. 2012DOI
  22. Hoffmann, Jan; Hofmann, Martin. Amortized Resource Analysis with Polynomial Potential: A Static Inference of Polynomial Bounds for Functional Programs. Programming Languages and Systems (ESOP 2010), vol. 6012, pp. 287–306. 2010DOI
  23. Hairer, Ernst; Lubich, Christian; Wanner, Gerhard. Geometric Numerical Integration: Structure-Preserving Algorithms for Ordinary Differential Equations. Springer. 2006DOI
  24. Howard, William A. The Formulae-as-Types Notion of Construction. To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp. 479–490. 1980
  25. Huet, Gérard. A Unification Algorithm for Typed λ\lambda-Calculus. Theoretical Computer Science, vol. 1, no. 1, pp. 27–57. 1975DOI
  26. Huet, Gérard. Resolution d'équations dans les langages d'ordre 1,2,…,ω1,2,\dots,\omega. Proceedings of the 2nd International Conference on Automata, Languages and Programming (ICALP). 1976. Higher-order unification; semi-decidability and search behavior
  27. Hurkens, Antonius J. C. A Simplification of Girard's Paradox. Typed Lambda Calculi and Applications (TLCA 1995), vol. 902, pp. 266–278. 1995DOI
  28. Jones, Neil D.; Gomard, Carsten K.; Sestoft, Peter. Partial Evaluation and Automatic Program Generation. Prentice Hall. 1993
  29. Kaminsky, M. Benjamin. Geometric Computation: Twin Helices and the Algebra of Flow. 2025. Preprint DOI, pending acceptanceDOI
  30. Korepin, V. E.; Bogoliubov, N. M.; Izergin, A. G. Quantum Inverse Scattering Method and Correlation Functions. Cambridge University Press. 1993
  31. Kogge, Peter M. The Architecture of Symbolic Computers. McGraw-Hill. 1991. Also listed in some catalogs as a 1990 publication/printing.
  32. Kochen, Simon; Specker, Ernst P. The Problem of Hidden Variables in Quantum Mechanics. Journal of Mathematics and Mechanics, vol. 17, no. 1, pp. 59–87. 1967
  33. Landauer, Rolf. Irreversibility and Heat Generation in the Computing Process. IBM Journal of Research and Development, vol. 5, no. 3, pp. 183–191. 1961DOI
  34. Landin, Peter J. The Next 700 Programming Languages. Communications of the ACM, vol. 9, no. 3, pp. 157–166. 1966DOI
  35. Milner, Robin. A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences, vol. 17, no. 3, pp. 348–375. 1978DOI
  36. Moon, David A. Garbage Collection in a Large Lisp System. Proceedings of the 1984 ACM Symposium on LISP and Functional Programming. 1984. Describes GC techniques in the Symbolics 3600 environment
  37. Nielsen, Michael A.; Chuang, Isaac L. Quantum Computation and Quantum Information. Cambridge University Press. 2010
  38. Patterson, David A.; Ditzel, David R. The Case for the Reduced Instruction Set Computer. ACM SIGARCH Computer Architecture News, vol. 8, no. 6, pp. 25–33. 1980
  39. Perlis, Alan J. Epigrams on Programming. ACM Press. 1982. Often circulated as ``Epigrams in Programming''; includes the ``Turing tarpit'' epigram
  40. Pierce, Benjamin C. Types and Programming Languages. The MIT Press. 2002
  41. Rice, H. G. Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society, vol. 74, no. 2, pp. 358–366. 1953DOI
  42. Rogers, Hartley. Theory of Recursive Functions and Effective Computability. McGraw–Hill. 1967
  43. Sabry, Amr; Felleisen, Matthias. Reasoning about Programs in Continuation-Passing Style. LISP and Symbolic Computation, vol. 6, no. 3–4, pp. 289–360. 1993DOI
  44. Shapiro, Lionel. Curry's Paradox. 2017. Accessed 2026-03-03. Stanford Encyclopedia of Philosophy
  45. Soare, Robert I. Recursively Enumerable Sets and Degrees. Springer. 1987DOI
  46. Schaefer, Stefan; Sommer, Rainer; Virotta, Francesco. Critical slowing down and error analysis in lattice QCD simulations. Nuclear Physics B, vol. 845, no. 1, pp. 93–119. 2011DOI
  47. Steele, Guy L. The Evolution of Lisp. History of Programming Languages, Volume II. 2002
  48. Tait, William W. Intensional Interpretations of Functionals of Finite Type I. The Journal of Symbolic Logic. 1967. Classic normalization proof technique (Tait's method)
  49. Tarski, Alfred. The Concept of Truth in Formalized Languages. Oxford University Press. 1936. Translated in Logic, Semantics, Metamathematics (1956)
  50. Thorup, Mikkel. All structured programs have small tree width and good register allocation. Information and Computation. 1998DOI
  51. Turing, Alan M. On Computable Numbers, with an Application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, vol. s2-42, no. 1, pp. 230–265. 1937DOI
  52. Troyer, Matthias; Wiese, Uwe-Jens. Computational Complexity and Fundamental Limitations to Fermionic Quantum Monte Carlo Simulations. Physical Review Letters, vol. 94, no. 17, pp. 170201. 2005DOI
  53. Wells, J. B. Typability and Type-Checking in the Second-Order Lambda-Calculus are Equivalent and Undecidable. Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), pp. 176–185. 1994DOI
  54. Wells, J. B. Typability and Type Checking in System F are Equivalent and Undecidable. Annals of Pure and Applied Logic, vol. 98, no. 1–3, pp. 111–156. 1999DOI
  55. Wright, Andrew K.; Felleisen, Matthias. A Syntactic Approach to Type Soundness. Information and Computation, vol. 115, no. 1, pp. 38–94. 1994
  56. Weinreb, Daniel; Moon, David. The Lisp Machine Manual. MIT Artificial Intelligence Laboratory. 1981
  57. Weirich, Stephanie; Voizard, Antoine; Azevedo de Amorim, Pedro Henrique; Eisenberg, Richard A. A Specification for Dependent Types in Haskell. Proceedings of the ACM on Programming Languages, vol. 1, no. ICFP, pp. 31:1–31:29. 2017DOI

Version history

  1. v1 · 39 pagesSubmitted by Benjamin KaminskyInitial depositCurrentNov 11, 2026