Ramified corecurrence and logspace.

*(English)*Zbl 1342.68139
Mislove, Michael (ed.) et al., Proceedings of the 27th conference on the mathematical foundations of programming semantics (MFPS XXVII), Pittsburgh, PA, USA, May 25–28, 2011. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 276, 247-261 (2011).

Summary: Ramified recurrence over free algebras has been used over the last two decades to provide machine-independent characterizations of major complexity classes. We consider here ramification for the dual setting, referring to coinductive data and corecurrence rather than inductive data and recurrence.

Whereas ramified recurrence is related basically to feasible time (PTime) complexity, we show here that ramified corecurrence is related fundamentally to feasible space. Indeed, the 2-tier ramified corecursive functions are precisely the functions over streams computable in logarithmic space. Here we define the complexity of computing over streams in terms of the output rather than the input, i.e. the complexity of computing the \(n\)-th entry of the output as a function of \(n\). The class of stream functions computable in logspace seems to be of independent interest, both theoretical and practical.

We show that a stream function is definable by ramified corecurrence in two tiers iff it is computable by a transducer on streams that operates in space logarithmic in the position of the output symbol being computed. A consequence is that the two-tier ramified corecursive functions over finite streams are precisely the logspace functions, in the usual sense.

For the entire collection see [Zbl 1281.68036].

Whereas ramified recurrence is related basically to feasible time (PTime) complexity, we show here that ramified corecurrence is related fundamentally to feasible space. Indeed, the 2-tier ramified corecursive functions are precisely the functions over streams computable in logarithmic space. Here we define the complexity of computing over streams in terms of the output rather than the input, i.e. the complexity of computing the \(n\)-th entry of the output as a function of \(n\). The class of stream functions computable in logspace seems to be of independent interest, both theoretical and practical.

We show that a stream function is definable by ramified corecurrence in two tiers iff it is computable by a transducer on streams that operates in space logarithmic in the position of the output symbol being computed. A consequence is that the two-tier ramified corecursive functions over finite streams are precisely the logspace functions, in the usual sense.

For the entire collection see [Zbl 1281.68036].

##### MSC:

68Q15 | Complexity classes (hierarchies, relations among complexity classes, etc.) |

##### Keywords:

coinductive data; stream automata; corecurrence; lazy corecurrence; ramification; logarithmic space; implicit computational complexity
PDF
BibTeX
XML
Cite

\textit{R. Ramyaa} and \textit{D. Leivant}, Electron. Notes Theor. Comput. Sci. 276, 247--261 (2011; Zbl 1342.68139)

Full Text:
DOI

##### References:

[1] | Allouche, J.P.; Shallit, J., Automatic sequences: theory, applications, generalizations, (2003), Cambridge University Press, pages 152-153 |

[2] | Stephen Bellantoni. Predicative recursion and computational complexity. PhD thesis, University of Toronto, 1992. · Zbl 0766.68037 |

[3] | Bellantoni, Stephen; Cook, Stephen, A new recursion-theoretic characterization of the poly-time functions, Computational complexity, 2, 97-110, (1992) · Zbl 0766.68037 |

[4] | Guillaume Bonfante. Some programming languages for logspace and ptime. In AMAST, pages 66-80, 2006. · Zbl 1236.68074 |

[5] | Michael J. Burrell, Robin Cockett, and Brian F. Redmond. Pola: a language for ptime programming. In Logic and Computational Complexity, Workshop Proceedings, 2009. |

[6] | Clote, Peter; Takeuti, Gaisi, Bounded arithmetic for nc, alogtime, l and nl, Ann. pure appl. logic, 56, 1-3, 73-117, (1992) · Zbl 0772.03028 |

[7] | Cook, Stephen A.; Rackoff, Charles, Space lower bounds for maze threadability on restricted machines, SIAM J. comput., 9, 3, 636-652, (1980) · Zbl 0445.68038 |

[8] | Cook, Stephen A.; Urquhart, Alasdair, Functional interpretations of feasible constructive arithemtic, Annals of pure and applied logic, 63, 103-200, (1993) · Zbl 0780.03026 |

[9] | Hugo Férée, Emmanuel Hainry, Mathieu Hoyrup, and Romain Péchoux. Interpretation of stream programs: Characterizing type 2 polynomial time complexity. In ISAAC, pages 291-303, 2010. · Zbl 1311.03068 |

[10] | Gaboardi, Marco; Péchoux, Romain, Global and local space properties of stream programs, (), 51-66 · Zbl 1305.68055 |

[11] | Hartmanis, Juris, On non-determinancy in simple computing devices, Acta inf., 1, 336-344, (1972) · Zbl 0229.68014 |

[12] | Jones, Neil D., Logspace and ptime characterized by programming languages, Theor. comput. sci., 228, 151-174, (October 1999) |

[13] | Kristiansen, Lars, Neat function algebraic characterizations of logspace and linspace, Computational complexity, 14, 72-88, (2005) · Zbl 1161.68477 |

[14] | Leivant, Daniel, Ramified recurrence and computational complexity I: word recurrence and poly-time, (), 320-343 · Zbl 0844.03024 |

[15] | Leivant, Daniel; Marion, Jean-Yves, Ramified recurrence and computational complexity ii: substitution and poly-space, (), 486-500 · Zbl 1044.03526 |

[16] | Lind, John; Meyer, Albert R., A characterization of log-space computable functions, SIGACT news, 5, 26-29, (1973) |

[17] | Peter Møller Neergaard. A functional language for logarithmic space. In APLAS, pages 311-326, 2004. · Zbl 1116.68377 |

[18] | Oitavem, Isabel, Logspace without bounds, (), 355-362 · Zbl 1233.03047 |

[19] | Ramyaa Ramyaa and Daniel Leivant. Feasible functions over co-inductive data. In Workshop on Logic, Language, Information and Computation, pages 191-203, 2010. · Zbl 1305.68088 |

[20] | Reutenauer, Christophe, Subsequential functions: characterizations, minimization, examples, (), 62-79 · Zbl 0735.68001 |

[21] | Rutten, Jan J.M.M., Automata coinduction (an exercise in coalgebra), (), 194-218 · Zbl 0940.68085 |

[22] | Walter J. Savitch and Paul M.B. Vitányi. Linear time simulation of multihead turing machines with head-to-head jumps. In ICALP, pages 453-464, 1977. · Zbl 0353.68074 |

[23] | Ulrich Schöpp. Stratified bounded affine logic for logarithmic space. In LICS, pages 411-420, 2007. |

[24] | Schütte, Kurt, Proof theory, (1977), Springer-Verlag Berlin · Zbl 0367.02012 |

[25] | Uustalu, Tarmo; Vene, Varmo, Primitive (co)recursion and course-of-value (co)iteration, categorically, Informatica, lith. acad. sci., 10, 5-26, (1999) · Zbl 0935.68011 |

[26] | Varmo Vene and Tarmo Uustalu. Functional programming with apomorphisms (corecursion). In Ninth Nordic Workshop on Programming Theory, 1998. · Zbl 0963.68028 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.