Lambda the Ultimate

I'm not sure I buy your phrasing - how do I describe non-termination using a logic? It seems to me that what's interesting is what we include.

how do I describe non-termination using a logic? It seems to me that what's interesting is what we include.

I see that you don't accept the law of the excluded middle: an excellent demonstration of intuistionistic logic. ;-)

If you prefer, you could conceive of it the other way around: I want to select the class of only and all the normalizing terms in untyped LC, observe that those are equivalent to those that can be proven in intuisitionistic logic, and use that.

I just think this requires a bigger leap of discovery than the other way around in this instance.

Put differently, how do you define the universe of possibilties of what you might include a priori? Isn't it easier to start from something too much and whittle it down to just right?

It depends on the things you're looking to exclude. We already know from conventional logic that if we wish to exclude non-termination we're going to have to throw away some terminating terms as well. I don't know if that's been shown to apply to the functions described as well as the terms (though I suspect so), I should go poke around the big pile of CS theory results again.

Now there's a thought: is there an intuitionistic proof that the halting problem's only semi-decidable (I'll settle for proving it's not decidable)?

Certainly ideas like the lambda cube and extending typing to subtyping seem to me to show a progression of things we can include - as do advances like qualified types.

Edited to add: Of course, substructural types would be an option in the other direction, and qualified types are only an improvement if you're not willing to let your polymorphism be unsound!

Sheesh, it's hard to answer a simple question with a simple answer around here. ;-)

Li's original question probably doesn't involve non-termination; it just so happens that part of the interesting correspondence in CH involves strong normalization.

If you want to generalize the notion of types as logical constraints on the well-formedness of programs (which seems to be Li's intent), I'm suggesting using this "what do you want to filter out" approach as a way of thinking about it.

Obviously, there is lots more to say about CH, types and programming, intuitionistic logic, etc. I'm just trying to spread it out over a longer period by addressing one problem at a time. ;-)

The point is to localize errors. To make exact descriptions of the domain of functions so that as many logical errors as possible also are type errors. And to make sure that they are detected as soon as possible.

I am not focusing on type inference or actually eliminating any specific class of programs. Just to make sure that if the program breaks its specification, its reported as soon as possible.

In which case you're left looking at rendering the specification as a type - which in many ways throws you right in the deep end because you need a decently powerful logic.

Yes I have that, the thing Im worried about is that the logic is to powerful.

If you are wobbly on all the gory details about the power and limitations of type systems and logical systems, maybe the thing to do is look at specific examples that have already been developed by others to deal with such problems.

The example you originally gave about delimited ranges has been looked at by the dependent-typing folks (the much-discussed-here Epigram, for example.) What the trade-offs, limitations and problems of such regimes are already much thought about and described.

If someone had already developed the perfect type system that had all the right power and none of the short-comings. type theory would no longer hold much interest. Given that it is still a hard problem, standing on the shoulders of giants rather than trying to do your own from scratch is probably the way to go.