Induction by Coinduction and Control Operators in Call-by-Name
This paper studies emulation of induction by coinduction in a call-by-name language with control operators. Since it is known that call-by-name programming languages with control operators cannot have general initial algebras, interaction of induction and control operators is often restricted to eff...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2013-09-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1309.1258v1 |
| _version_ | 1818936692554334208 |
|---|---|
| author | Yoshihiko Kakutani Daisuke Kimura |
| author_facet | Yoshihiko Kakutani Daisuke Kimura |
| author_sort | Yoshihiko Kakutani |
| collection | DOAJ |
| description | This paper studies emulation of induction by coinduction in a call-by-name language with control operators. Since it is known that call-by-name programming languages with control operators cannot have general initial algebras, interaction of induction and control operators is often restricted to effect-free functions. We show that some class of such restricted inductive types can be derived from full coinductive types by the power of control operators. As a typical example of our results, the type of natural numbers is represented by the type of streams. The underlying idea is a counterpart of the fact that some coinductive types can be expressed by inductive types in call-by-name pure language without side-effects. |
| first_indexed | 2024-12-20T05:40:06Z |
| format | Article |
| id | doaj.art-19ea6250a7da4c67b1eeea6403002653 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-20T05:40:06Z |
| publishDate | 2013-09-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-19ea6250a7da4c67b1eeea64030026532022-12-21T19:51:28ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802013-09-01127Proc. COS 201310111210.4204/EPTCS.127.7Induction by Coinduction and Control Operators in Call-by-NameYoshihiko KakutaniDaisuke KimuraThis paper studies emulation of induction by coinduction in a call-by-name language with control operators. Since it is known that call-by-name programming languages with control operators cannot have general initial algebras, interaction of induction and control operators is often restricted to effect-free functions. We show that some class of such restricted inductive types can be derived from full coinductive types by the power of control operators. As a typical example of our results, the type of natural numbers is represented by the type of streams. The underlying idea is a counterpart of the fact that some coinductive types can be expressed by inductive types in call-by-name pure language without side-effects.http://arxiv.org/pdf/1309.1258v1 |
| spellingShingle | Yoshihiko Kakutani Daisuke Kimura Induction by Coinduction and Control Operators in Call-by-Name Electronic Proceedings in Theoretical Computer Science |
| title | Induction by Coinduction and Control Operators in Call-by-Name |
| title_full | Induction by Coinduction and Control Operators in Call-by-Name |
| title_fullStr | Induction by Coinduction and Control Operators in Call-by-Name |
| title_full_unstemmed | Induction by Coinduction and Control Operators in Call-by-Name |
| title_short | Induction by Coinduction and Control Operators in Call-by-Name |
| title_sort | induction by coinduction and control operators in call by name |
| url | http://arxiv.org/pdf/1309.1258v1 |
| work_keys_str_mv | AT yoshihikokakutani inductionbycoinductionandcontroloperatorsincallbyname AT daisukekimura inductionbycoinductionandcontroloperatorsincallbyname |