Re: if-then without -else?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

Re: if-then without -else?

Rodrigo Stevaux
which cannot be prohibited statically
if we want both the language to be Turing complete,
and type inference to be decidable.

Could you be so kind as to give a hint on literature that could help me understand this statement?

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: if-then without -else?

Alexis King
Detecting termination of an arbitrary program written in a
Turing-complete language is (about as literally as can be) the halting
problem:

    https://en.wikipedia.org/wiki/Halting_problem

This problem has been known to be unsolvable in general (assuming we
don’t discover some form of computation more powerful than a Turing
machine; that is, the Church-Turing thesis holds) since 1936, and is one
of the most fundamental results in computer science.

It’s possible to determine if programs halt if you restrict the language
sufficiently, but then it won’t be Turing-complete. However, this does
not make totality checking completely fruitless, as it turns out you can
do a great deal of useful things even in a language that is not
Turing-complete (which I find is often surprising to people).

Alexis

> On Aug 31, 2018, at 15:02, Rodrigo Stevaux <[hidden email]> wrote:
>
> which cannot be prohibited statically if we want both the language to
> be Turing complete, and type inference to be decidable.
>
>
> Could you be so kind as to give a hint on literature that could help
> me understand this statement?
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: if-then without -else?

Rodrigo Stevaux
Oh I see. Type checking a possibly infinite computation might itself take possibly infinite steps?

Em sex, 31 de ago de 2018 às 17:13, Alexis King <[hidden email]> escreveu:
Detecting termination of an arbitrary program written in a
Turing-complete language is (about as literally as can be) the halting
problem:

    https://en.wikipedia.org/wiki/Halting_problem

This problem has been known to be unsolvable in general (assuming we
don’t discover some form of computation more powerful than a Turing
machine; that is, the Church-Turing thesis holds) since 1936, and is one
of the most fundamental results in computer science.

It’s possible to determine if programs halt if you restrict the language
sufficiently, but then it won’t be Turing-complete. However, this does
not make totality checking completely fruitless, as it turns out you can
do a great deal of useful things even in a language that is not
Turing-complete (which I find is often surprising to people).

Alexis

> On Aug 31, 2018, at 15:02, Rodrigo Stevaux <[hidden email]> wrote:
>
> which cannot be prohibited statically if we want both the language to
> be Turing complete, and type inference to be decidable.
>
>
> Could you be so kind as to give a hint on literature that could help
> me understand this statement?

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.