Email Gateway (Aug 18 2022 at 12:31): Email Gateway (Aug 18 2022 at 12:31):From: Jens Doll <jd@cococo.de>
Hello,
my project Columbo is slowly making progress. I currently wonder about
decidability of the halting problem for simple while programs, resp.
Rice's theorem. The following while program does clearly halt for all
integer values in i,s,ug,og and it's function can be expressed by a
denotation:
http://cococo.de/products/windows/Columbo/sample1.html
What would Isabelle deduct from the code or it's denotation?
Greetings,
Jens
Email Gateway (Aug 18 2022 at 12:47):From: Jens Doll <jd@cococo.de>
I also have a gift: the two sample pages
http://cococo.de/products/windows/Columbo/sample1.html
http://cococo.de/products/windows/Columbo/sample2.html
have been updated for better readability.
Greetings,
Jens
Last updated: May 03 2024 at 04:19 UTC