Functions with local state: regularity and undecidability
We study programs of a finitary ML-like language RML<sub>f</sub> with ground-type references. RML<sub>f</sub> permits the use of functions with locally declared variables that remain private and persist from one use of the function to the next. Using game semantics we show th...
| Main Author: | |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
Elsevier
2005
|
| Subjects: |
| Summary: | We study programs of a finitary ML-like language RML<sub>f</sub> with ground-type references. RML<sub>f</sub> permits the use of functions with locally declared variables that remain private and persist from one use of the function to the next. Using game semantics we show that this leads to undecidability of program equivalence already at second order. We also examine the extent to which this feature can be captured by regular languages. This gives a decidability result for a second-order fragment RML<sub>f</sub><sup>-</sup> of RML<sub>f</sub>, which comprises many examples studied in the literature. |
|---|