Source-linked AI summary
Linear Dependent Types and Relative Completeness
Ugo Dal Lago, Marco Gaboardi
TL;DR
Subject reduction alone does not establish termination or evaluation time. dℓPCF decorates PCF types with linear dependent indices and is sound and relatively complete, capturing input-output behavior and Krivine-machine evaluation cost.
Problem
Subject reduction bounds a normal form but does not establish termination or evaluation time, leaving the cost information in a type judgment unclear.
Source: §4 · p. 21Method
dℓPCF decorates ordinary PCF types with first-order index terms, arranging them around linear types for full recursion.
Source: §1 · p. 2Results
At most (K+1)|t| steps suffice for a typed program whose output lies between I and J; conversely, an m-step evaluation of n yields an exact-output type with I ≤ m.
Source: §1 · p. 2Takeaways & Limitations
Completeness extends beyond ground-type programs to functions on natural numbers, while judgments also convey Krivine-machine step counts.
Source: §1 · p. 2Intensional soundness requires consistent constraints; with inconsistent Φ, the cited inequality need not force weight to decrease.
Source: §4.3 · p. 28
Abstract
from arXiv · showhide
A system of linear dependent types for the lambda calculus with full higher-order recursion, called dlPCF, is introduced and proved sound and relatively complete. Completeness holds in a strong sense: dlPCF is not only able to precisely capture the functional behaviour of PCF programs (i.e. how the output relates to the input) but also some of their intensional properties, namely the complexity of evaluating them with Krivine's Machine. dlPCF is designed around dependent types and linear logic and is parametrized on the underlying language of index terms, which can be tuned so as to sacrifice completeness for tractability.
1. Introduction
Type systems offer simplicity but are often incomplete, while program logics can be relatively complete but derivability is usually undecidable. This paper introduces dℓPCF, a sound and relatively complete type system that captures program behavior and evaluation cost, with completeness depending on the language of index terms.
1. Introduction
- Type systems are valued for simplicity and often-decidable checking, but can miss programs satisfying the property being checked.By contrast, program-logics completeness is desirable but only holds relatively, with derivability almost always undecidable.Source: §1 · pp. 1–2
- dℓPCF decorates ordinary PCF types with index terms and combines dependent types with a linear-logic-inspired decomposition.Index terms are first-order terms; the system is parametrized by an equational program E that interprets their function symbols.Source: §1 · p. 2
- For a judgment K t : Nat[I,J], soundness bounds the result between I and J and the evaluation by (K + 1) · |t| steps.The judgment also conveys functional behavior and the number of Krivine Abstract Machine steps.Source: §1 · p. 2
- If a PCF term evaluates to n in m steps, completeness assigns it a type with result n and cost index I ≤ m, and extends to functions on natural numbers.Thus the typing judgments capture both functional behavior and Krivine-machine evaluation steps.Source: §1 · p. 2
- Completeness is relative to E: it requires enough expressive power to encode all total computable functions, while simpler E makes type checking and inference easier.Soundness holds independently of the specific E; increasing E's expressive power enlarges the class of captured programs.Source: §1 · pp. 2–3
2. Types and Program Properties: An Informal Account
Ordinary PCF types specify broad input and output domains, while dependent types can describe particular functions and intervals of values. dℓPCF combines such descriptions with linear cost information to capture evaluation behavior and resource use.
2. Types and Program Properties: An Informal Account
- A type such as Nat → Nat does not identify which function a program computes; it can type both identity and a unary Ackermann function.Dependent types can specify a particular function, and dℓPCF also permits imprecise interval types such as Nat[5,8].Source: §2 · p. 3
- Ordinary types do not guarantee termination for full-recursion PCF, and programs that behave alike on one input can diverge on others.The example omega behaves like dbl on input 0 but diverges on positive inputs.Source: §2 · pp. 3–4
- Linear modalities make argument-copy counts explicit in types, allowing cost information to be computed during type derivation.The evaluation cost is measured by counting how often function arguments are copied.Source: §2 · p. 4
- The system's underlying equational program E can be chosen to tune the expressiveness and tractability of reasoning about types and costs.The paper describes this parameterization as a way to tune the type system.Source: §2 · p. 5
- For dbl, dℓPCF assigns an argument-use count of a + 1 and a cost proportional to a.The example type also gives the argument copies uniform, varying index-dependent types, a feature the passage identifies as crucial to completeness.Source: §2 · pp. 4–5
3. dℓPCF
Section 3 presents dℓPCF’s index-term-based linear refinement of PCF, assigning terms types and costs under semantic index constraints, and illustrates its use in capturing recursive programs’ input-output behavior. It also establishes subject reduction: a single reduction step preserves the type while making its index bound no larger.
3.1. Index Terms and Equational Programs.
- Index terms are interpreted through equational programs over a configurable signature; bounded sums and forest cardinalities include a mechanism for counting recursive-use trees.A forest cardinality may be undefined when it describes infinite trees corresponding to diverging recursive computations.Source: §3.1 · pp. 5–7
3.2. The Type System.
- dℓPCF refines PCF by linearly decorating type derivations, with modal types representing indexed families of instances of a basic type.The section describes a modal type as a binder over instances indexed from 0 up to a bound minus one.Source: §3.2 · p. 9
- Typing judgements express that a term has a type and cost under assumptions on index variables and the types of its free term variables.Applying typing rules can require index inequalities to follow semantically from the constraints; completeness requires that all true inequalities be available, making checking computationally problematic.Source: §3.2 · p. 11
- The typing rules are syntax-directed, and each dℓPCF derivation has a structurally identical derivation in ordinary PCF for the same term.Syntax-directedness permits proofs about derivations by induction on term structure.Source: §3.2 · p. 11
3.3. An Example.
- The example subsection begins constructing a dℓPCF derivation by isolating the subterm ifz x then 0 from dbl.Source: §3.3 · p. 11
- In dbl, f is not called when d = 0 and is called once when d > 0; the passage offers gt(d, 0) only as a guess for H, not a completed assignment.Source: §3.3 · p. 13
- The fixpoint rule types dbl by tracking recursive calls with an index variable b, yielding a type for dbl at each input size a.The example concludes with dbl typed at a function type mapping Nat[a] to Nat[2a].Source: §3.3 · pp. 13–14
3.4. Properties.
- Judgements are preserved under stronger constraints, larger weights, valid index-term substitution, and contravariant context and covariant type subtyping.The properties also include context weakening and instantiation of a bounded index variable.Source: §3.4 · pp. 14–16
- The generation lemma recovers the expected shape of lambda types and constraints for zero and successor numerals from their typing judgements.For zero, the lower natural-number index is 0; for a successor, the upper index is at least 1.Source: §3.4 · p. 17
- Term substitution preserves typing: replacing a variable by a typed term yields a derivation whose weight is bounded by the original weights and summed resource uses.The stated bound is H ≤ K + I + a sum of resource uses.Source: §3.4 · p. 17
- If t reduces to u with type σ at index I, then u retains type σ at an index J satisfying J ≤ I.The theorem applies to any one-step reduction t → u.Source: §3.4 · p. 19
- For the fix x.t case, the proof interprets index J as a recursive-call tree and constructs a typing derivation reflecting its recursive subtrees.The proof proceeds by induction on the typing derivation and builds one derivation for fix x.t.Source: §3.4 · pp. 19–20
- The proof defines M to count nodes in TcJ and N to identify a node label in TaJ from an offset; the resulting recursion tree is isomorphic to TaJ.These index terms support transferring recursive-call indices between the trees.Source: §3.4 · p. 20
4. Intensional Soundness
The section establishes that dℓPCF typing tracks both program behavior and evaluation cost on Krivine’s Machine. Its intensional soundness proof uses weighted machine configurations and a decreasing measure.
4. Intensional Soundness
- Subject reduction bounds possible normal-form results, but does not establish termination or evaluation time; the section addresses this gap for Krivine’s Machine.The question is whether the type weight K carries information about evaluation complexity.Source: §4 · p. 21
4.1. The KPCF Machine
- KPCF extends the Krivine Machine to PCF constants, conditionals, and fixpoints, with transitions implementing weak-head reduction and evaluating programs.The machine represents configurations as a term, an environment, and a stack.Source: §4.1 · p. 22
4.2. Types and Weights for Configurations
- Typing and weights are lifted to machine configurations to track the terms stored in environments and stacks.The section also introduces analogous, simpler PCF typability for closures, stacks, and configurations.Source: §4.2 · p. 23, §4.1 · p. 23
4.3. Measure Decreasing and Intensional Soundness
- Weighted subject reduction makes each machine step either preserve weight while shrinking configuration size or decrease weight with bounded size growth.The intensional-soundness argument combines weight and configuration size; it requires a consistent constraint set.Source: §4.3 · pp. 24, 25, 28
- Intensional soundness bounds a program’s evaluation steps using its typing weight and, by subject reduction, bounds its result between the type’s indices.Theorem 4.6 gives a step bound; the proof tracks a measure combining configuration weight and size.Source: §4.3 · pp. 24, 28
5. Relative Completeness
The section establishes relative completeness for programs and extends it to total functions, with typings capturing output or function behavior and evaluation cost. The proofs use weighted subject expansion for programs and uniformize families of derivations for total functions.
5. Relative Completeness
- For each PCF program evaluating to numeral n, dℓPCF has a derivation whose indices capture both the reduction-step count and n.For a total PCF function f computed in time g, a derivation captures both f's extensional behavior and the intensional property expressed by g.Source: §5 · p. 29
5.1. Universal Equational Program.
- A universal equational program acts as a finite-equation interpreter for all equational programs and supports forming sums and bounded sums of index terms.The stated properties ensure that sums and bounded sums can be formed modulo the program when the relevant index terms are defined.Source: §5.1 · pp. 29–30
5.2. Subject Expansion and Relative Completeness for Programs
- Weighted Subject Expansion preserves typing across a KPCF expansion step with weight increasing by at most one, and computes the resulting derivation effectively.The proof considers precise type derivations and transformations that leave weight information unaltered; the result holds when the underlying equational program is universal.Source: §5.2 · pp. 30–31
5.2. Subject Expansion and Relative Completeness for Programs.
- If PCF program t evaluates to m in n steps, index terms I,J satisfy JIK≤n and JJK=m, and dℓPCF types t at Nat[J] under index I.Relative completeness for programs follows directly from Weighted Subject Expansion.Source: §5.2 · p. 37
5.3. Uniformization and Relative Completeness for Functions.
- A recursively enumerable family of derivations that all erases to the same PCF derivation can be captured by one derivation, an extreme form of polymorphism.This uniformization result is the key step in extending relative completeness from programs to functions.Source: §5.3 · pp. 37, 41
- Index terms can be uniformized over a shared finite variable set even when their domains differ; types and modal types require a common erased type and fixed-shape constraints.The uniform index term is defined exactly when the corresponding family member is defined.Source: §5.3 · p. 38
- For t:Nat→Nat computing total computable f with cost g, terms I,J,K satisfy JI+JK≤g, JKK=f, and I t : [b<J]·Nat[a]⊸Nat[K].The function result follows by uniformizing derivations for the programs t n, which can be built using Subject Expansion.Source: §5.3 · p. 41
6. On the Undecidability of Type Checking
dℓPCF derives all true typing judgments for programs, with completeness extending to first-order functions. Checking derivations is undecidable in general, but instantiating the framework can yield sound, possibly decidable type systems.
6. On the Undecidability of Type Checking
- Completeness covers all true typing judgments for programs and extends to first-order functions.The framework’s flexibility comes with a general type-checking undecidability caveat.Source: §6 · p. 41
- Type checking is undecidable in general when derivations rely on semantic assumptions or subtyping tied to the equational program E.For sufficiently involved E, such as U, there is no hope of a decidable complete type-checking procedure.Source: §6 · p. 41
- Instantiating E and choosing sound systems to verify semantic assumptions can produce sound, possibly decidable type systems.Completeness requires universal E, while a simpler E can make inequality checking much easier or decidable.Source: §6 · p. 41
7. dℓPCF and Implicit Computational Complexity
The paper addresses the limited expressive power of many implicit computational complexity techniques for recognizing efficient programs. dℓPCF analyzes higher-order programs directly and provides intensional completeness for PCF programs with a given complexity.
7. dℓPCF and Implicit Computational Complexity
- Many ICC techniques recognize only a small slice of efficient programs, often excluding programs for natural, well-known algorithms.The paper distinguishes this practical expressive-power limitation from extensional completeness for complexity classes as function classes.Source: §7 · p. 42
- dℓPCF can prove the complexity of all PCF programs with that complexity by deriving typing judgments for them.The paper calls this stronger property intensional completeness.Source: §7 · p. 42
- dℓPCF analyzes higher-order functional programs’ time complexity directly, without translation to low-level programs.It is not an implicit system, since bounds appear throughout, but serves as a framework for experimenting with ICC techniques.Source: §7 · p. 42
8. Related Work
The paper contrasts dℓPCF’s operational completeness with related type-theoretic approaches. Its results combine complexity information with a single derivation for functions, while drawing inspiration from linear logic and game semantics.
8. Related Work
- Intersection types capture normalization and reduction complexity, but require separate typing for each function call, unlike dℓPCF’s single derivation for total natural-number functions.The contrast is with Theorem 5.12, which gives one type derivation for each such PCF program.Source: §8 · p. 42
- Refinement types provide logical completeness for properties true in all Henkin models, whereas dℓPCF reads program results and evaluation time from types.Source: §8 · p. 42
- dℓPCF internalizes history-free game semantics in a type system, extending bounds from polynomials to arbitrary first-order total functions on natural numbers.The paper also situates BLL and QBAL as precursors inspired by geometry of interaction.Source: §8 · p. 42