Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [termination]

The tag has no usage guidance.

4
votes
0answers
44 views

Inferring ranking functions in a general code graph with partial information

Let me define the notion of call graph: A program consists on a set of functions $f,g,h,\ldots$ where each function $n$ is as a mapping $n: D^l \to D^m$. Here $D$ is the datatype representing ...
1
vote
1answer
54 views

Stablishing termination of the construction of infinite stream with ranking functions

I'm working with Turing's paradigm to prove termination of programs by annotating functions with ranking functions and I encounter the following example: ...
2
votes
2answers
90 views

Inference of a measure for a decreasing chain

Given integers $v_0,\dots,v_{n-1} \in \mathbb{N}$, I want to find an integer $t>0$, a map $f:\mathbb{N} \times \{0,1,\dots,n-1\} \to \mathbb{N}^t$, and a well-founded order $>_t$ on $\mathbb{N}^...
1
vote
0answers
51 views

On the termination of mutually recursive functions

In Finding Lexicographic Orders for Termination Proofs in Isabelle/Holl the authors construct a method for proving termination of functions based on constructing a matrix that registers for each row ...
3
votes
0answers
22 views

Question about termination of term rewrite systems

Let $\mathcal{R} = (R, \Sigma)$ be a term rewrite system over a signature $\Sigma$ with set of basic rewrite rules $R$. It is known that $\mathcal{R}$ is terminating IF every basic rewrite rule $l \to ...
2
votes
1answer
25 views

Identifying/equating constants in a term rewrite system

Suppose we have a term rewrite system $\mathcal{R} = (R, \Sigma)$ with basic rewrite rules $R$ over a signature $\Sigma$. Suppose also that this rewrite system $\mathcal{R}$ is confluent and ...
0
votes
1answer
51 views

Type-0 grammar and terminal symbols

The question is pretty short, but I've been thinking about it quite some time: Are terminal symbols that are not in the defined alphabet still valid?
4
votes
1answer
66 views

Why does substitution terminate?

I'm formalizing some properties of lambda calculus in Coq and I have some problems proving termination of substitution. My terms are defined as: ...
1
vote
1answer
106 views

The set of turing machine that stops with input zero is not recursive

If M is a Turing Machine, consider the subset of $\mathbb{N}$ defined as: $$ \mathrm{ZTM} = \{ x \mid M_x(0)\downarrow \} $$ i.e. the set of 'indexes' of machines that halt on zero. It is possible ...
1
vote
1answer
21 views

Termination of a composition of terminating functions

Suppose there are two functions: $ f : X \rightarrow Y $ and $g : Y \rightarrow Z$ Both $g$ and $f$ can be implemented as algorithms that yield the correct result in a finite amount of time. It ...
3
votes
0answers
42 views

Termination of deterministic term rewriting

Consider a simple language: $$t ::= plus ~ t ~ t ~ | ~ gen ~ t ~ | ~ except ~ N ~ t ~ | ~ N$$ with N constructors plus, gen and except, N being the natural numbers, and $G = \{t_n\}$ a finite, ...
7
votes
2answers
211 views

What are the most expressive, terminating languages?

I'm less interested in languages where you can write almost anything, but then are required to write an accompanying proof that what you wrote terminates. I'm more interested in the design space of ...
10
votes
1answer
113 views

What is the chance that this code terminates?

I wrote this Python code, and wondered if it sometimes simply doesn't terminate (assuming we had infinite memory/time and no recursion depth limit). Intuitively you'd think it terminates, since at ...
-1
votes
1answer
157 views

Where to learn about Short-circuit evaluation? [closed]

I would like to implement short circuit evaluation logic in my code. And I want to know about the full details how it works? Ex: function a() {return true;} function b() {return false;} function c(...
4
votes
3answers
216 views

Termination in infinite-time

Does it make sense to speak of algorithms that take an infinite amount of time to terminate? In particular, suppose we have a loop with a bound function that is initially positive and is decreased ...