Recursive Definitions of Monadic Functions
Using standard domain-theoretic fixed-points, we present an approach for defining recursive functions that are formulated in monadic style. The method works both in the simple option monad and the state-exception monad of Isabelle/HOL's imperative programming extension, which results in a conve...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2010-12-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1012.4895v1 |
| _version_ | 1818790180445749248 |
|---|---|
| author | Alexander Krauss |
| author_facet | Alexander Krauss |
| author_sort | Alexander Krauss |
| collection | DOAJ |
| description | Using standard domain-theoretic fixed-points, we present an approach for defining recursive functions that are formulated in monadic style. The method works both in the simple option monad and the state-exception monad of Isabelle/HOL's imperative programming extension, which results in a convenient definition principle for imperative programs, which were previously hard to define. For such monadic functions, the recursion equation can always be derived without preconditions, even if the function is partial. The construction is easy to automate, and convenient induction principles can be derived automatically. |
| first_indexed | 2024-12-18T14:51:22Z |
| format | Article |
| id | doaj.art-e0098557189d46b2af1d497ebd0a1160 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-18T14:51:22Z |
| publishDate | 2010-12-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-e0098557189d46b2af1d497ebd0a11602022-12-21T21:04:10ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802010-12-0143Proc. PAR 201011310.4204/EPTCS.43.1Recursive Definitions of Monadic FunctionsAlexander KraussUsing standard domain-theoretic fixed-points, we present an approach for defining recursive functions that are formulated in monadic style. The method works both in the simple option monad and the state-exception monad of Isabelle/HOL's imperative programming extension, which results in a convenient definition principle for imperative programs, which were previously hard to define. For such monadic functions, the recursion equation can always be derived without preconditions, even if the function is partial. The construction is easy to automate, and convenient induction principles can be derived automatically.http://arxiv.org/pdf/1012.4895v1 |
| spellingShingle | Alexander Krauss Recursive Definitions of Monadic Functions Electronic Proceedings in Theoretical Computer Science |
| title | Recursive Definitions of Monadic Functions |
| title_full | Recursive Definitions of Monadic Functions |
| title_fullStr | Recursive Definitions of Monadic Functions |
| title_full_unstemmed | Recursive Definitions of Monadic Functions |
| title_short | Recursive Definitions of Monadic Functions |
| title_sort | recursive definitions of monadic functions |
| url | http://arxiv.org/pdf/1012.4895v1 |
| work_keys_str_mv | AT alexanderkrauss recursivedefinitionsofmonadicfunctions |