Semi-continuous Sized Types and Termination
Some type-based approaches to termination use sized types: an ordinal bound for the size of a data structure is stored in its type. A recursive function over a sized type is accepted if it is visible in the type system that recursive calls occur just at a smaller size. This approach is only sound if...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2008-04-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1236/pdf |
| _version_ | 1827323045042192384 |
|---|---|
| author | Andreas Abel |
| author_facet | Andreas Abel |
| author_sort | Andreas Abel |
| collection | DOAJ |
| description | Some type-based approaches to termination use sized types: an ordinal bound
for the size of a data structure is stored in its type. A recursive function
over a sized type is accepted if it is visible in the type system that
recursive calls occur just at a smaller size. This approach is only sound if
the type of the recursive function is admissible, i.e., depends on the size
index in a certain way. To explore the space of admissible functions in the
presence of higher-kinded data types and impredicative polymorphism, a
semantics is developed where sized types are interpreted as functions from
ordinals into sets of strongly normalizing terms. It is shown that upper
semi-continuity of such functions is a sufficient semantic criterion for
admissibility. To provide a syntactical criterion, a calculus for
semi-continuous functions is developed. |
| first_indexed | 2024-04-25T01:38:22Z |
| format | Article |
| id | doaj.art-faa27256632d41a6a54282f590c1fefd |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:38:22Z |
| publishDate | 2008-04-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-faa27256632d41a6a54282f590c1fefd2024-03-08T08:51:49ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742008-04-01Volume 4, Issue 210.2168/LMCS-4(2:3)20081236Semi-continuous Sized Types and TerminationAndreas AbelSome type-based approaches to termination use sized types: an ordinal bound for the size of a data structure is stored in its type. A recursive function over a sized type is accepted if it is visible in the type system that recursive calls occur just at a smaller size. This approach is only sound if the type of the recursive function is admissible, i.e., depends on the size index in a certain way. To explore the space of admissible functions in the presence of higher-kinded data types and impredicative polymorphism, a semantics is developed where sized types are interpreted as functions from ordinals into sets of strongly normalizing terms. It is shown that upper semi-continuity of such functions is a sufficient semantic criterion for admissibility. To provide a syntactical criterion, a calculus for semi-continuous functions is developed.https://lmcs.episciences.org/1236/pdfcomputer science - programming languagescomputer science - logic in computer scienced.1.1f.3.2f.4.1 |
| spellingShingle | Andreas Abel Semi-continuous Sized Types and Termination Logical Methods in Computer Science computer science - programming languages computer science - logic in computer science d.1.1 f.3.2 f.4.1 |
| title | Semi-continuous Sized Types and Termination |
| title_full | Semi-continuous Sized Types and Termination |
| title_fullStr | Semi-continuous Sized Types and Termination |
| title_full_unstemmed | Semi-continuous Sized Types and Termination |
| title_short | Semi-continuous Sized Types and Termination |
| title_sort | semi continuous sized types and termination |
| topic | computer science - programming languages computer science - logic in computer science d.1.1 f.3.2 f.4.1 |
| url | https://lmcs.episciences.org/1236/pdf |
| work_keys_str_mv | AT andreasabel semicontinuoussizedtypesandtermination |