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 non-deterministic programs are formalised in a rather usual way, opaque non-deterministic 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.

翻译：我们定义了一种带依赖类型的λ演算扩展，该扩展能够编码透明与不透明的概率程序，并通过可归约性技术证明了其强规范化性质。透明非确定性程序采用较为常规的方式形式化，而不透明非确定性程序则通过在语法中引入预言机常数进行形式化，其行为由预言函数调控。这些函数的通用性及其取值由相关预言机所在整体项的结构决定的特点，也使得我们能够模拟类学习行为。