3 ms·

> The asymptote cannot reach 100% of program behavior in any finitary way. That would solve the halting problem. There are languages that enforce termination.

> The asymptote cannot reach 100% of program behavior in any finitary way. That would solve the halting problem. There are languages that enforce termination. They only accept programs that can be shown to terminate through syntactic reasoning (e.g., when processing lists, you only recurse on the tail), or where you can prove termination by other means. Coq is like this, as is Isabelle, as is F* , as are others. They also provide different kinds of escape hatches if you really want non-terminating things, like processing infinite streams. This "we can never be sure of anything, because the halting problem" meme is getting boring. Yes, you cannot write the Collatz function in Coq. No, that is not a limitation in the real world.

hwayne 9y ago
> This "we can never be sure of anything, because the halting problem" meme is getting boring. Yes, you cannot write the Collatz function in Coq. No, that is not a limitation in the real world. How about, say, a video game? That's something where we reasonably _want_ it to not terminate, because we're primarily interested in its side effects.
- tom_mellior 9y ago
  That's what the escape hatches are for. In Coq, for instance, you can also write functions processing infinite streams, provided that they also produce something regularly. For example, in a game, you could write a function from an infinite stream of inputs to an infinite stream of frame updates. You can not write functions that would not terminate while computing the updates for some given frame. Alternatively, you just write a function to iterate your game world update N times, where you choose N large enough to ensure that your game can run until the heat death of the universe. That's not a nonterminating function, but it's long-running enough for all practical purposes.
danharaj 9y ago
I'm aware of strongly normalizing systems and the escape hatch of coinductive programming. But when we're talking about the space of all programs, the fundamental limit of incompleteness is important. How else do we judge the merit of a type system except by seeing how it fits into the overall space of computable processes? There are two ways to see type systems. In the first way you construct terms along with their types, this is called Church style. In the second way, the terms exist before their types and you use types to describe their behavior, this is called Curry style. In particular take System F. In Church style the terms of System F come with their types. In Curry style we see System F types as a way to describe the behavior of untyped lambda terms. I used to think Church style was more important but lately I've been more partial to Curry style. Programs exist before you type them, type systems tell you how they behave. They also tell you how to construct programs but this is subordinate to the more fundamental descriptive capacity.
- tom_mellior 9y ago
  > But when we're talking about the space of all programs, the fundamental limit of incompleteness is important. I agree with this. But I think that usually we are not really talking about all programs. We are talking about useful programs, and those are usually terminating. In theory, not always, see first-order theorem provers; but in practice, we always call a prover with a time limit because nontermination isn't useful. > Programs exist before you type them, type systems tell you how they behave. They also tell you how to construct programs but this is subordinate to the more fundamental descriptive capacity. That's an interesting point, and I agree in many respects. I think when programming in a dynamically typed language, I approach things in one style, and in statically typed languages in another style. But specifically for termination, I don't think so. I never want to write a nonterminating program; the termination property for my programs exists (as a requirement) before the program does.

hwayne 9y ago

> This "we can never be sure of anything, because the halting problem" meme is getting boring. Yes, you cannot write the Collatz function in Coq. No, that is not a limitation in the real world. How about, say, a video game? That's something where we reasonably _want_ it to not terminate, because we're primarily interested in its side effects.

tom_mellior 9y ago
That's what the escape hatches are for. In Coq, for instance, you can also write functions processing infinite streams, provided that they also produce something regularly. For example, in a game, you could write a function from an infinite stream of inputs to an infinite stream of frame updates. You can not write functions that would not terminate while computing the updates for some given frame. Alternatively, you just write a function to iterate your game world update N times, where you choose N large enough to ensure that your game can run until the heat death of the universe. That's not a nonterminating function, but it's long-running enough for all practical purposes.

danharaj 9y ago

I'm aware of strongly normalizing systems and the escape hatch of coinductive programming. But when we're talking about the space of all programs, the fundamental limit of incompleteness is important. How else do we judge the merit of a type system except by seeing how it fits into the overall space of computable processes? There are two ways to see type systems. In the first way you construct terms along with their types, this is called Church style. In the second way, the terms exist before their types and you use types to describe their behavior, this is called Curry style. In particular take System F. In Church style the terms of System F come with their types. In Curry style we see System F types as a way to describe the behavior of untyped lambda terms. I used to think Church style was more important but lately I've been more partial to Curry style. Programs exist before you type them, type systems tell you how they behave. They also tell you how to construct programs but this is subordinate to the more fundamental descriptive capacity.

tom_mellior 9y ago
> But when we're talking about the space of all programs, the fundamental limit of incompleteness is important. I agree with this. But I think that usually we are not really talking about all programs. We are talking about useful programs, and those are usually terminating. In theory, not always, see first-order theorem provers; but in practice, we always call a prover with a time limit because nontermination isn't useful. > Programs exist before you type them, type systems tell you how they behave. They also tell you how to construct programs but this is subordinate to the more fundamental descriptive capacity. That's an interesting point, and I agree in many respects. I think when programming in a dynamically typed language, I approach things in one style, and in statically typed languages in another style. But specifically for termination, I don't think so. I never want to write a nonterminating program; the termination property for my programs exists (as a requirement) before the program does.