Mr Flibble <flibble@reddwarf.jmc> writes:
Recursive definitions are fine, infinitely recursive definitions (such
as The Halting Problem) are INVALID.
(1) The halting problem is not an infinitely recursive definition.
(2) Infinitely recursive definitions are often fine. For example, the
list of Fibonacci numbers:
fibs = 1 : 1 : zipWith (+) fibs (tail fibs)
or the list of factorials:
facts = prod 1 1 where prod p n = p : prod (p*n) (n+1)
On 5/1/2022 9:39 AM, Ben wrote:
Mr Flibble <flibble@reddwarf.jmc> writes:
Recursive definitions are fine, infinitely recursive definitions (such
as The Halting Problem) are INVALID.
(1) The halting problem is not an infinitely recursive definition.
(2) Infinitely recursive definitions are often fine. For example, the
list of Fibonacci numbers:
This type is never fine: // Adapted from Clocksin & Mellish foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...))))))))))))
Because Gödel says
14 Every epistemological antinomy can likewise be used for a similar undecidability proof
G ↔ ¬Provable(F, G) is an epistemological antinomy therefore it is necessarily sufficiently equivalent to his G.
Likewise with this one: LP ↔ ¬True(LP)
It can be evaluated as semantically incorrect without the need to define True(). No matter how True() is defined LP ↔ ¬True(LP) is semantically incorrect because it specifies this:
LP ↔ ¬True(¬True(¬True(¬True(¬True(¬True(¬True(¬True(LP))))))))
and Prolog can detect and reject this with unify_with_occurs_check.
fibs = 1 : 1 : zipWith (+) fibs (tail fibs)
or the list of factorials:
facts = prod 1 1 where prod p n = p : prod (p*n) (n+1)
Sysop: | Keyop |
---|---|
Location: | Huddersfield, West Yorkshire, UK |
Users: | 366 |
Nodes: | 16 (2 / 14) |
Uptime: | 16:54:02 |
Calls: | 7,831 |
Files: | 12,930 |
Messages: | 5,770,234 |