Functional Reachability
What is reachability in higher-order functional programs? We formulate reachability as a decision problem in the setting of the prototypical functional language PCF and show that even in the recursion-free fragment generated from a finite base type, several versions of the reachability problem are u...
| Үндсэн зохиолчид: | , , |
|---|---|
| Формат: | Conference item |
| Хэвлэсэн: |
2009
|
| _version_ | 1826290304721879040 |
|---|---|
| author | Ong, C Tzevelekos, N Soc, I |
| author_facet | Ong, C Tzevelekos, N Soc, I |
| author_sort | Ong, C |
| collection | OXFORD |
| description | What is reachability in higher-order functional programs? We formulate reachability as a decision problem in the setting of the prototypical functional language PCF and show that even in the recursion-free fragment generated from a finite base type, several versions of the reachability problem are undecidable from order 4 onwards, and several other versions are reducible to each other. We characterise a version of the reachability problem in terms of a new class of tree automata introduced by Stirling at FoSSaCS 2009 called Alternating Dependency Tree Automata (ADTA). As a corollary, we prove that the ADTA non-emptiness problem is undecidable, thus resolving an open problem raised by Stirling. However, by restricting to contexts constructible from a finite set of variable names, we show that the corresponding solution set of a given instance of the reachability problem is regular. Hence the relativised reachability problem is decidable. © 2009 IEEE. |
| first_indexed | 2024-03-07T02:42:08Z |
| format | Conference item |
| id | oxford-uuid:aad1e708-dbec-495f-8360-fbc85dd1c804 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T02:42:08Z |
| publishDate | 2009 |
| record_format | dspace |
| spelling | oxford-uuid:aad1e708-dbec-495f-8360-fbc85dd1c8042022-03-27T03:17:38ZFunctional ReachabilityConference itemhttp://purl.org/coar/resource_type/c_5794uuid:aad1e708-dbec-495f-8360-fbc85dd1c804Symplectic Elements at Oxford2009Ong, CTzevelekos, NSoc, IWhat is reachability in higher-order functional programs? We formulate reachability as a decision problem in the setting of the prototypical functional language PCF and show that even in the recursion-free fragment generated from a finite base type, several versions of the reachability problem are undecidable from order 4 onwards, and several other versions are reducible to each other. We characterise a version of the reachability problem in terms of a new class of tree automata introduced by Stirling at FoSSaCS 2009 called Alternating Dependency Tree Automata (ADTA). As a corollary, we prove that the ADTA non-emptiness problem is undecidable, thus resolving an open problem raised by Stirling. However, by restricting to contexts constructible from a finite set of variable names, we show that the corresponding solution set of a given instance of the reachability problem is regular. Hence the relativised reachability problem is decidable. © 2009 IEEE. |
| spellingShingle | Ong, C Tzevelekos, N Soc, I Functional Reachability |
| title | Functional Reachability |
| title_full | Functional Reachability |
| title_fullStr | Functional Reachability |
| title_full_unstemmed | Functional Reachability |
| title_short | Functional Reachability |
| title_sort | functional reachability |
| work_keys_str_mv | AT ongc functionalreachability AT tzevelekosn functionalreachability AT soci functionalreachability |