Intersection Types and (Positive) Almost-Sure Termination
summary
Intersection types exactly characterize two probabilistic termination notions: the probability of convergence equals the least upper bound of norms of certain type distributions, and the expected number of steps equals the least upper bound of derivation weights. Types are built from multi-distributions and scaled multisets (arrow types map intersection types to distributions), and non-idempotency is necessary for precision. Results are both sound and complete, exemplified by a term with expectation 4, and are recursion-theoretically optimal: AST is Π0 2-complete and PAST is Σ0 2-complete.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 2:40Side Results
- 3:51Term Evaluation
- 5:23Probabilistic Termination
- 7:10Calculus
- 8:17Reduction Tree
- 8:57Recursiveness
- 9:39Intersection Types
- 11:34Multidistributions
- 15:27Examples
- 17:56Type Types
- 22:46Ongoing and Further Work
related talks
19mPositive Almost-Sure Termination – Complexity and Proof Rules
01h 11mStatistical Limits of Causal Inference
55mThree Problems in Computable Probability Theory
01h 39mIsomorphic Reasoning: Counting with Types Part 1
57mPropositions as Types
54mOpaque Types To Infinity
28mData Driven Convergence in Statistical Estimators
57mIt ain't over till it's over