arXiv subjects

Iman Poernomo

Publications and source records attributed to Iman Poernomo.

3 recordsLinked to original sources

arXiv2026

A Type Theory of Sense: Witnessed Choice in Stratified Semantic Spaces

We introduce TTS, a dependent type theory in which semantic composition is represented by horn filling and distinctions between possible completions are witnessed relative to explicit measurement regimes. TTS replaces globally canonical composition with regime-indexed indiscernibility and constructive apartness, allowing filler spaces to be classified as canonical when all completions are observationally connected and forked when two warranted completions are positively separated. Separation witnesses enter the calculus only through measurement contexts recording actual instrument outputs, yielding conservativity, provenance, and a no-fork-from-the-empty-record result. We prove that forks persist under refinement while canonicity may fail, and characterize exactly when an identification made by one regime can consistently coexist with a separation made by another. This framework supports a geometric account of Fregean sense as a choice of filler, reference as the boundary constraining that choice, and hyperintensional difference as measured apartness, while providing a falsifiable bridge to stratified representation spaces and branching behaviour in language-model generation.

cs.LO↗

arXiv2025

Open Horn Type Theory

We introduce Open Horn Type Theory (OHTT), an extension of dependent type theory with two primitive judgment forms: coherence and gap, subject to a mutual exclusion law. Unlike classical or intuitionistic negation, gap is not defined via implication but is a primitive witness of non-coherence. Judgments may also be open -- neither coherent nor gapped -- yielding a trichotomy that generalizes the binary derivable/underivable distinction. The central construction is the transport horn: a configuration where a term and a path both cohere, but transport along the path is witnessed as gapped. This captures obstructions that Homotopy Type Theory (HoTT) cannot express, since HoTT's Kan condition guarantees all transport succeeds. We develop the semantics via ruptured simplicial sets -- simplicial sets equipped with coherence and gap structure -- and ruptured Kan complexes, which model types where some horns fill, some are gap-witnessed, and some remain open. We show that HoTT embeds as the coherent fragment of OHTT, recovered by imposing totality. Three classes of obstructions are developed in detail: topological (monodromy, holonomy, characteristic classes), semantic (polysemy, meaning fibrations), and logical (resource-sensitive derivability, substructural failure). In each case, the gap witness is positive structure -- not absence of proof, but certified obstruction.

cs.LO↗

arXiv2025

DHoTT: A Temporal Extension of Homotopy Type Theory for Semantic Drift

Dynamic HoTT (DHoTT) is a conservative extension of Homotopy Type Theory designed for evolving texts in conversational AI. In a chat system, a large language model (LLM) is queried with a growing prefix: at turn tau the input is C(tau), the concatenation of all previous prompts and replies, and the new answer extends C(tau+1). We study the logical semantics of these time indexed texts and how their meanings drift or break over time, linking Homotopy Type Theory with distributional semantics and topological data analysis on embedding spaces. For each turn we embed all tokens seen so far using a frozen encoder and map them to the unit sphere, build a good cover by spherical caps, and form the Cech nerve. A Kan fibrant replacement yields a Kan complex ET(tau), the Evolving Text at time tau, where identity types are path spaces and dependent types support ordinary HoTT transport. Time is treated functorially so that all HoTT rules interpret fibrewise and standard substitution and conservativity properties hold. On top of this fibrewise HoTT layer we add a small cross time calculus for semantic change. A carry records when a later use has a certified path back into an earlier fibre under an admissibility policy. A rupture is a positive sigma type storing finite, policy checked failed attempts together with an open horn tag. An append only ledger accumulates carries and ruptures so that earlier failures are not erased when later alignments appear. We illustrate the construction on small, replicable examples from real human LLM dialogues using a concrete DeBERTa based embedding pipeline. This provides a principled, geometrically grounded core for analysing and auditing semantic drift in large language models and other embedding based systems.

cs.LO↗