Termination and semantics of probabilistic lambda calculus
<p>This thesis gives a complete method for proving the almost sure termination of probabilistic programs, in a simply-typed higher-order language with continuous random variables and an explicit recursion construct. The method is based on supermartingales and ranking functions, which are a pro...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | English |
| Published: |
2024
|
| Subjects: |
| _version_ | 1824458707576029184 |
|---|---|
| author | Kenyon-Roberts, A |
| author2 | Ong, L |
| author_facet | Ong, L Kenyon-Roberts, A |
| author_sort | Kenyon-Roberts, A |
| collection | OXFORD |
| description | <p>This thesis gives a complete method for proving the almost sure termination of probabilistic programs, in a simply-typed higher-order language with continuous random variables and an explicit recursion construct. The method is based on supermartingales and ranking functions, which are a probabilistic version of a loop variant, as described in similar work by McIver, Morgan, Kaminski and Katoen in the setting of a first-order imperative language. The basic version of this method is extended in three ways. <em>Sparse ranking functions</em> permit more flexibility in how the ranking functions may be defined, so that a sparse ranking function only needs to be defined at a subset of program states, which makes providing ranking functions much more convenient. <em>Antitone ranking functions</em> have a weaker condition on the rate of decrease than the basic version of ranking functions, so that they can be applied to programs that terminate arbitrarily slowly. <em>Ranking functions with respect to alternative reduction strategies</em> allow the order in which the program is assumed to evaluate in the ranking function to deviate somewhat from the actual reduction strategy used, again making it more convenient to define ranking functions. All of these extensions may be combined, and it is proven that if a program has an antitone sparse ranking function with respect to any reduction strategy, it is almost surely terminating.</p>
<p>There is also an overview of probabilistic programming, with a particular focus on some of the many different ways of defining a formal semantics for probabilistic lambda calculus. The last extension of the ranking function method, relating to alternative reduction strategies, makes use of a novel variant on the operational trace-based semantics with a limited confluence result despite the random sampling. This confluent trace semantics may be of interest beyond just its application to proving almost sure termination.</p> |
| first_indexed | 2025-02-19T04:30:10Z |
| format | Thesis |
| id | oxford-uuid:89030a47-d234-49bf-9ae9-f215b96ad80e |
| institution | University of Oxford |
| language | English |
| last_indexed | 2025-02-19T04:30:10Z |
| publishDate | 2024 |
| record_format | dspace |
| spelling | oxford-uuid:89030a47-d234-49bf-9ae9-f215b96ad80e2024-12-23T06:54:21ZTermination and semantics of probabilistic lambda calculusThesishttp://purl.org/coar/resource_type/c_db06uuid:89030a47-d234-49bf-9ae9-f215b96ad80eLambda calculusProgramming languages (Electronic computers)--SemanticsComputer programs--TerminationEnglishHyrax Deposit2024Kenyon-Roberts, AOng, LKlin, BStaton, SKammar, O<p>This thesis gives a complete method for proving the almost sure termination of probabilistic programs, in a simply-typed higher-order language with continuous random variables and an explicit recursion construct. The method is based on supermartingales and ranking functions, which are a probabilistic version of a loop variant, as described in similar work by McIver, Morgan, Kaminski and Katoen in the setting of a first-order imperative language. The basic version of this method is extended in three ways. <em>Sparse ranking functions</em> permit more flexibility in how the ranking functions may be defined, so that a sparse ranking function only needs to be defined at a subset of program states, which makes providing ranking functions much more convenient. <em>Antitone ranking functions</em> have a weaker condition on the rate of decrease than the basic version of ranking functions, so that they can be applied to programs that terminate arbitrarily slowly. <em>Ranking functions with respect to alternative reduction strategies</em> allow the order in which the program is assumed to evaluate in the ranking function to deviate somewhat from the actual reduction strategy used, again making it more convenient to define ranking functions. All of these extensions may be combined, and it is proven that if a program has an antitone sparse ranking function with respect to any reduction strategy, it is almost surely terminating.</p> <p>There is also an overview of probabilistic programming, with a particular focus on some of the many different ways of defining a formal semantics for probabilistic lambda calculus. The last extension of the ranking function method, relating to alternative reduction strategies, makes use of a novel variant on the operational trace-based semantics with a limited confluence result despite the random sampling. This confluent trace semantics may be of interest beyond just its application to proving almost sure termination.</p> |
| spellingShingle | Lambda calculus Programming languages (Electronic computers)--Semantics Computer programs--Termination Kenyon-Roberts, A Termination and semantics of probabilistic lambda calculus |
| title | Termination and semantics of probabilistic lambda calculus |
| title_full | Termination and semantics of probabilistic lambda calculus |
| title_fullStr | Termination and semantics of probabilistic lambda calculus |
| title_full_unstemmed | Termination and semantics of probabilistic lambda calculus |
| title_short | Termination and semantics of probabilistic lambda calculus |
| title_sort | termination and semantics of probabilistic lambda calculus |
| topic | Lambda calculus Programming languages (Electronic computers)--Semantics Computer programs--Termination |
| work_keys_str_mv | AT kenyonrobertsa terminationandsemanticsofprobabilisticlambdacalculus |