Probabilistic operational semantics for the lambda calculus
From MaRDI portal
Abstract: Probabilistic operational semantics for a nondeterministic extension of pure lambda calculus is studied. In this semantics, a term evaluates to a (finite or infinite) distribution of values. Small-step and big-step semantics are both inductively and coinductively defined. Moreover, small-step and big-step semantics are shown to produce identical outcomes, both in call-by- value and in call-by-name. Plotkin's CPS translation is extended to accommodate the choice operator and shown correct with respect to the operational semantics. Finally, the expressive power of the obtained system is studied: the calculus is shown to be sound and complete with respect to computable probability distributions.
Recommendations
- A probabilistic semantics for the pure \(\lambda\)-calculus
- A deterministic rewrite system for the probabilistic \(\lambda\)-calculus
- Probabilistic -calculus and Quantitative Program Analysis
- Boolean-valued semantics for the stochastic \(\lambda \)-calculus
- A lambda-calculus foundation for universal probabilistic programming
Cites work
- scientific article; zbMATH DE number 4179333 (Why is no real title available?)
- scientific article; zbMATH DE number 4179422 (Why is no real title available?)
- scientific article; zbMATH DE number 3764843 (Why is no real title available?)
- scientific article; zbMATH DE number 1064116 (Why is no real title available?)
- scientific article; zbMATH DE number 1748069 (Why is no real title available?)
- A lambda calculus for quantum computation with classical control
- A probabilistic language based upon sampling functions
- CPS transformation of beta-redexes
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Coinductive big-step operational semantics
- Domains for Computation in Mathematics, Physics and Exact Real Arithmetic
- Elements of stream calculus (an extensive exercise in coinduction)
- Introduction to bisimulation and coinduction
- LCF considered as a programming language
- Nondeterministic extensions of untyped \(\lambda\)-calculus
- Notions of computation and monads
- Probabilistic operational semantics for the lambda calculus
- Probabilistic -calculus and Quantitative Program Analysis
- Proofs of Randomized Algorithms in Coq
- Representing Control: a Study of the CPS Transformation
- Stochastic lambda calculus and monads of probability distributions
- The duality of computation
Cited in
(47)- A distribution semantics for probabilistic term rewriting
- Calibrating generative models: the probabilistic Chomsky-Schützenberger hierarchy
- scientific article; zbMATH DE number 7559292 (Why is no real title available?)
- On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
- scientific article; zbMATH DE number 7393562 (Why is no real title available?)
- QPCF: higher-order languages and quantum circuits
- Quantum programming made easy
- The Benefit of Being Non-Lazy in Probabilistic λ-calculus
- On higher-order probabilistic subrecursion
- On higher-order probabilistic subrecursion
- Probabilistic termination by monadic affine sized typing
- A Type Theory for Probabilistic \lambda –calculus
- Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
- Probabilistic -calculus and Quantitative Program Analysis
- Semantics of quantum programming languages: Classical control, quantum control
- Probabilistic call by push value
- Metric reasoning about -terms: the general case
- On the termination problem for probabilistic higher-order recursive programs
- Mitigating multi-target attacks in hash-based signatures
- Program equivalence in a typed probabilistic call-by-need functional language
- On applicative similarity, sequentiality, and full abstraction
- Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and Applications
- Stochastic lambda calculus and monads of probability distributions
- Factorize factorization
- scientific article; zbMATH DE number 7566061 (Why is no real title available?)
- Stochastic \(\lambda\)-calculi: an extended abstract
- A lambda-calculus foundation for universal probabilistic programming
- Probabilistic Böhm trees and probabilistic separation
- Solvability in a probabilistic setting (invited talk)
- Confluence in probabilistic rewriting
- Distributive semantics for nondeterministic typed -calculi
- A probabilistic semantics for the pure \(\lambda\)-calculus
- Probabilistic operational semantics for the lambda calculus
- On quantum lambda calculi: a foundational perspective
- scientific article; zbMATH DE number 7559285 (Why is no real title available?)
- Lambda calculus and probabilistic computation
- A logic of knowledge and justifications, with an application to computational trust
- Simple types for probabilistic termination
- A rewriting theory for quantum -calculus
- Probabilistic approach to the lambda definability for fourth order types
- scientific article; zbMATH DE number 7559289 (Why is no real title available?)
- Boolean-valued semantics for the stochastic \(\lambda \)-calculus
- A deterministic rewrite system for the probabilistic \(\lambda\)-calculus
- Decomposing probabilistic lambda calculi
- Compositionality of Probabilistic Hennessy-Milner Logic through Structural Operational Semantics
- \textsc{qPCF}: a language for quantum circuit computations
- The vectorial \(\lambda\)-calculus
This page was built for publication: Probabilistic operational semantics for the lambda calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2905328)
