The continuity of monadic stream functions
Brouwer’s continuity principle states that all functions from infinite sequences of naturals to naturals are continuous, that is, for every sequence the result depends only on a finite initial segment. It is an intuitionistic axiom that is incompatible with classical mathematics. Recently Mart́ín Es...
| Main Authors: | , |
|---|---|
| Format: | Conference or Workshop Item |
| Language: | English |
| Published: |
ACM
2017
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/41715/ |
| _version_ | 1848796338394759168 |
|---|---|
| author | Capretta, Venanzio Fowler, Jonathan |
| author_facet | Capretta, Venanzio Fowler, Jonathan |
| author_sort | Capretta, Venanzio |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | Brouwer’s continuity principle states that all functions from infinite sequences of naturals to naturals are continuous, that is, for every sequence the result depends only on a finite initial segment. It is an intuitionistic axiom that is incompatible with classical mathematics. Recently Mart́ín Escardó proved that it is also inconsistent in type theory. We propose a reformulation of the continuity principle that may be more faithful to the original meaning by Brouwer. It applies to monadic streams, potentially unending sequences of values produced by steps triggered by a monadic action, possibly involving side effects. We consider functions on them that are uniform, in the sense that they operate in the same way independently of the particular monad that provides the specific side effects. Formally this is done by requiring a form of naturality in the monad. Functions on monadic streams have not only a foundational importance, but have also practical applications in signal processing and reactive programming. We give algorithms to determine the modulus of continuity of monadic stream functions and to generate dialogue trees for them (trees whose nodes and branches describe the interaction of the process with the environment). |
| first_indexed | 2025-11-14T19:46:24Z |
| format | Conference or Workshop Item |
| id | nottingham-41715 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-14T19:46:24Z |
| publishDate | 2017 |
| publisher | ACM |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-417152020-05-08T12:15:14Z https://eprints.nottingham.ac.uk/41715/ The continuity of monadic stream functions Capretta, Venanzio Fowler, Jonathan Brouwer’s continuity principle states that all functions from infinite sequences of naturals to naturals are continuous, that is, for every sequence the result depends only on a finite initial segment. It is an intuitionistic axiom that is incompatible with classical mathematics. Recently Mart́ín Escardó proved that it is also inconsistent in type theory. We propose a reformulation of the continuity principle that may be more faithful to the original meaning by Brouwer. It applies to monadic streams, potentially unending sequences of values produced by steps triggered by a monadic action, possibly involving side effects. We consider functions on them that are uniform, in the sense that they operate in the same way independently of the particular monad that provides the specific side effects. Formally this is done by requiring a form of naturality in the monad. Functions on monadic streams have not only a foundational importance, but have also practical applications in signal processing and reactive programming. We give algorithms to determine the modulus of continuity of monadic stream functions and to generate dialogue trees for them (trees whose nodes and branches describe the interaction of the process with the environment). ACM 2017-08-18 Conference or Workshop Item PeerReviewed application/pdf en https://eprints.nottingham.ac.uk/41715/1/monadic_continuity_LICS2017.pdf Capretta, Venanzio and Fowler, Jonathan (2017) The continuity of monadic stream functions. In: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'17), 20-23 Jun 2017, Reykjavik, Iceland. monadic stream function continuity type theory functional programming stream monad dialogue trees strategy trees |
| spellingShingle | monadic stream function continuity type theory functional programming stream monad dialogue trees strategy trees Capretta, Venanzio Fowler, Jonathan The continuity of monadic stream functions |
| title | The continuity of monadic stream functions |
| title_full | The continuity of monadic stream functions |
| title_fullStr | The continuity of monadic stream functions |
| title_full_unstemmed | The continuity of monadic stream functions |
| title_short | The continuity of monadic stream functions |
| title_sort | continuity of monadic stream functions |
| topic | monadic stream function continuity type theory functional programming stream monad dialogue trees strategy trees |
| url | https://eprints.nottingham.ac.uk/41715/ |