Saying "latently-typed language" is making a category mistake

[Patricia Shanahan]

Pascal Costanza wrote:
> Matthias Blume wrote:
>> Pascal Costanza <pc at p-cos.net> writes:
>>
>>> Patricia Shanahan wrote:
>>>> Vesa Karvonen wrote:
>>>> ...
>>>>> An example of a form of informal reasoning that (practically) every
>>>>> programmer does daily is termination analysis.  There are type systems
>>>>> that guarantee termination, but I think that is fair to say that it
>>>>> is not
>>>>> yet understood how to make a practical general purpose language, whose
>>>>> type system would guarantee termination (or at least I'm not aware
>>>>> of such
>>>>> a language).  It should also be clear that termination analysis 
>>>>> need not
>>>>> be done informally.  Given a program, it may be possible to
>>>>> formally prove
>>>>> that it terminates.
>>>> To make the halting problem decidable one would have to do one of
>>>> two
>>>> things: Depend on memory size limits, or have a language that really is
>>>> less expressive, at a very deep level, than any of the languages
>>>> mentioned in the newsgroups header for this message.
>>> Not quite. See http://en.wikipedia.org/wiki/ACL2
>>
>> What do you mean "not quite"?  Of course, Patricia is absolutely
>> right.  Termination-guaranteeing languages are fundamentally less
>> expressive than Turing-complete languages.  ACL2 was not mentioned in
>> the newsgroup header.
> 
> ACL2 is a subset of Common Lisp, and programs written in ACL2 are 
> executable in Common Lisp. comp.lang.lisp is not only about Common Lisp, 
> but even if it were, ACL2 would fit.

To prove Turing-completeness of ACL2 from Turing-completeness of Common
Lisp you would need to run the reduction the other way round, showing
that any Common Lisp program can be converted to, or emulated by, an
ACL2 program.

Patricia