on termination

11 views
Skip to first unread message

Cagdas Ozgenc

unread,
May 8, 2003, 2:06:22 AM5/8/03
to Haskell Cafe List
Greetings.
 
This may be a little off topic, but I could not get much response from comp.theory, so here it goes:
 
Is it possible to have a programming language that can be used to produce only the programs that terminate, but at the same time decide all recursive languages? Or does such limitation automatically reduce the class of languages that such a programming language decide to primitive-recursive?
 
Perhaps, I couldn't explain it very clearly. I suppose another way of saying this is: Is there a strongly normalizing system that can decide the class of recursive languages? Perhaps something less strong than a Turing Machine, for example deciding all recursive languages but not recognizing any recursively enumerable languages.
 
Thanks

Andrew J Bromage

unread,
May 8, 2003, 2:20:22 AM5/8/03
to Cagdas Ozgenc, Haskell Cafe List
G'day.

On Thu, May 08, 2003 at 09:05:25AM +0300, Cagdas Ozgenc wrote:

> Is it possible to have a programming language that can be used to
> produce only the programs that terminate, but at the same time decide
> all recursive languages? Or does such limitation automatically reduce
> the class of languages that such a programming language decide to
> primitive-recursive?

I don't know if this answers your question, but the class of primitive
recursive programs is not the largest class of provably terminating
programs there is.

For example, I can very easily produce a programming language which
consists of primitive recursive programs plus these five other specific
programs which I happen to know always terminate because I proved
it by other means.

Cheers,
Andrew Bromage
_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Cagdas Ozgenc

unread,
May 8, 2003, 3:40:18 AM5/8/03
to Haskell Cafe List

> I don't know if this answers your question, but the class of primitive
> recursive programs is not the largest class of provably terminating
> programs there is.
>
> For example, I can very easily produce a programming language which
> consists of primitive recursive programs plus these five other specific
> programs which I happen to know always terminate because I proved
> it by other means.

That's a good example. So how much can we expand this class? Is it possible
to cover all recursive languages, or is there a theorem that says this is
not possible?

Peter Gammie

unread,
May 8, 2003, 4:08:21 AM5/8/03
to Cagdas Ozgenc, Haskell Cafe List
> That's a good example. So how much can we expand this class? Is it possible
> to cover all recursive languages, or is there a theorem that says this is
> not possible?

The class of recursive (total) functions is not recursively enumerable,
i.e. not acceptable by a Turing machine. This result can be found in any
textbook on recursive function theory (ask me off list and I'll dig up a
reference).

More interestingly, it is possible to (uniformly) define classes of total
functions that are strictly larger than the primitive recursive class - in
particular, this is what type theorists spend a lot of time doing. (See,
for example, Simon Thompson's book on Type Theory and Functional
Programming.)

Now, a question of my own: is it possible to uniformly define a class of
functions that have a non-trivial decidable halting predicate? The notion
of "uniform" is up for argument, but i want to rule out examples like
Andrew's that involve combining classes in trivial ways.

cheers
peter

Cagdas Ozgenc

unread,
May 8, 2003, 4:44:20 AM5/8/03
to Haskell Cafe List

> The class of recursive (total) functions is not recursively enumerable,
> i.e. not acceptable by a Turing machine. This result can be found in any
> textbook on recursive function theory (ask me off list and I'll dig up a
> reference).

You lost me there. I thought recursive class is a subset of recursively
enumerable class. Perhaps you are referring to a special case.

> More interestingly, it is possible to (uniformly) define classes of total
> functions that are strictly larger than the primitive recursive class - in
> particular, this is what type theorists spend a lot of time doing. (See,
> for example, Simon Thompson's book on Type Theory and Functional
> Programming.)

I have skimmed through the following work.

http://www.math.chalmers.se/~bove/Papers/phd_thesis_abs.html

She claims that it is not possible syntactically detect termination, if the
recursion is not based on smaller components at each turn. But I think she
doesn't supply a proof for that.

> Now, a question of my own: is it possible to uniformly define a class of
> functions that have a non-trivial decidable halting predicate? The notion
> of "uniform" is up for argument, but i want to rule out examples like
> Andrew's that involve combining classes in trivial ways.

You lost me once again. What do you mean, could you please eloborate?

Peter Gammie

unread,
May 8, 2003, 6:16:19 AM5/8/03
to Cagdas Ozgenc, Haskell Cafe List
On Thu, 8 May 2003, Cagdas Ozgenc wrote:

> > The class of recursive (total) functions is not recursively enumerable,
> > i.e. not acceptable by a Turing machine. This result can be found in any
> > textbook on recursive function theory (ask me off list and I'll dig up a
> > reference).
>
> You lost me there. I thought recursive class is a subset of recursively
> enumerable class. Perhaps you are referring to a special case.

No, I am saying that you cannot write a program that runs on a Turing
machine that accepts all and only (some representation of) the class of
total functions. You can, of course, write programs that accept subsets of
this class (e.g. the primitive recursive functions) or all of this class
and some more (e.g. Turing-computable functions, incidentally including
some partial functions along the way).

Tony Hoare wrote a paper about this that you might find interesting:

http://portal.acm.org/citation.cfm?id=356606&coll=portal&dl=ACM&CFID=10349987&CFTOKEN=44706211#FullText

> > More interestingly, it is possible to (uniformly) define classes of total
> > functions that are strictly larger than the primitive recursive class - in
> > particular, this is what type theorists spend a lot of time doing. (See,
> > for example, Simon Thompson's book on Type Theory and Functional
> > Programming.)
>
> I have skimmed through the following work.
>
> http://www.math.chalmers.se/~bove/Papers/phd_thesis_abs.html
>
> She claims that it is not possible syntactically detect termination, if the
> recursion is not based on smaller components at each turn. But I think she
> doesn't supply a proof for that.

I believe this statement as it stands is not true; there are functions
that can be proved terminating but do not uniformly reduce the size of an
argument. (Does Ackermann's function serve as a counter example?) Suffice
it to say that Ana's condition is sufficient but not necessary, and is
used in practice as it can be automated. See the work done on termination
analysis in Mercury for variations on this theme:

http://citeseer.nj.nec.com/speirs97termination.html

> > Now, a question of my own: is it possible to uniformly define a class of
> > functions that have a non-trivial decidable halting predicate? The notion
> > of "uniform" is up for argument, but i want to rule out examples like
> > Andrew's that involve combining classes in trivial ways.
>
> You lost me once again. What do you mean, could you please eloborate?

OK:

1. The primitive recursive functions have a trivial termination predicate,
viz "true". This is also the case for the type theorists' systems I
have seen.

2. The Turing partially-computable functions have an undecidable
termination predicate.

What I want: a class of functions that don't all terminate, don't all not
terminate, and furthermore I can tell how a given element of the class
will behave without running it. It must have at least some expressiveness;
this is up for grabs, but it'll have to encompass at least primitive
recursion to be interesting.

Utility? Absolutely none. ;-)

cheers
peter

Doaitse Swierstra

unread,
May 8, 2003, 7:10:20 AM5/8/03
to Peter Gammie, Doaitse Swierstra, Cagdas Ozgenc, Haskell Cafe List
You may want to look at the large body of work hat has been done on
termination in rewrite systems, where many classes and properties have
been identified over the years. I am not an expert but:

The termination hierarchy for term rewriting,
Applicable Algebra in Engineering, Communication and Computing, 2001,
volume 12, pages 3-19

might be a good starting point,

Doaitse Swierstra


On donderdag, mei 8, 2003, at 12:15 Europe/Amsterdam, Peter Gammie
wrote:

Cagdas Ozgenc

unread,
May 8, 2003, 8:17:19 AM5/8/03
to Haskell Cafe List
I have read books/articles on rewriting systems. All of them talk about how
to prove termination and confluence, but none of them seem to generalize and
present the big picture. I don't really care about the properties of a
particular rewriting system. I am looking for milestone results. Let me see
if I can acquire the reference you pointed, is it available on the Internet?


> You may want to look at the large body of work hat has been done on
> termination in rewrite systems, where many classes and properties have
> been identified over the years. I am not an expert but:
>
> The termination hierarchy for term rewriting,
> Applicable Algebra in Engineering, Communication and Computing, 2001,
> volume 12, pages 3-19
>
> might be a good starting point,
>
> Doaitse Swierstra
>

Eray Ozkural

unread,
May 8, 2003, 9:27:12 AM5/8/03
to Cagdas Ozgenc, Haskell Cafe List
On Thursday 08 May 2003 09:05, Cagdas Ozgenc wrote:
> Is it possible to have a programming language that can be used to produce
> only the programs that terminate, but at the same time decide all recursive
> languages? Or does such limitation automatically reduce the class of
> languages that such a programming language decide to primitive-recursive?

I'm not sure if that's theoretically possible. A recursive language requires
more than an LBA for recognition. But then the new edition of Cindrella book
says when you use a polynomial-bounded TM it's not guaranteed to halt. I
pondered the same question last year but when I couldn't find an answer
easily I gave up :)

Is your intention to design such a programming language or to make a
mindblowing proof?

Maybe it's better to start with subsets of recursive languages. DL people are
dealing with decidable subsets of FOL, that might be interesting. Ouch, the
thought of all recursive sets gave me a headache (^_-)

Cheers,

--
Eray Ozkural (exa) <er...@cs.bilkent.edu.tr>
Comp. Sci. Dept., Bilkent University, Ankara KDE Project: http://www.kde.org
www: http://www.cs.bilkent.edu.tr/~erayo Malfunction: http://mp3.com/ariza
GPG public key fingerprint: 360C 852F 88B0 A745 F31B EA0F 7C07 AE16 874D 539C

Andrew J Bromage

unread,
May 8, 2003, 10:30:21 PM5/8/03
to Peter Gammie, Haskell Cafe List
G'day all.

On Thu, May 08, 2003 at 06:07:44PM +1000, Peter Gammie wrote:

> Now, a question of my own: is it possible to uniformly define a class of
> functions that have a non-trivial decidable halting predicate? The notion
> of "uniform" is up for argument, but i want to rule out examples like
> Andrew's that involve combining classes in trivial ways.

The Mercury group did some work on this as a static analysis. Have a
look for all papers with "termination analysis" in the title:

http://www.cs.mu.oz.au/research/mercury/information/papers.html

Unfortunately this work is probably no use for Haskell, as they all
rely on data structures not being infinite or cyclic (which they are
in any logic language which features an occurs check or statically
computable equivalent).

Cheers,
Andrew Bromage

Andrew J Bromage

unread,
May 8, 2003, 10:39:18 PM5/8/03
to Peter Gammie, Cagdas Ozgenc, Haskell Cafe List
G'day all.

On Thu, May 08, 2003 at 08:15:11PM +1000, Peter Gammie wrote:

> Utility? Absolutely none. ;-)

Not true. The Mercury group did this analysis for a reason, namely,
that the transformation:

p :- q, r.

becomes

p :- r, q.

preserves static semantics in a declarative logic language, however
it does not preserve operational semantics unless r always terminates.

I suppose this is somewhat analogous to strictness analysis or other
analyses designed to preserve full laziness in Haskell.

Cheers,
Andrew Bromage

Peter Gammie

unread,
May 8, 2003, 10:39:49 PM5/8/03
to Andrew J Bromage, Haskell Cafe List
On Fri, 9 May 2003, Andrew J Bromage wrote:

> On Thu, May 08, 2003 at 06:07:44PM +1000, Peter Gammie wrote:
>
> > Now, a question of my own: is it possible to uniformly define a class of
> > functions that have a non-trivial decidable halting predicate? The notion
> > of "uniform" is up for argument, but i want to rule out examples like
> > Andrew's that involve combining classes in trivial ways.
>
> The Mercury group did some work on this as a static analysis. Have a
> look for all papers with "termination analysis" in the title:
>
> http://www.cs.mu.oz.au/research/mercury/information/papers.html
>
> Unfortunately this work is probably no use for Haskell, as they all
> rely on data structures not being infinite or cyclic (which they are
> in any logic language which features an occurs check or statically
> computable equivalent).

To flog the horse a bit further: this isn't what i'm looking for, as there
are predicates that do terminate and fail to be identified as such.
(Putting it another way, the termination check is incomplete - as all such
checks must be for a Turing-complete language.) I recall Harald reckoning
their check is adequate for 80% of the predicates in the compiler, so it
is impressive even so.

A friend pointed me to David Turner's page on strong functional
programming:

http://www.cs.ukc.ac.uk/people/staff/dat/esfp.html

that seems related to what we're discussing.

cheers
peter

Peter Gammie

unread,
May 8, 2003, 10:46:22 PM5/8/03
to Andrew J Bromage, Haskell Cafe List
On Fri, 9 May 2003, Andrew J Bromage wrote:

> On Thu, May 08, 2003 at 08:15:11PM +1000, Peter Gammie wrote:
>
> > Utility? Absolutely none. ;-)
>
> Not true. The Mercury group did this analysis for a reason, namely,
> that the transformation:
> p :- q, r.
>
> becomes
>
> p :- r, q.
>
> preserves static semantics in a declarative logic language, however
> it does not preserve operational semantics unless r always terminates.

argh! having a language that satisfies my constraints is pretty useless;
in practice I'd expect you're better off going for Turing completeness +
analysis (ala Mercury, incomplete) or Turing incompleteness + trivial
termination predicate (ala traditional Type Theory - not to belittle the
efforts that go into termination/totality proofs, or expressing programs
in their languages.).

cheers
peter

ol...@pobox.com

unread,
May 8, 2003, 11:03:17 PM5/8/03
to pe...@cse.unsw.edu.au, haskel...@haskell.org

Peter Gammie wrote:
> What I want: a class of functions that don't all terminate, don't all not
> terminate, and furthermore I can tell how a given element of the class
> will behave without running it. It must have at least some expressiveness;
> this is up for grabs, but it'll have to encompass at least primitive
> recursion to be interesting.

Let us consider a first-order language of functions defined with the
help of addition, multiplication, branching-on-zero, and NPFIX.
Functional applications are allowed provided they use the names of
previously defined functions. (NPFIX n) is the n-th Church numeral (aka fold)
NPFIX n f seed --> f (f ... (f seed)) n times (n>=0)
seed otherwise
The second argument of NPFIX is the name of a previously defined
function (a known name, a functional constant). The domain of our
functions consists of integers and a special value 'undefined' (to be
called NaN for short). The reduction rules are as usual, with an
addition
NaN + x -> NaN + x for any x, etc.
That is, any operation with NaN leads to non-termination.

The language obviously includes every primitive recursive function.
There are terminating expressions (any expression that never directly
or indirectly mentions NaN always terminates). There are obviously
non-terminating functions, such as f(x) = x + NaN.

It is also clear that the halting predicate for our language is
decidable. Given an expressing, we examine it and the body of all
involved functions. If we don't find any NaN, we yield TRUE. If we
find a NaN, we "abstractly" interpret our expression. That is, we
execute it step by step until we come across a step that tries to add,
compare, multiply NaN. At this point we yield FALSE. If our abstract
interpreter halts, we yield TRUE. Obviously our abstract interpreter
is just the concrete interpreter with one small change. Because any
sequence of NaN-free reductions in our language is a sequence of
reductions for some primitive recursive function, such sequence must
terminate.

We're a bit running afoul of the requirement:

> I can tell how a given element of the class will behave without
> running it

but then, a decision procedure must take some 'deciding', so to
speak -- if it is non-trivial. We must have a deciding machine. In our
example, the deciding machine is the original machine with a slight
modification.

ol...@pobox.com

unread,
May 9, 2003, 2:35:24 PM5/9/03
to pe...@cse.unsw.edu.au, haskel...@haskell.org

I'd like to clarify the termination decision procedure. I believe it
can take the body of a function in our language and tell if the
function terminates for all inputs. This implies that we can decide on
termination without evaluating the function on all inputs (whose set
is countably infinite).

A small clarification: the 'branch-on-zero' statement should have the
form "if-nonnegative exp then exp1 else exp2".

Because the domain includes 'undefined' (aka NaN), the only functions
that terminate for all inputs are those that leave their arguments
alone and either propagate them or return constants. For example, the
following functions terminate on all inputs
f1(x) = x
f2(x,y) = y
f3(x) = 0
f4(x) = if-nonnegative power(5,125) then x else NaN
The following functions will fail to terminate on at least one input:
g1(x) = x + x
g2(x) = if-non-negative x then x else NaN
g3(x) = if-non-negative x*x then 0 else 1

Although it seems that g3 is equivalent to f3, that is not true:
g3(NaN) diverges whereas f3(NaN) returns 0.

These examples clarify a decision procedure, which can be stated as
follows: if a partial evaluation of f(x...z) -- that is, unfolding plus
constant propagation -- reduces f() to f1, f2, or f3 types, the
function f() terminates on all inputs. Otherwise, there is one value
(most likely NaN), that, when passed to f(), will cause it to diverge.

Our partial evaluation procedure first unfolds all function
calls. That is possible because the call graph does not have direct
cycles (NPFIX must be treated as a special node in the call
graph). Any operation (multiplication, addition, comparison, NPFIX) on
a dynamic value can lead to a non-termination (if that value is
NaN). Thus the only operations that can still guarantee termination
are "if exp1 then exp2 else exp3" and "NPFIX exp1 exp2 exp3" where
exp1 is a constant expression. We can evaluate it. Because it contains
only primitive recursive functions, we provably can do that in some
finite time. Therefore, we can decide which branch to take and
continue to analyze exp2 or exp3. It seems the decision procedure is
total and correct.

Eray Ozkural

unread,
May 12, 2003, 2:55:25 PM5/12/03
to ol...@pobox.com, pe...@cse.unsw.edu.au, haskel...@haskell.org
On Friday 09 May 2003 21:33, ol...@pobox.com wrote:
> I'd like to clarify the termination decision procedure. I believe it
> can take the body of a function in our language and tell if the
> function terminates for all inputs. This implies that we can decide on
> termination without evaluating the function on all inputs (whose set
> is countably infinite).

I've seen many constructions on primitive recursive functions but what I don't
understand, not having the required expertise on recursive function theory,
is whether the set of primitive recursive functions correspond to recursive
sets in theory of computation.

I got confused when I read that Ackermann's function was a recursive function
that was not primitive. Could you please explain this to me?

Excuse me if I'm being ignorant about this subject.

Regards,

--
Eray Ozkural (exa) <er...@cs.bilkent.edu.tr>
Comp. Sci. Dept., Bilkent University, Ankara KDE Project: http://www.kde.org
www: http://www.cs.bilkent.edu.tr/~erayo Malfunction: http://mp3.com/ariza
GPG public key fingerprint: 360C 852F 88B0 A745 F31B EA0F 7C07 AE16 874D 539C

_______________________________________________

Jon Fairbairn

unread,
May 12, 2003, 6:18:19 PM5/12/03
to er...@cs.bilkent.edu.tr, haskel...@haskell.org
On 2003-05-12 at 21:53+0300 Eray Ozkural wrote:

> I've seen many constructions on primitive recursive
> functions but what I don' t understand, not having the
> required expertise on recursive function theory, is
> whether the set of primitive recursive functions
> correspond to recursive sets in theory of computation.

They don't, because

> [...] Ackermann's function was a recursive function that
> was not primitive.

If I remember correctly, that's the chief reason Ackermann
came up with the function. Have a look at <URL:
http://mathworld.wolfram.com/AckermannFunction.html > and
the links on that page for computable and primitive
recursive, and see if that helps. The site also has a
definition of recursive.


Jón

--
Jón Fairbairn Jon.Fa...@cl.cam.ac.uk
31 Chalmers Road j...@cl.cam.ac.uk
Cambridge CB1 3SZ +44 1223 570179 (after 14:00 only, please!)

Eray Ozkural

unread,
May 13, 2003, 5:24:24 AM5/13/03
to Jon Fairbairn, haskel...@haskell.org
On Tuesday 13 May 2003 01:17, Jon Fairbairn wrote:
> On 2003-05-12 at 21:53+0300 Eray Ozkural wrote:
> > I've seen many constructions on primitive recursive
> > functions but what I don' t understand, not having the
> > required expertise on recursive function theory, is
> > whether the set of primitive recursive functions
> > correspond to recursive sets in theory of computation.
>
> They don't, because
>
> > [...] Ackermann's function was a recursive function that
> > was not primitive.
>
> If I remember correctly, that's the chief reason Ackermann
> came up with the function. Have a look at <URL:
> http://mathworld.wolfram.com/AckermannFunction.html > and
> the links on that page for computable and primitive
> recursive, and see if that helps. The site also has a
> definition of recursive.

OK. Then isn't there an answer to the original question? I couldn't find a
machine model that satisfies Cagdas's operational requirements. Any thoughts?
Maybe it's a very easy answer but I can't see it, and I can't say I know the
proof of every theorem in Cindrella book.

Cheers,

--
Eray Ozkural (exa) <er...@cs.bilkent.edu.tr>
Comp. Sci. Dept., Bilkent University, Ankara KDE Project: http://www.kde.org
www: http://www.cs.bilkent.edu.tr/~erayo Malfunction: http://mp3.com/ariza
GPG public key fingerprint: 360C 852F 88B0 A745 F31B EA0F 7C07 AE16 874D 539C

_______________________________________________

Cagdas Ozgenc

unread,
May 13, 2003, 9:09:29 AM5/13/03
to haskel...@haskell.org

> >
> > If I remember correctly, that's the chief reason Ackermann
> > came up with the function. Have a look at <URL:
> > http://mathworld.wolfram.com/AckermannFunction.html > and
> > the links on that page for computable and primitive
> > recursive, and see if that helps. The site also has a
> > definition of recursive.
>
> OK. Then isn't there an answer to the original question? I couldn't find a
> machine model that satisfies Cagdas's operational requirements. Any
thoughts?
> Maybe it's a very easy answer but I can't see it, and I can't say I know
the
> proof of every theorem in Cindrella book.
>
> Cheers,


Indeed, I am still looking for a theorem of some sort that either equates
stongly normalizing systems to primitive recursive functions (if this is the
case), or a theorem that demonstrates some sort of limitation to strongly
normalizing systems when compared to a turing machine, or a system that can
decide recursive class but unable to recognize recursively enumerable class.

Eray Ozkural

unread,
May 13, 2003, 3:41:23 PM5/13/03
to Cagdas Ozgenc, haskel...@haskell.org
On Tuesday 13 May 2003 16:08, Cagdas Ozgenc wrote:
> Indeed, I am still looking for a theorem of some sort that either equates
> stongly normalizing systems to primitive recursive functions (if this is
> the case), or a theorem that demonstrates some sort of limitation to
> strongly normalizing systems when compared to a turing machine, or a system
> that can decide recursive class but unable to recognize recursively
> enumerable class.

Hmm, I think this depends on what a strongly normalizing system is :) Slightly
going out of my sphere of knowledge (^_^)

Cheers,

--
Eray Ozkural (exa) <er...@cs.bilkent.edu.tr>
Comp. Sci. Dept., Bilkent University, Ankara KDE Project: http://www.kde.org
www: http://www.cs.bilkent.edu.tr/~erayo Malfunction: http://mp3.com/ariza
GPG public key fingerprint: 360C 852F 88B0 A745 F31B EA0F 7C07 AE16 874D 539C

_______________________________________________

C T McBride

unread,
May 14, 2003, 5:26:31 AM5/14/03
to er...@cs.bilkent.edu.tr, Cagdas Ozgenc, haskel...@haskell.org
Hi

> On Tuesday 13 May 2003 16:08, Cagdas Ozgenc wrote:
> > Indeed, I am still looking for a theorem of some sort that either equates
> > stongly normalizing systems to primitive recursive functions (if this is
> > the case), or a theorem that demonstrates some sort of limitation to
> > strongly normalizing systems when compared to a turing machine, or a system
> > that can decide recursive class but unable to recognize recursively
> > enumerable class.

There ain't no such thing. Recursiveness is undecidable. More concretely,
a strongly normalizing system captures a class of terminating functions
which is necessarily incomplete: a simple diagonalization argument shows
that the system's own normalization function (terminating, by definition)
cannot be coded within the system itself.

> Hmm, I think this depends on what a strongly normalizing system is :)
> Slightly going out of my sphere of knowledge (^_^)

A *strongly* normalizing system is one where *all* reduction strategies
yield a normal form. Type theories are usually designed to be strongly
normalizing, hence they are Turing incomplete; they do contain all
programs which are *provably* terminating in the particular logic to which
they correspond, but that logic, being consistent, is necessarily also
incomplete.

(Incidentally, Cayenne's type theory is the exception rather than the
rule: it's much-criticized undecidable typechecking comes down to the
availability of non-terminating programs at the type level. ghc with
`undecidable instances' allows you to write non-terminating Prolog
programs at the type level, thus breaking for exactly the same reason.
What exactly is Haskell's type level programming language, anyway?)

Of course, restricting to an incomplete fragment does not necessarily
mean `primitive recursion' in the narrow sense which excludes Ackermann's
function, viz

data Nat = O | S Nat

primrec :: Nat -> (Nat -> Nat -> Nat) -> Nat -> Nat
primrec base step O = base
primrec base step (S n) = step n (primrec base step n)

Just a bit of polymorphism is enough to overcome that problem:

polyprimrec :: t -> (Nat -> t -> t) -> Nat -> t
polyprimrec base step O = base
polyprimrec base step (S n) = step n (polyprimrec base step n)

Old fashioned dependent type theories present computation over inductive
datatypes by equipping their structural induction principles with a
computational behaviour---an inductive proof of all n : Nat . P n, when
applied to 3, reduces to step 2 (step 1 (step 0 base)), just like
polyprimrec, but with

base :: P 0,
and step :: all n : Nat. P n -> P (S n).

Suitably equipped with `pattern matching' sugar, these induction
principles provide quite a rich language of terminating functions,
necessarily incomplete, but including such notoriously troublesome
customers as first-order unification.

Moreover, a structural induction principle is just the recursion operator
which comes `free of charge' with an inductive datatype: many other total
recursive idioms can be proven admissible once (by a process which
resembles coding up a memoization scheme), then re-used freely in
programs.

So there's no magic complete answer to guaranteed termination, but it is,
I claim, useful to work within an incomplete but terminating language
if it enables you te express the structural reasons why your program
works, not just what it should do next.

Hope this helps

Conor

Cagdas Ozgenc

unread,
May 14, 2003, 7:54:26 AM5/14/03
to haskel...@haskell.org

> > On Tuesday 13 May 2003 16:08, Cagdas Ozgenc wrote:
> > > Indeed, I am still looking for a theorem of some sort that either
equates
> > > stongly normalizing systems to primitive recursive functions (if this
is
> > > the case), or a theorem that demonstrates some sort of limitation to
> > > strongly normalizing systems when compared to a turing machine, or a
system
> > > that can decide recursive class but unable to recognize recursively
> > > enumerable class.
>
> There ain't no such thing. Recursiveness is undecidable. More concretely,
> a strongly normalizing system captures a class of terminating functions
> which is necessarily incomplete: a simple diagonalization argument shows
> that the system's own normalization function (terminating, by definition)
> cannot be coded within the system itself.

I think that is not correct. Diagonalization cannot be pursued on every
situation, because it has some prerequisites (for example the system should
be capable of using its programs as subprograms, or ability to invert the
outcome of a program). If the system captures only terminating functions,
then the termination can be simply calculated like the following:

willTerminate:: (a->b) -> Bool
willTerminate = true

As you can see I decided the termination for all functions. Maybe you mean
something else. I don't quite know what "normalization function" is. Another
counter example is a Deterministic Finite Automata. It will terminate on all
finite inputs, and it can encode its own termination function (again similar
to the above trivial function).

> > Hmm, I think this depends on what a strongly normalizing system is :)
> > Slightly going out of my sphere of knowledge (^_^)
>
> A *strongly* normalizing system is one where *all* reduction strategies
> yield a normal form. Type theories are usually designed to be strongly
> normalizing, hence they are Turing incomplete; they do contain all
> programs which are *provably* terminating in the particular logic to which
> they correspond, but that logic, being consistent, is necessarily also
> incomplete.
>

> Of course, restricting to an incomplete fragment does not necessarily
> mean `primitive recursion' in the narrow sense which excludes Ackermann's
> function, viz

That's not the point. It does exclude Ackermann because it will fail to
compile if the compiler is unable to detect the termination of Ackermann's
function. I don't know much about this (it is indeed what I was trying to
learn by starting this discussion), but it may be factual that a general
termination test can only be written for primitive recursive function class
(it is irrelevant that one can prove termination for some non primitive
recursive functions, the question is "is there a general algorithm for a
wider class?"). If this is the case then too bad for us. My question is as
follows: "What is the largest class that we can find a termination
procedure?".

> So there's no magic complete answer to guaranteed termination, but it is,
> I claim, useful to work within an incomplete but terminating language
> if it enables you te express the structural reasons why your program
> works, not just what it should do next.

It will be definetely useful, and it may not necessarily be incomplete. If I
remember correctly monoid(N,+) : monoid defined over naturals with addition
operator is sound and complete. Of course systems where one can write
homological statements will be incomplete. It may be the case that a useful
strongly normalizing system may turn out to be complete. But I don't care
about completeness. Getting back to the core discussion, I really would like
to know the limitations of terminating systems.

Cagdas Ozgenc

unread,
May 14, 2003, 8:01:24 AM5/14/03
to haskel...@haskell.org
My question is as
> follows: "What is the largest class that we can find a termination
> procedure?".

Perhaps that's a little misleading, but I don't know how to phrase it
properly. Basically what is the largest class of languages that a
terminating system can decide?

Alastair Reid

unread,
May 14, 2003, 8:32:24 AM5/14/03
to Cagdas Ozgenc, haskel...@haskell.org
Can this topic be taken elsewhere please?

The discussion never had much to do with Haskell and the relevance seems to
have been falling steadily.

--
Alastair Reid

Eray Ozkural

unread,
May 14, 2003, 9:08:49 AM5/14/03
to C T McBride, Cagdas Ozgenc, haskel...@haskell.org
Hello,

On Wednesday 14 May 2003 12:25, C T McBride wrote:
> A *strongly* normalizing system is one where *all* reduction strategies
> yield a normal form. Type theories are usually designed to be strongly
> normalizing, hence they are Turing incomplete; they do contain all
> programs which are *provably* terminating in the particular logic to which
> they correspond, but that logic, being consistent, is necessarily also
> incomplete.

I guess if Godel were here he could tell us that any consistent formal system
powerful enough to express number theory is necessarily incomplete. So maybe
I was asking the contrapositive, so the answer is already known? That is, if
a system is complete, it cannot express number theory. This follows from
incompleteness. But I'm not sure if that is what I was asking. It seems to be
different: is there a language to denote any complete system? That's the
question, and L_d or L_u doesn't seem to be the answer to that (on their own)

Is there a known proof that one needs at least a TM to recognize all decidable
languages? Ouch, I must fix my head and I'll get back to this :)

If you guys think haskell-cafe is improper for this conversation we can
continue on theory-edge on yahoo groups. But I don't think it's improper,
after all there is all kind of theoretical weirdness talked of in the main
haskell discussion list. Why should this be any less relevant???

We were just having a similar conversation about CSLs and recursive sets on
theory-edge so you might want to check it out while it's hot.

Regards,

--
Eray Ozkural (exa) <er...@cs.bilkent.edu.tr>
Comp. Sci. Dept., Bilkent University, Ankara KDE Project: http://www.kde.org
www: http://www.cs.bilkent.edu.tr/~erayo Malfunction: http://mp3.com/ariza
GPG public key fingerprint: 360C 852F 88B0 A745 F31B EA0F 7C07 AE16 874D 539C

_______________________________________________

Simon Peyton-Jones

unread,
May 14, 2003, 9:34:28 AM5/14/03
to er...@cs.bilkent.edu.tr, C T McBride, Cagdas Ozgenc, haskel...@haskell.org

| If you guys think haskell-cafe is improper for this conversation we =
can
| continue on theory-edge on yahoo groups. But I don't think it's =
improper,
| after all there is all kind of theoretical weirdness talked of in the =

main
| haskell discussion list. Why should this be any less relevant???

Anyway this is Haskell Café, where the rules are pretty loose! (If it =
were on the main Haskell list I'd certainly suggest moving the thread to =
Haskell-café, but it seem ok there, to me.)

S

Cagdas Ozgenc

unread,
May 14, 2003, 10:30:27 AM5/14/03
to haskel...@haskell.org
I agree. It is a Café after all, even though coffee is not served to clients
:) We should be permitted to socialize and discuss casually.
Plus, it is a related subject.

----- Original Message -----
From: "Simon Peyton-Jones" <sim...@microsoft.com>
To: <er...@cs.bilkent.edu.tr>; "C T McBride" <c.t.m...@durham.ac.uk>
Cc: "Cagdas Ozgenc" <co...@cornell.edu>; <haskel...@haskell.org>
Sent: Wednesday, May 14, 2003 4:33 PM
Subject: RE: on termination

| If you guys think haskell-cafe is improper for this conversation we can
| continue on theory-edge on yahoo groups. But I don't think it's improper,
| after all there is all kind of theoretical weirdness talked of in the main


| haskell discussion list. Why should this be any less relevant???

Anyway this is Haskell Café, where the rules are pretty loose! (If it were


on the main Haskell list I'd certainly suggest moving the thread to

Markus....@infineon.com

unread,
May 14, 2003, 10:45:22 AM5/14/03
to haskel...@haskell.org
Somebody asked for coffee?

/ / /
\ \ \
/ / /
+++++++++++
+ +--\
+ +___/
\+++++/
=============
=========

--
Markus Schnell
Infineon Technologies AG, CPR ET
Tel +49 (89) 234-20875

Sam Moelius

unread,
May 14, 2003, 11:11:27 AM5/14/03
to c.t.m...@durham.ac.uk, haskel...@haskell.org
C T McBride wrote:
> a simple diagonalization argument shows
> that the system's own normalization function (terminating, by definition)
> cannot be coded within the system itself.

I would be interested in seeing this. Could you elaborate, or point us to a
link where this is spelled out?

Sam Moelius

Eray Ozkural

unread,
May 14, 2003, 2:55:25 PM5/14/03
to Sam Moelius, c.t.m...@durham.ac.uk, haskel...@haskell.org
On Wednesday 14 May 2003 18:10, Sam Moelius wrote:
> I would be interested in seeing this. Could you elaborate, or point us to
> a link where this is spelled out?

I can't see an immediate diagonalization proof either.


--
Eray Ozkural (exa) <er...@cs.bilkent.edu.tr>
Comp. Sci. Dept., Bilkent University, Ankara KDE Project: http://www.kde.org
www: http://www.cs.bilkent.edu.tr/~erayo Malfunction: http://mp3.com/ariza
GPG public key fingerprint: 360C 852F 88B0 A745 F31B EA0F 7C07 AE16 874D 539C

_______________________________________________

Andrew J Bromage

unread,
May 14, 2003, 11:58:22 PM5/14/03
to Cagdas Ozgenc, haskel...@haskell.org
G'day all.

On Wed, May 14, 2003 at 05:27:19PM +0300, Cagdas Ozgenc wrote:

> I agree. It is a Café after all, even though coffee is not served to clients
> :) We should be permitted to socialize and discuss casually.

(Obscure joke alert.)

Eray probably only drinks tea.

Cheers,
Andrew Bromage

Andrew J Bromage

unread,
May 15, 2003, 12:17:22 AM5/15/03
to haskel...@haskell.org
G'day.

On Wed, May 14, 2003 at 04:05:54PM +0300, Eray Ozkural wrote:

> It seems to be
> different: is there a language to denote any complete system?

Of course there is. A language is just a subset of the power set of
some symbol alphabet. So, for example, the set of all halting TMs
(encoded appropriately) forms a language.

> Is there a known proof that one needs at least a TM to recognize all
> decidable languages?

Here's my working definition of "decidable language":

A language L is decidable for some class of automata C if
there is an automaton in C which recognises L and halts
for all inputs.

That is, my working definition of "decidable language" is dependent
on the class of automata in which you're trying to implement
decidability.

If your class of automata is DFAs, for example, all languages are
decidable, so you don't even need a TM for that. If your class of
automata is TMs, not even a TM will help you.

Cheers,
Andrew Bromage

Andrew J Bromage

unread,
May 15, 2003, 12:23:21 AM5/15/03
to haskel...@haskell.org
G'day.

On Wed, May 14, 2003 at 02:59:50PM +0300, Cagdas Ozgenc wrote:

> Perhaps that's a little misleading, but I don't know how to phrase it
> properly. Basically what is the largest class of languages that a
> terminating system can decide?

Assuming for the moment that your "terminating system" is a TM...

I believe that if you were to produce such a class of languages, I can
produce another recursively enumerable language not in your class by
some kind of diagonalisation procedure. I can then create a
terminating recogniser which accepts your class, plus the new language
as a special case.

Cheers,
Andrew Bromage

Cagdas Ozgenc

unread,
May 15, 2003, 3:25:28 AM5/15/03
to haskel...@haskell.org

>
> Of course there is. A language is just a subset of the power set of
> some symbol alphabet. So, for example, the set of all halting TMs
> (encoded appropriately) forms a language.

It is not a power set. A language is a subset of the word monoid generated
by the alphabet by applying reccurent production of the alphabet (the star
operation).

> > Is there a known proof that one needs at least a TM to recognize all
> > decidable languages?
>
> Here's my working definition of "decidable language":
>
> A language L is decidable for some class of automata C if
> there is an automaton in C which recognises L and halts
> for all inputs.

I always thought in a similar fashion. But literature insists that the
decidability is always measured with respect to a Turing Machine. Thus, I
was unable to communicate to many other people on the usenet.

Andrew J Bromage

unread,
May 15, 2003, 3:46:36 AM5/15/03
to Cagdas Ozgenc, haskel...@haskell.org
G'day.

On Thu, May 15, 2003 at 10:23:21AM +0300, Cagdas Ozgenc wrote:

> It is not a power set. A language is a subset of the word monoid generated
> by the alphabet by applying reccurent production of the alphabet (the star
> operation).

You're right, sorry.

> I always thought in a similar fashion. But literature insists that the
> decidability is always measured with respect to a Turing Machine.

That's probably because of the Church-Turing thesis (i.e. computation
equals Turing Machine). However, there are smaller and larger
definitions of "computation" than what can be accomplished on a TM.

Cheers,
Andrew Bromage

Eray Ozkural

unread,
May 15, 2003, 7:29:33 AM5/15/03
to Cagdas Ozgenc, haskel...@haskell.org
On Thursday 15 May 2003 10:23, Cagdas Ozgenc wrote:
> I always thought in a similar fashion. But literature insists that the
> decidability is always measured with respect to a Turing Machine. Thus, I
> was unable to communicate to many other people on the usenet.

Hmm.

But, the real question you are asking doesn't seem to be quite trivial Cagdas.

Cheers,

--
Eray Ozkural (exa) <er...@cs.bilkent.edu.tr>
Comp. Sci. Dept., Bilkent University, Ankara KDE Project: http://www.kde.org
www: http://www.cs.bilkent.edu.tr/~erayo Malfunction: http://mp3.com/ariza
GPG public key fingerprint: 360C 852F 88B0 A745 F31B EA0F 7C07 AE16 874D 539C

_______________________________________________

Eray Ozkural

unread,
May 15, 2003, 7:44:58 AM5/15/03
to Andrew J Bromage, haskel...@haskell.org
On Thursday 15 May 2003 07:16, Andrew J Bromage wrote:
> G'day.
>
> On Wed, May 14, 2003 at 04:05:54PM +0300, Eray Ozkural wrote:
> > It seems to be
> > different: is there a language to denote any complete system?
>
> Of course there is. A language is just a subset of the power set of
> some symbol alphabet. So, for example, the set of all halting TMs
> (encoded appropriately) forms a language.
>

Well... A language L \subset of \Sigma^* as Cagdas said.

Anyway, by language I meant something else. Is "Formal System" better?

Let's see:
Is there a formal system to denote all complete systems and nothing else?

Let's try it in automata jargon:

We know that one needs a machine more powerful than an LBA to recognize all
recursive languages. However, even an LBA, by definition is a TM and it can
loop over two symbols forever. That is not all LBAs are guaranteed to halt.

Can there be an alternative machine formulation that only recognizes recursive
sets and nothing else? That is it should be stronger than an LBA, yet less
powerful than a TM because it excludes R.E - recursive. So, we are looking
for something that doesn't have a corresponding machine. It's possible that
it does not exist. But the proof could be interesting for us.


> > Is there a known proof that one needs at least a TM to recognize all
> > decidable languages?

[snip]


>
> If your class of automata is DFAs, for example, all languages are
> decidable, so you don't even need a TM for that. If your class of
> automata is TMs, not even a TM will help you.

This is not a proof I hope :P

Cheers,

--
Eray Ozkural (exa) <er...@cs.bilkent.edu.tr>
Comp. Sci. Dept., Bilkent University, Ankara KDE Project: http://www.kde.org
www: http://www.cs.bilkent.edu.tr/~erayo Malfunction: http://mp3.com/ariza
GPG public key fingerprint: 360C 852F 88B0 A745 F31B EA0F 7C07 AE16 874D 539C

_______________________________________________

Cagdas Ozgenc

unread,
May 15, 2003, 8:51:43 AM5/15/03
to haskel...@haskell.org
> Let's see:
> Is there a formal system to denote all complete systems and nothing
else?

Completeness is not equal to deciding all recursive languages IMO. The
bottom explanation of yours is not the same as the above question. Systems
with sufficient power are incomplete. The system I am looking for doesn't
have to decide its own termination, but its termination should be decideable
by using an auxillary TM.
Be careful with the jargon. Literature insists that "undecidable" is equal
to "cannot be decided by a TM". Although an automaton may not decide its own
halting , it may be decided by a TM, hence will be called decideable.

> Let's try it in automata jargon:
>
> We know that one needs a machine more powerful than an LBA to recognize
all
> recursive languages. However, even an LBA, by definition is a TM and it
can
> loop over two symbols forever. That is not all LBAs are guaranteed to
halt.
>
> Can there be an alternative machine formulation that only recognizes
recursive
> sets and nothing else?

You mean "decide" not "recognize", right?

> That is it should be stronger than an LBA, yet less
> powerful than a TM because it excludes R.E - recursive. So, we are
looking
> for something that doesn't have a corresponding machine. It's possible
that
> it does not exist. But the proof could be interesting for us.

The fact that there may be looping LBAs is irrelevant because we can discard
those, since the halting is decidable(again note the terminology, can be
decided by a TM) for LBA. Indeed the system has to be powerful than an LBA
but we still should be able to write a TM that is capabale of discarding the
ones that go into infinite loop. I don't know whether it is correct to say
that it should be more powerful than a LBA, because it won't have the power
to loop :).

C T McBride

unread,
May 15, 2003, 10:07:30 AM5/15/03
to Cagdas Ozgenc, haskel...@haskell.org
Hi

I'm sorry about the level of consternation this discussion seems to be
generating, so let me attempt to clarify my previous remarks.

The diagonalization argument which shows that any total language
misses some total programs is the usual one: Godel-code everything in
sight, then make the alleged universal program eat a twisted copy of
itself. It's the Epimenides/Cantor/Russell/Quine/Godel/Turing
argument. And it goes like this...

Suppose we have a programming language in which all expressions
compute to a value excluding bottom. For sake of argument, let's
code expressions and values as natural numbers (an ascii source file
is just a big number; so is a finite output). In particular, every
function f from Nat to Nat which lives in the language is quoted by a
code (quote f) :: Nat, and we know a total function which unquotes,
executing a coded f at a given argument

eval :: Nat -> (Nat -> Nat)

with spec

eval (quote f) x = f x
eval _ _ = 0

Given such a function, I can summon up its evil cousin, with spec:

evil :: Nat -> Nat

evil code = 1 + (eval code code)

Now, if eval is total, so is evil. But if evil lies within our language,
it will have a number. Without loss of generality, quote evil is a human
number and that number is 666. So, we get

evil 666
= 1 + (eval 666 666)
= 1 + evil 666

which is plainly untrue.

Hence evil is a total function which is not expressible in the language
(so eval better not be expressible either).

Of course, for any language of total functions, its Halting Problem is
trivial, but that's beside the point. There is no largest class of
recognizably terminating programs, because no such class can include
its own *evaluation* function, which is by definition terminating.
Given a total language L, we can always construct a strictly larger
language L', also recognizable, which also includes the eval function
for L.

Meanwhile, back in the cafe, why should Haskellers give a monkeys? Two
reasons: one pertinent now, one potential.

Firstly, when we make (or Haskell derives) recursive instance
declarations, we might like to know that

(1) the compiler will not go into a spin when attempting to compute the
object code which generates the dictionary for a given instance
(2) the code so generated will not loop at run-time

You might argue that (1) is not so important, because you can always
ctrl-C, but (2) is more serious, because if it fails, you get the
situation where the compiler approves your program, then breaks it
by inserting bogus code, promising to deliver an instance which does
not actually exist.

To guarantee these properties, we essentially need to ensure that the
instance declaration language is a terminating fragment of Prolog. The
various flags available now are either way too cautious or way too
liberal: what's a suitable middle way? There is no most general choice.

Secondly, might it be desirable to isolate a recognizable sublanguage of
Haskell which contains only total programs? Pedagogically, Turner argues
that it's useful to have a `safe' language in which to learn.
Rhetorically, making bottom a value is just sophistry to hide the fact
that looping and match failure are pretty bad side-effects available
within an allegedly pure language---preferable to core-dumps or wiping
your hard drive, but still bad. Logically, if you want to show a program
is correct, it helps if you can get its totality for free. Pragmatically,
there are fewer caveats to optimizing bottomless programs.

As we've seen, such a sublanguage (perhaps called `Ask', a part of Haskell
which definitely excludes Hell) cannot contain all the angels, but it
certainly admits plenty of useful ones who can always answer mundane
things you might Ask. It's ironic, but not disastrous that lucifer, the
evaluation function by which Ask's angels bring their light, is himself an
angel, but one who must be cast into Hell.

Yours religiously

Conor

Eray Ozkural

unread,
May 15, 2003, 1:23:21 PM5/15/03
to Cagdas Ozgenc, haskel...@haskell.org
On Thursday 15 May 2003 15:49, Cagdas Ozgenc wrote:
> Completeness is not equal to deciding all recursive languages IMO. The
> bottom explanation of yours is not the same as the above question. Systems
> with sufficient power are incomplete. The system I am looking for doesn't
> have to decide its own termination, but its termination should be
> decideable by using an auxillary TM.
> Be careful with the jargon. Literature insists that "undecidable" is equal
> to "cannot be decided by a TM". Although an automaton may not decide its
> own halting , it may be decided by a TM, hence will be called decideable.
>

Decidable means that accept or reject states are guaranteed to halt. That is
as you said the defining property of recursive sets. The complement of a
recursive set is recursive....
I didn't say otherwise (that it should have to decide a "halting problem" for
itself). Let's rephrase. If a language is recursively enumerable but not
recursive it's not decidable. You would like to exclude all such languages
from your automata and would like to recognize (accept or reject) all
recursive languages. Right?

> The fact that there may be looping LBAs is irrelevant because we can
> discard those, since the halting is decidable(again note the terminology,
> can be decided by a TM) for LBA. Indeed the system has to be powerful than
> an LBA but we still should be able to write a TM that is capabale of
> discarding the ones that go into infinite loop. I don't know whether it is
> correct to say that it should be more powerful than a LBA, because it won't
> have the power to loop :).

You mean the following:
I can write a programming language for CSL recognizers that can, at compile
time, give an error message such as:
** Undecidable program!!! Check your logic!

Do you mean this? And how do you, for instance generalize this to polynomial
bounded automata or higher orders?

Sincerely,

--
Eray Ozkural (exa) <er...@cs.bilkent.edu.tr>
Comp. Sci. Dept., Bilkent University, Ankara KDE Project: http://www.kde.org
www: http://www.cs.bilkent.edu.tr/~erayo Malfunction: http://mp3.com/ariza
GPG public key fingerprint: 360C 852F 88B0 A745 F31B EA0F 7C07 AE16 874D 539C

Carl R. Witty

unread,
Jun 9, 2003, 7:50:21 PM6/9/03
to Cagdas Ozgenc, Haskell Cafe List
"Cagdas Ozgenc" <co...@cornell.edu> writes:

> This may be a little off topic, but I could not get much response from =
> comp.theory, so here it goes:
>
> Is it possible to have a programming language that can be used to =
> produce only the programs that terminate, but at the same time decide =
> all recursive languages? Or does such limitation automatically reduce =
> the class of languages that such a programming language decide to =
> primitive-recursive?

If you have any programming language (say Haskell), and if you have
some formal system which is capable of proving termination properties
of programs in your programming language (and in which proofs are
machine-checkable), then you can create a new language "Terminating
Haskell" simply by pairing each program with a proof of termination.

Of course, if you start with a Turing-complete language, then your
formal system is necessarily incomplete; this means there will be
programs that do terminate but that you cannot prove terminate. So
your programming language will include programs that decide all
languages that you can prove recursive (in your formal system), but
not all recursive languages. However, if your formal system is
strong enough, it may be possible to prove termination of all the
programs you really care about.

Some theorem-proving systems (including ACL2 and PVS) are like this --
within the logic, you can write programs in a Turing-complete
language, as long as you can prove termination. (More precisely, the
language would be Turing-complete were it not for the termination
requirement. In both cases, the "program" portion is fairly distinct
from the "proof of termination" portion, so that it does make sense to
talk about what the language would be like without the termination
requirement.)

It has long been a goal of mine to create a Haskell-like programming
language where you could mark portions as being guaranteed to
terminate. The compiler would prove termination whenever it could,
but in cases where the termination proof was too complicated for
automatic proofs, the programmer would be required to add an explicit
proof of termination.

Carl Witty

Reply all
Reply to author
Forward
0 new messages