/HaltingProblem

The proof of undecidability of halting problem, using the model -- WHILE language.

Primary LanguageAgda

HaltingProblem

Focus on the proof of undecidability of halting problem. Using the computation model - WHILE language.

Folder While/* contains the definition, syntax and semantic of the WHILE language. Folder Universal/* contains the method to code and decode the program in WHILE language, and the proof of the correctness of the universal WHILE program. Folder HaltingProblem/* contains the proof of the undecidability of halting problem by contradiction. which is, assume there exists some machine that could decide the halting problem, then, proof the contradictory.