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

[Pascal Costanza]

Patricia Shanahan wrote:
> 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.

Sorry, obviously I was far from being clear. ACL2 is not 
Turing-complete. All iterations must be expressed in terms of 
well-founded recursion.


Pascal

-- 
3rd European Lisp Workshop
July 3 - Nantes, France - co-located with ECOOP 2006
http://lisp-ecoop06.bknr.net/