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.File | Dimensione | Formato | |
---|---|---|---|
978-3-030-41103-9_3.pdf
solo utenti autorizzati
Descrizione: versione pubblicata
Tipologia:
Versione dell'editore
Licenza:
Copyright dell'editore
Dimensione
569.29 kB
Formato
Adobe PDF
|
569.29 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.