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

TL;DR

This paper introduces a dependently typed lambda calculus extension that encodes probabilistic programs with transparent and opaque nondeterminism, proving strong normalization and enabling reasoning about trustworthiness.

Contribution

It presents a novel dependently typed system that models probabilistic computation with both transparent and opaque nondeterminism, including trustworthiness reasoning.

Findings

Proves strong normalization for the extended calculus.

Formalizes opaque nondeterminism using oracle constants.

Enables reasoning about program trustworthiness within the type system.

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.