Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Strongly Normalising System of Dependent Types for Transparent and Opaque Probabilistic Computation

Francesco A. Genco

TL;DR

This work presents a strongly normalising system that combines dependent types with probabilistic and nondeterministic computation, including both transparent and opaque execution models via oracle constants and oracular functions. The core technical contribution is a reducibility-based strong normalization proof for both terms and type constructors, together with a careful treatment of kinds, type constructors, and their evaluation during typing. A novel trustworthiness predicate and a static evaluation framework are added to reason about the runtime behavior and reliability of probabilistic programs within the type system. The resulting framework enables precise encoding of learning-like behavior and the testing of program trust during type checking, with potential implications for reliable, opacity-aware AI systems grounded in formal type theory.

Abstract

We define an extension of lambda-calculus with dependents types that enables us to encode transparent and opaque probabilistic programs and prove a strong normalisation result for it by a reducibility technique. While transparent nondeterministic programs are formalised by rather usual techniques, opaque nondeterministic programs are formalised by introducing in the syntax oracle constants, the behaviour of which is governed by oracular functions. The generality of these functions and the fact that their values are determined by the form of the whole term inside which the relative oracle occurs also enable us to simulate learning-like behaviours. We then extend the calculus in order to define a computational trustworthiness predicate. The extension of the calculus does not only enable us to precisely formalise a notion of trustworthiness and to encode the procedures required to test it on programs, but also to reason, by means of the type system, on the behaviour of programs with respect to trustworthiness.

A Strongly Normalising System of Dependent Types for Transparent and Opaque Probabilistic Computation

TL;DR

This work presents a strongly normalising system that combines dependent types with probabilistic and nondeterministic computation, including both transparent and opaque execution models via oracle constants and oracular functions. The core technical contribution is a reducibility-based strong normalization proof for both terms and type constructors, together with a careful treatment of kinds, type constructors, and their evaluation during typing. A novel trustworthiness predicate and a static evaluation framework are added to reason about the runtime behavior and reliability of probabilistic programs within the type system. The resulting framework enables precise encoding of learning-like behavior and the testing of program trust during type checking, with potential implications for reliable, opacity-aware AI systems grounded in formal type theory.

Abstract

We define an extension of lambda-calculus with dependents types that enables us to encode transparent and opaque probabilistic programs and prove a strong normalisation result for it by a reducibility technique. While transparent nondeterministic programs are formalised by rather usual techniques, opaque nondeterministic programs are formalised by introducing in the syntax oracle constants, the behaviour of which is governed by oracular functions. The generality of these functions and the fact that their values are determined by the form of the whole term inside which the relative oracle occurs also enable us to simulate learning-like behaviours. We then extend the calculus in order to define a computational trustworthiness predicate. The extension of the calculus does not only enable us to precisely formalise a notion of trustworthiness and to encode the procedures required to test it on programs, but also to reason, by means of the type system, on the behaviour of programs with respect to trustworthiness.

Paper Structure

This paper contains 6 sections, 12 theorems, 38 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Kinds, types and terms
  3. The calculus
  4. The evaluation relation and its basic properties
  5. Strong normalisation
  6. A theory of program evaluation and trustworthiness

Key Result

Theorem 4.1

For any type constructor $\varphi :\Phi$, if $\varphi\mapsto \varphi'$, then $\varphi':\Phi$ and all free term variables of $\varphi '$ occur free also in $\varphi$. For any term $t : A$, if $t\mapsto_p t'$, then $t':A'$---where $A'$ has the same propositional and quantificational structure as $A$ b

Figures (6)

  • Figure 1: Formation and axiom rules for kinds and types
  • Figure 2: Kind assignment rules
  • Figure 3: Weakening rules
  • Figure 4: Type assignment and conversion rules
  • Figure 5: Evaluation reductions
  • ...and 1 more figures

Theorems & Definitions (42)

  • Definition 2.1: Typeless Terms
  • Definition 2.2: Kindless Type constructors
  • Definition 2.3: Kinds
  • Definition 2.4: Variables occurring in a kind
  • Definition 2.5: Subconstructors and variables occurring in a type constructor
  • Definition 2.6: Subterms and variables occurring in a term
  • Definition 2.7: Binder scope, bound variables, free variables
  • Definition 2.8: Substitution
  • Definition 2.9: Term contexts and type constructor contexts
  • Definition 3.1: Oracle constants and oracular functions
  • ...and 32 more