Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Zeta Functions and the (Linear) Logic of Markov Processes

Thomas Seiller

TL;DR

This work constructs a semantic model for second-order linear logic using realisability over sub-Markov kernels, revealing a cocycle that ties program execution to zeta functions. Beginning with discrete Interaction Graphs and extending to graphings and dynamical systems, it demonstrates how zeta-based measurements underlie orthogonality and type formation, and then generalizes to probabilistic and sub-Markov models. The main contributions include a LL^2 model accommodating discrete and continuous distributions and a robust cocycle framework for zeta-measurements across graphs, graphings, and kernels. These developments offer a principled bridge between linear logic semantics, dynamical-system invariants, and probabilistic computation, with potential implications for probabilistic programming and complexity theory.

Abstract

The author introduced models of linear logic known as ''Interaction Graphs'' which generalise Girard's various geometry of interaction constructions. In this work, we establish how these models essentially rely on a deep connection between zeta functions and the execution of programs, expressed as a cocycle. This is first shown in the simple case of graphs, before begin lifted to dynamical systems. Focussing on probabilistic models, we then explain how the notion of graphings used in Interaction Graphs captures a natural class of sub-Markov processes. We then extend the realisability constructions and the notion of zeta function to provide a realisability model of second-order linear logic over the set of all (discrete-time) sub-Markov processes.

Zeta Functions and the (Linear) Logic of Markov Processes

TL;DR

This work constructs a semantic model for second-order linear logic using realisability over sub-Markov kernels, revealing a cocycle that ties program execution to zeta functions. Beginning with discrete Interaction Graphs and extending to graphings and dynamical systems, it demonstrates how zeta-based measurements underlie orthogonality and type formation, and then generalizes to probabilistic and sub-Markov models. The main contributions include a LL^2 model accommodating discrete and continuous distributions and a robust cocycle framework for zeta-measurements across graphs, graphings, and kernels. These developments offer a principled bridge between linear logic semantics, dynamical-system invariants, and probabilistic computation, with potential implications for probabilistic programming and complexity theory.

Abstract

The author introduced models of linear logic known as ''Interaction Graphs'' which generalise Girard's various geometry of interaction constructions. In this work, we establish how these models essentially rely on a deep connection between zeta functions and the execution of programs, expressed as a cocycle. This is first shown in the simple case of graphs, before begin lifted to dynamical systems. Focussing on probabilistic models, we then explain how the notion of graphings used in Interaction Graphs captures a natural class of sub-Markov processes. We then extend the realisability constructions and the notion of zeta function to provide a realisability model of second-order linear logic over the set of all (discrete-time) sub-Markov processes.

Paper Structure

This paper contains 23 sections, 23 theorems, 75 equations, 4 figures.

Table of Contents

  1. Contributions and plan of the paper
  2. Related work
  3. Interaction Graphs: the discrete case
  4. Interaction Graphs: basic notions
  5. Bowen-Lanford Zeta Functions
  6. Zeta functions of weighted directed graphs
  7. Zeta, Execution and a Cocycle Property
  8. Graphings and dynamical systems
  9. Dynamical Systems
  10. A submodel
  11. Zeta Functions for dynamical systems
  12. Probabilities and kernels
  13. A probabilistic model
  14. Discrete-image sub-Markov processes
  15. A sub-Markov processes cocycle
  16. ...and 8 more sections

Key Result

Lemma 1.9

Let $N(n)$ denote the number of all possible strings $(v_1,\dots, v_n)$ representing a closed path in $G$ of length $n$. Then:

Figures (4)

  • Figure 1: On the left: implicit cut between two graphs (one is plain, the other is dashed). On the right: explicit cut between the same two graphs (the cut is shown below). Both representations lead to the same result, as the cut-elimination is represented by execution, an operation defined from alternating paths. It is easily checked that there is a bijective correspondence between alternating paths on the left and alternating paths on the right.
  • Figure 2: Proof of \ref{['assocexec2']}, first figure
  • Figure 3: Proof of \ref{['assocexec2']}, second figure
  • Figure 4: Figure for proof of \ref{['commutexec']}

Theorems & Definitions (91)

  • Definition 1.3: Alternating paths
  • Definition 1.4
  • Definition 1.5
  • Definition 1.6
  • Definition 1.7: seiller-goim
  • Definition 1.8
  • Lemma 1.9
  • Lemma 1.10
  • Proposition 1.11
  • proof
  • ...and 81 more