HackerPapers

arXiv:2307.14805cs.LO

Linear Termination over N is Undecidable

Fabian Mitterwallner, Aart Middeldorp, René Thiemann

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

Abstract

Recently it was shown that it is undecidable whether a term rewrite system can be proved terminating by a polynomial interpretation in the natural numbers. In this paper we show that this is also the case when restricting the interpretations to linear polynomials, as is often done in tools, and when only considering single-rule rewrite systems. What is more, the new undecidability proof is simpler than the previous one. We further show that polynomial termination over the rationals/reals is undecidable.

arXiv comments
Presented at WST 2023
Journal reference
DOI
Subjects
cs.LOLogic in Computer Science

On Hacker News

Linked by 1 identifiable commenter in 2 comments across 2 threads, from Oct 2023 to Oct 2023.

Comments linking this paper, per year.

Discussed in comments2 threads

  1. The deep link equating math proofs and computer programs 1 comment

    • Note this quote from the article. "One way to resolve the paradox, therefore, is to put these types into a hierarchy, so they can only contain elements of a “lower level” than themselves. Then a type can’t contain itself, which avoids the self-referentiality that creates the…

      nyrikkiView on HNParent context

  2. Language Models Represent Space and Time 1 comment

    • The lack of generally accepted definition for knowledge and intelligence makes these conversations difficult but the above post is important to remember. The paper has nothing to do with the common sense problem. While it is a preprint, I do wonder how useful this will be to…

      nyrikkiView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.