Lawvere’s fixed point theorem: from λ-calculus to biology

Conversación de origen: «RNA vs DNA types» (https://claude.ai/chat/a1572c34-aaca-4b60-8d47-5e400ebff607), sin transcripción propia en el repo: este documento es su transcripción, en inglés. Índice: documentos.

Transcript of a conversation with Claude. Live version: https://claude.ai/artifact/Hc847KM3jqjQ4LQ6gNbLuJ

1. Lawvere’s theorem and fixed points in λ-calculus

Oriol: Lawvere fixed point theorem has relations with fixed points in lambda calculus

Claude: Yes — they’re essentially the same argument. The Y combinator is Lawvere’s proof written as a lambda term.

The theorem. In a cartesian closed category, if there is a point-surjective map φ : A → B^A (every map A → B is φ(a) for some point a), then every f : B → B has a fixed point.

The proof is one diagonal step. Define g(a) = f(φ(a)(a)). By surjectivity g = φ(a₀) for some a₀. Then φ(a₀)(a₀) = g(a₀) = f(φ(a₀)(a₀)), so φ(a₀)(a₀) is a fixed point.

Lambda calculus. In the untyped λ-calculus every term is also a function on terms. Semantically that means a reflexive object D with D ≅ D^D, as in Scott’s D∞. Take A = B = D and φ the isomorphism (trivially surjective). Then:

• The diagonal φ(a)(a) is self-application, x x.
  
• g is λx. f (x x).
  
• The fixed point φ(g)(g) is (λx. f (x x)) (λx. f (x x)).

That is exactly Y f; abstracting over f gives Curry’s Y combinator. So “every term has a fixed point” in λ-calculus is Lawvere’s theorem applied to D ≅ D^D.

The contrapositive is the paradox side. In Set, negation on 2 = {0,1} has no fixed point, so no surjection A → 2^A exists — Cantor’s theorem. Varying A and B gives Russell, Tarski’s undefinability of truth, Gödel’s diagonal lemma and the halting problem: all the same diagonal construction.

Two consequences for λ-calculus:

• No set-theoretic models. D ≅ D^D can’t hold in Set with all functions unless D is a single point. Scott escaped this with domains and continuous functions, where every endomap already has a least fixed point (Kleene/Tarski).
  
• No Y in simply typed λ-calculus. No type A gets a surjection onto A → A, so there is no fixed-point combinator, consistent with strong normalization. General recursion needs fix as a primitive, as in PCF.

Computability. Take A = ℕ, B^A = partial computable functions, φ = a Gödel numbering. The theorem gives Kleene’s recursion theorem: every computable transformation of programs has an extensional fixed point. Quines are the standard example.

Gödel’s self-referential sentence, the Y combinator and Cantor’s diagonal are one categorical argument. Whether you get a paradox or a fixed point depends on whether some f : B → B lacks a fixed point (impossibility) or the surjection exists (self-reference). Yanofsky’s A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points (2003) develops this.

2. Why λ-calculus models look the way they do

Oriol: Why are lambda calculus models that way?

Claude: Because they are forced to. The requirement D ≅ D^D collides with Cantor, and each feature of the standard models is a way around that collision.

1. Cardinality rules out Set. If D^D means all functions, |D^D| > |D| whenever D has two or more elements. D^D must be a restricted space of “acceptable” functions, small enough to fit back inside D.
   
2. Continuity is the restriction that works. Scott used continuous functions on a domain, a partial order of information where x ⊑ y means “y knows at least as much as x”. A program produces each finite piece of output after reading only a finite piece of input, so it is monotone and continuous. A continuous function is fixed by its action on finite approximations, which is countably much data, so D^D can be as small as D.
   
3. Lawvere explains why ⊥ must exist. Once D ≅ D^D, every map D → D has a fixed point. A negation-like map cannot exist without one, so something must be its own negation: ⊥, the undefined or non-terminating value. The Russell term (λx. not (x x))(λx. not (x x)) doesn’t blow up; it evaluates to ⊥. The partial order absorbs the diagonal argument, which is why semantics of recursion is always semantics of partiality.
   
4. Fixed points come for free. Any continuous f has a least fixed point, the limit of ⊥ ⊑ f(⊥) ⊑ f(f(⊥)) ⊑ … (Kleene): unfolding a recursive definition more and more times. In D∞ the Y combinator denotes exactly this fixed point.
   
5. D∞ is built as a limit. You can’t write down D ≅ [D → D] directly. Scott started with D₀, set Dₙ₊₁ = [Dₙ → Dₙ], embedded each level in the next and took the inverse limit: a fixed point of D ↦ [D → D], found by the same iterate-and-limit idea one level up.

Other models follow the same pattern.

• Graph models (Plotkin and Scott’s Pω, Engeler’s model) encode a continuous function as the set of its finite input/output pairs, so a function becomes an element.
  
• Combinatory algebras are purely algebraic: an application operation with S and K.

All of them handle the Cantor obstruction by allowing only functions determined by finite information. λ-terms are programs, programs use finite information, and that finiteness makes self-application consistent.

3. Relation to the Rosetta Stone

Oriol: What is the relation of this theorem to roseta?

Claude: Taking “roseta” as Baez and Stay’s Physics, Topology, Logic and Computation: A Rosetta Stone (arXiv:0903.0340): Lawvere’s theorem lives in only one corner of it, and the paper’s main distinction explains why.

Their point is that the common structure is a symmetric monoidal closed category, not a cartesian closed one. In Hilb the tensor product ⊗ is not a cartesian product, so there is no natural diagonal A → A ⊗ A: the no-cloning theorem. On the logic and computation side, the matching systems are linear logic and linear λ-calculus, where every variable is used exactly once.

Where Lawvere fits. The proof needs a diagonal: in g(a) = f(φ(a)(a)) the input a is used twice. In λ-calculus that is the x x inside Y; categorically it is the copying map Δ : A → A × A. So the theorem holds in the cartesian part: Set-like categories, intuitionistic logic, ordinary λ-calculus, linked by Curry–Howard–Lambek.

The linear part has no diagonal argument.

• Computation: linear λ-calculus has no fixed-point combinator; without duplication, β-reduction shrinks terms, so everything terminates.
  
• Logic: linear logic without the exponential ! blocks the usual diagonal constructions, which is why “light” linear logics capture polynomial time.
  
• Physics: a quantum state can’t be copied, so it can’t be fed to itself as x x requires.

Self-reference costs copying. Lawvere’s theorem — and with it Y, Gödel, Cantor and Russell — is what you get once copying is allowed. In linear logic, ! is the switch that turns copying, and the diagonal argument, back on.

4. What “copying” means

Oriol: What do you mean by copying?

Claude: Being able to use the same input twice. Categorically that is the diagonal Δ : A → A × A, a ↦ (a, a). Every set has one, and every object of a cartesian category has one for free.

The same ability in each column of the Rosetta Stone:

• Computation: a variable occurs more than once, as in λx. x x or λx. (x, x).
  
• Logic: the contraction rule. Hypotheses are reusable, so A implies A ∧ A.
  
• Categories: the diagonal Δ.
  
• Physics: cloning, turning one copy of a state into two.

Its twin is deletion, a map A → 1 (weakening in logic, an unused variable in λ). Cartesian categories have both for every object; monoidal categories need not.

Why quantum states can’t be copied. Suppose a linear C sends ψ ↦ ψ ⊗ ψ. On a + b, copying requires a⊗a + a⊗b + b⊗a + b⊗b, but linearity gives a⊗a + b⊗b. The cross terms don’t match: the no-cloning theorem. A fixed basis can be copied (|i⟩ ↦ |i⟩⊗|i⟩), but only that basis, so it isn’t natural. Copying a chosen basis is essentially what “classical information” means inside quantum theory.

Resources. Read A as “I have one euro”. A ⊸ A ⊗ A should not be provable. Linear logic reads propositions as resources for this reason: no free copying, no free deletion.

Insight. The only non-trivial step in Lawvere’s proof is feeding a both to φ and to the resulting function; remove the diagonal and the argument collapses. Fox’s theorem: a symmetric monoidal category is cartesian exactly when every object has natural, compatible copy and delete maps. Linear logic’s !A (“as many copies of A as you like”) restores copying as a controlled choice, and with it Y and the diagonal arguments.

5. Lawvere in any CCC

Oriol: Is there some mapping of lawere theorem? I supose in any CCC?

Claude: Yes. It holds in every cartesian closed category, and needs only finite products:

Let φ : A × A → B be such that every g : A → B equals φ(–, a) for some point a : 1 → A. Then every f : B → B has a fixed point.

Define g = f ∘ φ ∘ Δ, so g(x) = f(φ(x, x)). Pick a with g = φ(–, a). Then φ(a, a) = g(a) = f(φ(a, a)). In a CCC, φ curries to A → B^A.

One theorem, many categories.

The last row is the least literal: arithmetic isn’t directly a CCC, so you set up a category of formulas and substitutions (Yanofsky does this).

Typed λ view. If B^A is a retract of A (ψ : B^A → A, φ : A → B^A, φ ∘ ψ = id), then fix f = φ (ψ g) (ψ g) with g = λx. f (φ x x). If A ≅ B^A this is exactly Y. Any type containing its own function space as a retract gets a fixed-point combinator.

Where it stops. In symmetric monoidal closed categories without a diagonal (linear logic, Hilb), the proof fails at its first step.

Insight. The theorem is about products more than function spaces. Point-surjectivity is weaker than surjectivity, which is why it works in realizability toposes. In Set the contrapositive gives impossibility results; in domains or realizability the direct form gives constructions. Which you get depends only on the category.

Sources: Lawvere, Diagonal arguments and cartesian closed categories (1969); Yanofsky (2003).

6. Untyped λ-calculus

Oriol: What about u typed lambda calculus

Claude: Reading it as untyped: the untyped λ-calculus is a CCC that satisfies Lawvere’s hypothesis by construction.

Untyped means “unityped” (Scott). One type U; every term is both data and function, so U behaves like its own function space:

• application gives φ : U → U^U;
  
• abstraction gives ψ : U^U → U;
  
• β-reduction says φ ∘ ψ = id, so U^U is a retract of U;
  
• adding η also gives ψ ∘ φ = id, so U ≅ U^U.

Lambek and Scott: models of λβ are reflexive objects in CCCs, and λβη models are those with U ≅ U^U. Scott built such a CCC from syntax: terms modulo β, then the Karoubi envelope (split idempotents), whose “types” are retracts of U.

So Lawvere applies with A = B = U. fix f = φ (ψ g) (ψ g), g = λx. f (φ x x) becomes, writing application as juxtaposition, (λx. f (x x)) (λx. f (x x)) = Y f. Y is Lawvere’s proof carried out in the syntactic category.

History. Church designed λ-calculus as a foundation for logic, with connectives as terms. In 1935 Kleene and Rosser proved it inconsistent; Curry later gave a simpler version. In Lawvere’s terms, once every map on U has a fixed point, a term “not” with not(p) ≠ p is a contradiction: Y(not) equals its own negation. Church kept the pure calculus as a theory of computation, where Y(not) just fails to terminate.

Consequence. Every type in Scott’s CCC is a retract of U, and every endomap of a retract of U has a fixed point. So untyped λ can’t support a consistent logic of propositions, and its models need ⊥.

Insight. Typed versus untyped is one question: does some type contain its own function space as a retract? Simple types never do, hence normalization; untyped λ makes U such a type, hence Turing-completeness. Recursive types like μX. X → B bring the retraction back, which is how Haskell or OCaml can write Y without a built-in fix. The Kleene–Rosser inconsistency and Y are the same theorem.

If you meant simply typed: Lawvere’s hypothesis never holds there. No type A → B is a retract of A in the free CCC, so there is no Y and every term normalizes.

7. Examples of CCCs

Oriol: Can you provide more examples of CCC?

Claude: The main families, with what the exponential B^A looks like:

Non-examples. Top (exponentials only for locally compact A); Grp, Ring (products, no exponentials); Rel (its “product” is disjoint union, also its coproduct; compact closed); Vect, Hilb (closed for ⊗, not a product).

Insight. CCC-ness usually fails through the exponential, not the products. Lawvere picks out where self-reference can happen: Set, FinSet and Heyting algebras have no reflexive objects; domains, the effective topos and Scott’s Karoubi envelope do. Toposes add a subobject classifier Ω; Lawvere with B = Ω gives the internal Cantor and Russell, as Lawvere originally framed it.

8. Applied CCCs

Oriol: Some CCC focused on applied setting?

Claude: Most applied CCCs fix one problem: the natural category for a domain (measurable spaces, manifolds, topological spaces) isn’t cartesian closed, so higher-order programs have no meaning there, and a “convenient” CCC is built instead.

• Probabilistic programming: quasi-Borel spaces. Aumann (1961): no σ-algebra on ℝ^ℝ makes evaluation measurable, so “a random function” has no standard meaning. Heunen, Kammar, Staton and Yang (LICS 2017) axiomatize admissible random elements ℝ → X instead; the result is CCC with a probability monad. Recursion needed ωqbs, combining them with domains (Vákár, Kammar, Staton, POPL 2019) — again, fixed points need ⊥.
  
• Automatic differentiation: diffeological spaces. Manifolds aren’t CCC. Diffeological and Frölicher spaces make function spaces smooth again. Huot, Staton and Vákár (2020) used them to prove AD correct for higher-order programs. Related: Ehrhard and Regnier’s differential λ-calculus.
  
• Databases and scientific models: C-sets. Spivak’s functorial data migration: a schema is a small category C, an instance a functor C → Set, so instances form a presheaf topos. Migrations are adjoint functors. AlgebraicJulia’s Catlab implements this (ACSets) for epidemiological models, Petri nets and reaction networks.
  
• Compilers: “compiling to categories”. Conal Elliott (ICFP 2017) turns Haskell λ-terms into morphisms of any cartesian (closed) category, reinterpreted as circuits, AD, interval analysis or GPU code.
  
• Sensor fusion: sheaves. Robinson and others model sensors as sheaves; gluing local readings is the sheaf condition, and inconsistencies show up as cohomology.
  
• Proof assistants. Coq, Lean and Agda use locally cartesian closed categories; dependent Π-types are local exponentials.

Insight. The pattern: a classical category lacks exponentials, and a convenient category restores them by axiomatizing the probes into a space (random elements, smooth plots) rather than its subsets. Recursion keeps bringing back domains. Diffeological spaces, quasi-Borel spaces and C-sets are all concrete sheaves or presheaves, which is why they are CCC.

Given a bioinformatics background, the C-sets / AlgebraicJulia line is closest, e.g. compositional models of reaction networks.

9. What it means for C-sets

Oriol: What means in this setting?

Claude: Read as: what do cartesian closedness and Lawvere’s theorem mean for C-sets used for reaction networks?

The setting. For Petri nets the schema C has S (species), T (transitions), I (input arcs) and O (output arcs), with maps I → S, I → T, O → S, O → T. The reaction 2H₂ + O₂ → 2H₂O is one transition with three input arcs and two output arcs. Instances form the presheaf topos Set^C.

• Products and pullbacks: combining models. Libkind, Baas, Patterson and Fairbanks build stratified epidemic models this way: type an SIR model and an age-structure model over a shared type system, take the pullback, and get SIR with age groups, all reactions combined correctly.
  
• Exponentials: internal hom and queries. G^F is the object of maps F → G. In data migration, Δ (reindexing) renames or projects tables, Σ (left adjoint) unions and glues, Π (right adjoint) does “for all” joins. Π exists because presheaf toposes are locally cartesian closed.
  
• Ω: the logic of sub-models. Sub-networks form a Heyting, not Boolean, algebra: the complement of a subgraph usually isn’t one (dangling edges). AlgebraicRewriting.jl uses this for double-pushout rewriting, which works because toposes are adhesive.
  
• Lawvere: a limit on self-description. With B = Ω, negation has no fixed point (in graphs, Ω has three global truth values and negation moves each). So no instance A has a point-surjective A → Ω^A: no model can contain a complete internal index of its own sub-models. Cantor, internal to the database world.

Positive fixed-point results don’t appear: finite C-sets have no reflexive objects and no Y.

Insight. In applied category theory the useful parts are pullbacks (composing models) and Π (universal queries), not self-reference. Heyting logic shows up through the dangling-edge problem, not philosophy. Fixed points need infinity with continuity (domains) or computability (realizability).

10. In biological terms

Oriol: In biological terms?

Claude: Two separate stories: established practice in modelling biochemical networks, and the older idea of self-reproduction as a fixed point.

1. Modelling networks (established)

• Pullbacks: combining structure. A metabolic network and a compartment model (cytosol, mitochondrion, nucleus), typed over a small reaction-type network, give each metabolite in each compartment with reactions and transport assigned automatically. Same for pathways by cell type or epidemics by age.
  
• Gluing: composing pathways. Baez and Pollard treat reaction networks as open systems glued along shared species: glycolysis and the TCA cycle glue along pyruvate and acetyl-CoA, and the composite’s dynamics follow from the parts’.
  
• Rewriting: rule-based biochemistry. “A kinase binds a free site on its substrate and phosphorylates it” is a local pattern replacement. Kappa and BioNetGen have categorical semantics as graph rewriting.
  
• Heyting logic: knockouts. Removing an enzyme leaves reactions with dangling arcs. You must choose between the largest network avoiding the species (reactions with that arc cut, usually wrong) and removing every reaction that touches it.

2. Self-reproduction (the Lawvere story)

Von Neumann’s self-reproducing automaton, formalized by Kleene’s recursion theorem, needs a description used twice: interpreted to build machinery (translation) and copied into the offspring (replication). That is φ(a)(a). A cell is a quine: the genome encodes the machinery that reads and copies that genome.

DNA replication is the diagonal Δ : a ↦ (a, a). Self-reproduction works because genetic information is classical, discrete and copyable; unclonable heredity would remove the diagonal construction.

More speculative: Robert Rosen’s (M,R)-systems in Life Itself characterize organisms as “closed to efficient causation”, in effect requiring maps B → Hom(A, B) to solve fixed-point equations. Critics dispute both the mathematics and his conclusion that life is non-computable; treat it as inspiration.

Insight. Practical systems biology uses category theory for composition, not self-reference. The Lawvere–von Neumann reading puts the diagonal argument in the replication fork, and suggests why life runs on digital, copyable heredity.

11. Von Neumann’s self-reproducing automata

Oriol: Can you expand on con Neumann?

Claude: Around 1948–49, before DNA’s structure was known, von Neumann gave the logical answer to “how can anything reproduce itself?”, with the same diagonal shape as Lawvere’s theorem and Y.

The problem (Hixon Symposium 1948, Illinois lectures). Machines seem to make simpler things. A self-copier seems to need a self-description, which would have to describe itself, and so on forever.

The solution: four parts.

• A, universal constructor: given φ(X), builds X.
  
• B, copier: duplicates any description.
  
• C, controller: sequences the steps.
  
• φ(A+B+C): a description of the machine, not of the description.
  

1. C has A read φ, building a new A+B+C.
   
2. C has B copy φ.
   
3. C attaches the copy to the new machine.
   
4. The offspring is (A+B+C) + φ(A+B+C).

The regress vanishes because the description is used twice — interpreted by A, copied by B — the diagonal φ(a)(a).

The same trick in code (a Python quine):

s='s=%r;print(s%%s)';print(s%s)

In s % s the string is both the template (program, A interprets φ) and the argument (data). %r makes a quoted copy: the copier B, the diagonal Δ. Kleene’s recursion theorem (1938) guarantees quines in every language.

The formal model. Following Ulam, a 2D cellular automaton with 29 states per cell and four neighbours. Arthur Burks completed and published it as Theory of Self-Reproducing Automata (1966); it was first run in the 1990s (Nobili and Pesavento). Simplifications: Codd’s 8-state automaton, Langton’s loops.

Evolution. Add any part D: φ(A+B+C+D) builds D too and passes it on, so changes in the description are inherited. Von Neumann suggested a complexity threshold above which constructors can make things as complex as themselves or more.

Biological reading (Watson–Crick came in 1953):

Schrödinger’s What Is Life? (1944) had suggested a chromosomal “code-script”; von Neumann’s addition was the dual use, with the two operations kept separate. Sydney Brenner later remarked that biologists would have done well to read von Neumann.

Where it’s loose. Ribosomes are encoded in the genome but needed to read it; von Neumann starts with A already built. The RNA-world hypothesis (speculative) has RNA as both description and machinery — code and data the same type, like U ≅ U^U. Separating DNA from proteins would then be the step to a typed system, with translation as the map between types.

Insight. The fixed point is not a description containing itself but a description applied to itself through copying. B duplicates exactly, so genetic information must be the cloneable kind. Mutations in φ give heritable variation for selection to act on.

12. Types of RNA vs DNA

Oriol: What are the types of RNA vs DNA

Claude: Two readings: the biological classes, and the roles in the typed analogy. The first explains the second.

The 2′-OH makes RNA reactive and lets one strand fold into catalytic 3D shapes. DNA lacks it and forms a rigid helix: stable and copyable, poor at doing anything.

Kinds of DNA (almost all store the description): nuclear genomic DNA; mitochondrial and chloroplast DNA; bacterial plasmids; DNA virus genomes. Non-coding regulatory regions (promoters, enhancers) are still data read by proteins. Catalytic DNA exists only in the lab.

Kinds of RNA, by role:

• Description: mRNA (working copy of a gene); viral RNA genomes (flu, SARS-CoV-2).
  
• Machinery: rRNA (catalytic core of the ribosome; peptide bonds are formed by RNA); RNase P and self-splicing introns; snRNA (spliceosome core).
  
• Interpreter: tRNA, the codon–amino acid adaptor; with its loading enzymes it physically carries the genetic code.
  
• Regulation: miRNA, siRNA, piRNA; lncRNA; riboswitches; CRISPR RNA.
  
• Both at once: viroids, small RNA circles, some self-cleaving (they still use the host’s polymerase).

Mapping onto the typed analogy

DNA is description only, proteins machinery only, RNA spans both.

Insight. The ribosome’s catalytic centre is RNA, the same material as the code it reads — often seen as a fossil of the RNA world. tRNA is the interpreter’s lookup table: the code is set by which amino acid each tRNA carries, not by chemical necessity. One missing oxygen made DNA a pure data type.

13. Why “untyped”?

Oriol: Why untyped?

Claude: By analogy with λ-calculus: one kind of thing does two jobs a typed system keeps apart.

In λ-calculus, one type U; every term is data (passed as an argument) and function (applied to arguments). U ≅ U^U allows x x: the same object is operator and operand.

In the RNA world, one kind of molecule is data (a template, read and copied) and machinery (a ribozyme catalysing reactions). The ideal case, an RNA replicase copying RNA including itself, is x x in chemical form. Lab-evolved polymerase ribozymes copy fairly long templates, but none yet fully copies itself.

Modern cells are typed: DNA = data; protein = function; mRNA = intermediate format. Translation is φ : Data → Function with no general map back — Crick’s central dogma. In Lawvere terms there is no ψ : Function → Data with φ ∘ ψ = id, so no reflexive object and no direct self-application.

How typed cells still reproduce: with explicit components — constructor (ribosomes) for φ, copier (DNA polymerase) for Δ, control to sequence them. Like typed λ-calculus adding fix as a primitive (PCF).

Why go from untyped to typed? (analogy only)

• Stability: robust, double-stranded DNA allows error correction, like the safety of types.
  
• Division of labour: proteins (20 amino acids) are better catalysts than RNA (4 bases).
  
• Control: untyped systems let anything act on anything; RNA-world models suffer parasitic sequences copied without contributing.

Untyped corners today. The ribosome’s RNA core; retroviruses’ reverse transcription (RNA → DNA, within the data side); prions, misfolded proteins converting normal proteins — machinery copying machinery with no description, a bit like x x among functions.

Insight. “Untyped” means the same entity is operand and operator. The central dogma reads as a type discipline: φ exists, ψ doesn’t, so Lawvere’s hypothesis fails between DNA and protein. Typed systems give up automatic fixed points and add recursion as a primitive; cells did the same with dedicated replication machinery.

14. In plain biology, and cells with no DNA

Oriol: And in biological terms? What about cells with no DNA?

Claude: First the idea without mathematics, then cells with no DNA, which fit it well.

The idea in plain biology

• Early life (RNA-world hypothesis): RNA was probably both recipe (heritable information) and worker (catalysing reactions, possibly copying RNA). Nothing separated instructions from machines.
  
• Modern life: DNA is the archive (stable, copied at division, never a tool); proteins are the workers; RNA is mostly messenger and part of the reading machinery.
  
• One-way flow: DNA → RNA → protein. A protein can’t write its sequence back into DNA. That split is what “typed” meant.

Cells with no DNA — machinery without a description. They work but can’t reproduce, repair their programme or replace their proteins.

Young red blood cells (reticulocytes) keep some mRNA for a day or two, then run only on existing proteins until they wear out. Birds, reptiles and fish keep the nucleus; losing it is a mammalian specialisation.

What these cells show

• Machinery separates from description: like a compiled program with its source deleted — it runs, but nothing can be modified, repaired or copied.
  
• The description lives elsewhere: every DNA-less cell is made by a stem cell that keeps its DNA (bone marrow, lens epithelium, skin basal cells, plant companion cells).
  
• The same split at organism level: Weismann’s barrier (1890s). The germline carries the description; the soma is machinery that dies with the individual, and somatic changes don’t flow back. The germline is φ, the body is the extra part D.

Do any self-reproducing cells lack DNA? No. All known bacteria, archaea and eukaryotes have DNA genomes. RNA genomes occur only in viruses and viroids, which aren’t cells. RNA-only protocells belong to origin-of-life hypotheses and lab attempts.

Insight. DNA-less cells are pure machinery: functional, terminal, unable to reproduce — showing why von Neumann’s design needs φ on board. Multicellular organisms divide the work spatially: a few cells keep the description, many become disposable machinery. Weismann’s barrier is the central dogma’s one-way flow at organism scale.
15. Lawvere and the Curry–Howard isomorphism

Oriol: What is the relation between lawere theorem and curry Howard isomorphism?

Claude: Under Curry–Howard, Lawvere’s theorem reads as Curry’s paradox, and the Y combinator becomes a proof of that paradox.

The dictionary. Curry–Howard–Lambek matches logic (propositions, proofs, ∧, ⇒, ⊤), λ-calculus (types, terms, pairs, functions) and cartesian closed categories (objects, morphisms). Lawvere’s theorem holds in any CCC, so it has a logical reading.

The hypothesis as logic. Lawvere needs A ⇒ B as a retract of A: d : (A ⇒ B) → A and e : A → (A ⇒ B) with e ∘ d = id. Logically, A ↔︎ (A ⇒ B): “A says: if A, then B.”

The conclusion as logic: B is provable (Curry’s paradox):
1. Assume A. Then A ⇒ B, and applying it to A gives B. So A ⇒ B, with no assumptions left.
2. From A ⇒ B we get A.
3. Combining both, B.

The proof term is Lawvere’s fixed point: g = λx. e x x : A ⇒ B, and the proof of B is g (d g). It uses x twice (contraction). Normalizing it never ends: g (d g) reduces to e (d g) (d g), then back to g (d g). Paradox and non-termination are the same phenomenon.

In Haskell:

newtype R b = R (R b -> b) -- R b ≅ (R b -> b): the retraction
app :: R b -> R b -> b
app (R f) x = f x -- e : R b -> (R b -> b)
anything :: b -- “proves” every proposition
anything = (\x -> app x x) (R (\x -> app x x))

“app x x” is the diagonal φ(a)(a). “anything” type-checks at every b, including the empty type, and loops forever: as a logic Haskell is inconsistent for exactly Lawvere’s reason, with no fix or recursive definition used.

Why proof assistants forbid this. Coq, Agda and Lean reject types like R through the strict positivity check: the type being defined may not appear to the left of an arrow in its own definition. That check blocks Lawvere’s hypothesis in syntax. With B = ⊥ the hypothesis is A ↔︎ ¬A, the liar or Russell’s set, and a consistent logic can contain no such A.

Löb’s theorem. □(□A → A) → □A is, under Curry–Howard, the type of a guarded fixed-point combinator (Nakano; guarded type theory): fix : (▷A → A) → A, where ▷A means “A, one step later”. The delay allows recursion without inconsistency.

Back to copying. Curry’s paradox needs contraction, so some contraction-free logics can keep naive comprehension without collapsing — the same point as the Rosetta Stone discussion.

Insight. Under Curry–Howard, Lawvere says a proposition equivalent to its own implication proves everything; Y is the proof term and its non-termination is the paradox. Consistent systems block the hypothesis with strict positivity, no contraction, or a delay modality. Programming languages keep recursion and accept inconsistency; proof assistants keep consistency and restrict recursion.

16. History of the Rosetta Stone, and more domains

Oriol: What is the history of Rosetta stone? Are there more domains mapped?

Claude: The Rosetta Stone paper is the 2009 point where a 40-year line of category theory linking logic, computation and physics was written down as one dictionary. Since then the same dictionary has been extended to about a dozen more fields.

Why “Rosetta Stone”. The original stone, found in 1799, carries one decree in three scripts, which let Champollion decipher hieroglyphs. In mathematics the image was first used by André Weil: in a 1940 letter to his sister Simone, he called the analogy between number fields, function fields over finite fields and Riemann surfaces a Rosetta Stone. Baez and Stay used it for physics, topology, logic and computation.

History of the paper’s ideas
- 1934–1969: Curry and then Howard: proofs correspond to programs
- 1963: Lawvere’s functorial semantics: theories as categories
- 1969: Lawvere’s diagonal-argument paper (the fixed-point theorem)
- 1970s–80: Lambek: cartesian closed categories ≅ typed λ-calculus
- 1987: Girard’s linear logic: logic without free copying
- 1988: Atiyah’s TQFT axioms: physics as a functor from cobordisms
- 1980s–90s: Joyal and Street: braided monoidal categories, string diagrams
- 1995: Baez and Dolan: higher-dimensional algebra and TQFT
- 2004: Abramsky and Coecke: categorical quantum mechanics
- 2009: Baez and Stay, arXiv:0903.0340
- 2011: Published in New Structures for Physics (Lecture Notes in Physics 813, ed. Coecke)

Their contribution was synthesis: symmetric monoidal closed categories are the shared grammar, and the cartesian case (logic, λ-calculus) is a special case.

Other domains mapped since
- Homotopy theory: types as spaces, equalities as paths — HoTT book (2013), Voevodsky’s univalence
- Quantum computing: string-diagram calculus for qubits — ZX-calculus (Coecke–Duncan 2008), Picturing Quantum Processes (2017)
- Linguistics: grammar into vector-space meaning — DisCoCat (Coecke, Sadrzadeh, Clark 2010)
- Electrical circuits, control: circuits and signal-flow diagrams as morphisms — Baez–Fong, Baez–Erbele; graphical linear algebra (Bonchi, Sobociński, Zanasi)
- Chemistry, biology: open reaction networks, Petri nets — Baez–Pollard (2017), AlgebraicJulia
- Probability, statistics: stochastic maps, Bayesian inference — Markov categories (Fritz 2020)
- Machine learning: backpropagation as a functor, lenses — Fong, Spivak, Tuyéras (2019); categorical deep learning (2024)
- Game theory: composable open games — Ghani, Hedges et al. (2018)
- Databases: schemas as categories, migration as functors — Spivak (2012)
- Physics, higher: fully extended TQFTs — Lurie’s cobordism hypothesis (2009)

Also: “computational trinitarianism”, Robert Harper’s 2011 name for logic, types and categories as three views of one thing (HoTT added spaces as a fourth); and applied category theory as a field, with an annual ACT conference since 2018 and the journal Compositionality since 2019.

Insight. Markov categories fit the copying theme: a random variable can be copied, but copying is not natural for stochastic maps (sampling twice ≠ sampling once and copying), so probability sits between the cartesian and quantum worlds. Most later entries use symmetric monoidal categories, not cartesian closed ones. Lawvere’s theorem stays in the cartesian corner: HoTT has copying, so diagonal arguments work there; circuits, quantum and probability mostly lack it.

(Answered from memory; dates approximate.)