8

This is an example of a branching process. The behavior of a branching process depends on the expected number of children, which in your case is $1.25 > 1$. When this number is at most 1, the process gets extinct with probability 1. When the number is more than 1, it has a chance of surviving forever; the extinction probability is just what you calculated ...


7

There are plenty of classes of programming languages where all programs terminate. The most common form of enforcing termination is by way of types. The most well-developed theory of typing systems for terminating computation might be that of Barendregt's Lambda cube, which decomposes typing into three orthogonal axes: Parametric polymorphism Higher kinds ...


5

I think Turing's method is probably fine, but you are mistaken about why exactly the code you wrote, "terminates." First, note that this is not really (written as) a function at all. It is a self-referential value. And the reason the program terminates even though it's defined in it is that the program does not attempt to evaluate it fully. In this case, ...


4

Following Bellantoni & Cook's foundational work in A New Recursion-Theoretic Characterization of Polytime Functions, there's been a lot of work on simple characterizations of complexity classes by means of total languages, with strong connections to linear logic as Martin Berger notes in the comments. Building on this work, other complexity classes have ...


4

Short-circuit evaluation is based on lazy-evaluation (call-by-need evaluation) of the arguments of some function or operator. This is all described in various wikipedia articles. The idea is that the function call defers requesting evaluation of its arguments until they are actually needed, possibly never evaluating them if the computation may proceed ...


4

A big thing that is studied in higher type computability is infinite streams. Others have talked about hyper computation but this isn't quite the same. For starters the objects and functions studied in higher type computability are all things you can do in Haskell or some other such real programing language. These functions DO terminate in finite time thanks ...


3

This is a very succinct way of presenting the contradiction argument, and I strongly recommend you read a textbook on the topic, or some detailed explanations. There are tons of resources that explain this remarkable and beautiful argument, from many viewpoints. Still, to answer your question: denote by $Q$ the program you describe. Then $Q$ is a valid ...


3

I think you are really asking a question about the definition of the notion of well-foundedness. I think the notion of loop variants is a bit of a red herring here: I would argue that any reasonable definition of well-foundedness should enable proving that a loop is terminating iff there is a well-founded relation which acts as a variant for it, almost as a ...


3

Yes. This is possible. $t=1$ suffices. Take $$\begin{align*} f(m,n-1) &= Cm + D\\ f(m,n-2) &= f(m+v_{n-2},n-1) + 1 = Cm + C v_{n-2} + D + 1\\ f(m,n-3) &= f(m+v_{n-3},n-2) + 1 = Cm + C v_{n-3} + C v_{n-2} + D + 2\\ &\ldots\\ f(m,i) &= Cm + C v_{i} + \dots + C v_{n-2} + D + n-1-i \end{align*}$$ where we take the constant $C>0$ to be ...


3

Yes, there are plenty of models of computation on infinite data where computations go on forever. For example, ordinary finite automata can be adapted to deal with infinite strings, giving $\omega$-automata. However, it doesn't make sense to talk about such computations terminating since terminate means "end" and an infinite computation doesn't do that. ...


3

What you are describing is a notion of hypercomputation. Several ways of making sense of infinite computation are described in the Wikipedia article on hypercomputation. The approach of Hamkins and Lewis seems particularly popular. There is no need to invoke a cardinal-valued variable though; you can just have a plain old infinite loop.


2

Derek Elkins' comment solved my problem! Here's the solution I came up with: We create a seperate renaming function rename: Term -> nat -> nat -> Term, which assumes that the name to rename with is fresh. This makes it trivially terminating. Fixpoint rename (t:Term) (x y : nat): Term := match t with | TVar z => if beq_nat y z then TVar ...


2

Counterexample: $f(c) \rightarrow f(d)$ In general, there are some modularity theorems for termination and confluence that may apply if, e.g. your constants do not appear at all in any rule. There are probably some weaker assumptions that can make this work though.


2

This may take the form of a quantity which is asserted to decrease continually and vanish when the machine stops. Lambda calculus evaluation is a sequence of beta reduction steps. So for the lambda calculus (with or without types: types don't affect evaluation), you want a quantity (a positive integer) that decreases at each reduction step. Such a quantity ...


2

Indeed this is obvious. Now you need to "prove" it. The difficulty will depend on what definitions (and axioms) you assume when you say that "$f$ and $g$ can be implemented". Start by making these definitions explicit.


1

It's your exercise, so I'll let you answer it, but here is a hint. Consider the sequence of words visited by repeatedly applying the rewrite rule and its relationship to lexicographic order. Work through a few examples and see if you can form a conjecture.


1

Pushdown automata do not necessarily halt. They are not forced to read input each step, they can also do so-called $\lambda$-instructions where the tape is not advanced. Then we can have an infinite loop at a certain tape position. Likewise, linear bounded automata may loop, and do not always halt. However, they can be simulated by a Turing machine, which ...


1

No. The grammar is defined like this: G = (V,SIGMA, R, S) where V is your set of variables (non-terminals) and SIGMA is your alphabet (terminals). All the symbols you are allowed to use in the substitution of a rule are the union of V and SIGMA. If you simply cannot use a symbol out of that set, since it does not exists in the context of your grammar.


1

Hint: if you want to know whether $M$ accepts $w$, build a machine that replaces its input with $w$ and then does whatever $M$ does.


Only top voted, non community-wiki answers of a minimum length are eligible