We present a theory of types where formulas may contain a choice constructor. This constructor allows for the selection of a particular type among a finite set of options, each corresponding to a given probabilistic term. We show that this theory induces a type assignment system for the probabilistic λ –calculus introduced in an earlier work by Chris Hankin, Herbert Wiklicky and the author, where probabilistic terms represent probability distributions on classical terms of the simply typed λ –calculus. We prove the soundness of the type assignment with respect to a probabilistic term reduction and a normalization property of the latter.
A Type Theory for Probabilistic { extdollar}{ extdollar}{ extbackslash}lambda { extdollar}{ extdollar}{ extendash}calculus
Alessandra Di Pierro
2020-01-01
Abstract
We present a theory of types where formulas may contain a choice constructor. This constructor allows for the selection of a particular type among a finite set of options, each corresponding to a given probabilistic term. We show that this theory induces a type assignment system for the probabilistic λ –calculus introduced in an earlier work by Chris Hankin, Herbert Wiklicky and the author, where probabilistic terms represent probability distributions on classical terms of the simply typed λ –calculus. We prove the soundness of the type assignment with respect to a probabilistic term reduction and a normalization property of the latter.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
