1. Forum
  2. Usenet
  3. COMP.THEORY

  • Proof of Halting Problem Decidability in Typed Hypercomputational Progr

    From Mr Flibble@21:1/5 to All on Fri Apr 25 19:01:56 2025
    ### Introduction
    This document proves that the halting problem is decidable in a
    computational framework called Typed Hypercomputational Programs (THP).
    The THP model allows both halting and non-halting programs, uses a type
    system to prevent self-referential paradoxes, and assumes infinite computational resources (infinite time and memory) for simulating program execution. The proof addresses the assumption that self-referential
    conflation of a decider and its input constitutes a category (type) error, which the type system eliminates to ensure decidability.

    ---

    ### Step 1: Define the THP Framework
    THP is a typed functional programming model that permits partial programs, restricts self-reference, and leverages infinite resources to analyze
    program behavior.

    #### Syntax and Types
    - **Types**:
    - Basic: Int, Bool, String.
    - Function types: σ → τ.
    - No recursive types.
    - **Programs**: Terms M : σ. Descriptions ⟨M⟩ : String.
    - **Program Behavior**:
    - Total: Halts on all inputs.
    - Partial: May halt or loop indefinitely.
    - **Typing Rules**:
    - Simply typed lambda calculus rules.
    - General recursion allows non-halting programs.
    - **Non-Self-Referential Constraint**: Prevents M : σ → τ from
    simulating itself on ⟨M⟩ : String in a paradoxical way.
    - **Semantics**:
    - Call-by-value evaluation.
    - M(x) may halt (return τ) or loop.
    - **Infinite Resources**:
    - Hypercomputational model with infinite time/memory.
    - Termination oracle T : String × σ → Bool simulates M(x) indefinitely.
    - **Universal Evaluator*
  • From Mikko@21:1/5 to Mr Flibble on Sat Apr 26 11:03:06 2025
    On 2025-04-25 19:01:56 +0000, Mr Flibble said:

    ### Introduction
    This document proves that the halting problem is decidable in a
    computational framework called Typed Hypercomputational Programs (THP).
    The THP model allows both halting and non-halting programs, uses a type system to prevent self-referential paradoxes, and assumes infinite computational resources (infinite time and memory) for simulating program execution. The proof addresses the assumption that self-referential conflation of a decider and its input constitutes a category (type) error, which the type system eliminates to ensure decidability.

    ---

    ### Step 1: Define the THP Framework

    Before the step 1 you should specify what it means to halt when infinitely
    many elemntary actions are executed.

    --
    Mikko

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Richard Heathfield@21:1/5 to Mr Flibble on Fri May 2 06:15:40 2025
    On 25/04/2025 20:01, Mr Flibble wrote:
    The proof addresses the assumption that self-referential
    conflation of a decider and its input constitutes a category (type) error, which the type system eliminates to ensure decidability.

    So you've designed a system in which you guarantee decidability.
    Great! Let's see the code for your decider.

    --
    Richard Heathfield
    Email: rjh at cpax dot org dot uk
    "Usenet is a strange place" - dmr 29 July 1999
    Sig line 4 vacant - apply within

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mr Flibble@21:1/5 to Richard Heathfield on Fri May 2 15:09:28 2025
    On Fri, 02 May 2025 06:15:40 +0100, Richard Heathfield wrote:

    On 25/04/2025 20:01, Mr Flibble wrote:
    The proof addresses the assumption that self-referential conflation of
    a decider and its input constitutes a category (type) error,
    which the type system eliminates to ensure decidability.

    So you've designed a system in which you guarantee decidability.
    Great! Let's see the code for your decider.

    The code for a decider would be trivial: it merely needs to be of the simulating type, possibly stack machine based; such a machine is already a solved problem: the only question is the magnitude of the resources that
    can be allocated to it (infinite in this case).

    /Flibble

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mr Flibble@21:1/5 to Richard Heathfield on Fri May 2 16:42:28 2025
    On Fri, 02 May 2025 17:31:30 +0100, Richard Heathfield wrote:

    On 02/05/2025 16:09, Mr Flibble wrote:
    On Fri, 02 May 2025 06:15:40 +0100, Richard Heathfield wrote:

    On 25/04/2025 20:01, Mr Flibble wrote:
    The proof addresses the assumption that self-referential conflation
    of a decider and its input constitutes a category (type) error,
    which the type system eliminates to ensure decidability.

    So you've designed a system in which you guarantee decidability.
    Great! Let's see the code for your decider.

    The code for a decider would be trivial:

    And yet it remains conspicuous by its absence.

    it merely needs to be of the
    simulating type, possibly stack machine based; such a machine is
    already a solved problem: the only question is the magnitude of the
    resources that can be allocated to it (infinite in this case).

    Great! No problem there, then. Off you go...

    No problem at all.

    /Flibble

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Richard Heathfield@21:1/5 to Mr Flibble on Fri May 2 17:31:30 2025
    On 02/05/2025 16:09, Mr Flibble wrote:
    On Fri, 02 May 2025 06:15:40 +0100, Richard Heathfield wrote:

    On 25/04/2025 20:01, Mr Flibble wrote:
    The proof addresses the assumption that self-referential conflation of
    a decider and its input constitutes a category (type) error,
    which the type system eliminates to ensure decidability.

    So you've designed a system in which you guarantee decidability.
    Great! Let's see the code for your decider.

    The code for a decider would be trivial:

    And yet it remains conspicuous by its absence.

    it merely needs to be of the
    simulating type, possibly stack machine based; such a machine is already a solved problem: the only question is the magnitude of the resources that
    can be allocated to it (infinite in this case).

    Great! No problem there, then. Off you go...

    --
    Richard Heathfield
    Email: rjh at cpax dot org dot uk
    "Usenet is a strange place" - dmr 29 July 1999
    Sig line 4 vacant - apply within

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)