Document Open Access Logo

Term Rewriting Characterisation of LOGSPACE for Finite and Infinite Data

Author Lukasz Czajka

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2018.13.pdf
  • Filesize: 432 kB
  • 19 pages

Document Identifiers

Author Details

Lukasz Czajka
  • University of Copenhagen, Denmark

Funding

  • Czajka, Lukasz: Supported by Marie Skłodowska-Curie action "InfTy", program H2020-MSCA-IF-2015, number 704111.

Cite As Get BibTex

Lukasz Czajka. Term Rewriting Characterisation of LOGSPACE for Finite and Infinite Data. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.FSCD.2018.13

Abstract

We show that LOGSPACE is characterised by finite orthogonal tail-recursive cons-free constructor term rewriting systems, contributing to a line of research initiated by Neil Jones. We describe a LOGSPACE algorithm which computes constructor normal forms. This algorithm is used in the proof of our main result: that simple stream term rewriting systems characterise LOGSPACE-computable stream functions as defined by Ramyaa and Leivant. This result concerns characterising logarithmic-space computation on infinite streams by means of infinitary rewriting.

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity theory and logic
  • Theory of computation → Equational logic and rewriting
Keywords
  • LOGSPACE
  • implicit complexity
  • term rewriting
  • infinitary rewriting
  • streams

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1999. Google Scholar
  2. G. Bonfante. Some programming languages for LOGSPACE and PTIME. In AMAST 2006, pages 66-80, 2006. Google Scholar
  3. D. de Carvalho and J. G. Simonsen. An implicit characterization of the polynomial-time decidable sets by cons-free rewriting. In RTA-TLCA 2014, pages 179-193, 2014. Google Scholar
  4. Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra Silva. A coinductive framework for infinitary rewriting and equational reasoning. In RTA 2015, 2015. Google Scholar
  5. Jörg Endrullis and Andrew Polonsky. Infinitary rewriting coinductively. In TYPES 2011, pages 16-27, 2011. Google Scholar
  6. Juris Hartmanis. On non-determinancy in simple computing devices. Acta Informatica, 1(4):336-344, Dec 1972. Google Scholar
  7. N. D. Jones. LOGSPACE and PTIME characterized by programming languages. Theor. Comput. Sci., 228(1-2):151-174, 1999. Google Scholar
  8. N. D. Jones. The expressive power of higher-order types or, life without CONS. J. Funct. Program., 11(1):5-94, 2001. Google Scholar
  9. Neil D. Jones. Computability and complexity - from a programming perspective. Foundations of computing series. MIT Press, 1997. Google Scholar
  10. C. Kop. On first-order cons-free term rewriting and PTIME. In DICE 2016, 2016. Google Scholar
  11. C. Kop and J. G. Simonsen. Complexity hierarchies and higher-order cons-free rewriting. In FSCD 2016, pages 23:1-23:18, 2016. Google Scholar
  12. C. Kop and J. G. Simonsen. The power of non-determinism in higher-order implicit complexity. In ESOP 2017, pages 668-695, 2017. Google Scholar
  13. D. Leivant and R. Ramyaa. The computational contents of ramified corecurrence. In FoSSaCS 2015, pages 422-435, 2015. Google Scholar
  14. R. Ramyaa and D. Leivant. Ramified corecurrence and logspace. Electr. Notes Theor. Comput. Sci., 276:247-261, 2011. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact