# Questions tagged [termination]

The tag has no usage guidance.

15 questions
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 ...
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: ...
90 views

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 ...
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?
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: ...
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 ...
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 ...
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, ...
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 ...
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 ...