  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.
