Email Gateway (Aug 22 2022 at 13:17): Email Gateway (Aug 22 2022 at 13:17):From: Gergely Buday <gbuday@karolyrobert.hu>
Hi,
this is not an Isabelle per se question, but as there are people here versed in programming language theory, and this I think relates to the function package of Isabelle, I feel this adequate here.
http://cs.stackexchange.com/questions/58076/axiomatisation-in-the-presence-of-recursion
--
He develops the Fork calculus for reasoning about concurrent functional programs, the motivation being Concurrent ML.
In chapter 5, he writes:
First, we add a recursion operator, allowing us to define processes
with infinite behaviour. Recursion is not difficult to deal with
(thanks to the use of operational semantics), except that the
axiomatisation cannot be shown complete in presence of recursion.
There is no literature reference here, so I ask you: where can I read about why recursion makes a programming language's axiomatisation cannot be proved complete, and in precisely what meaning?
--
Can you clarify what you mean by the axiomatization of a programming language? I'm assuming it's because, once there is recursion, there are programs which halt for which there exist no proofs that they halt, but I can't be sure not knowing what exactly the completeness is talking about here. - jmite
--
Do I understand correctly that the above remark about adding recursion to a language makes any axiomatisation incomplete is true
for the same reason that makes it impossible to create a general function definition in a higher order logic of total functions, without the need to supply a termination proof in general?
Email Gateway (Aug 22 2022 at 13:17):From: David Cock <david.cock@inf.ethz.ch>
The question is a little loose with terminology. I would guess that
he's referring to the "Axiomatisation of Strong Equivalence" introduced
on P51 i.e. the axiomatisation of the process equivalence relation. And
if (presumably) a terminating process isn't equivalent to a
nonterminating process in his relation, then it really should be
incomplete/undecidable. Seems that it's defined in terms of syntactic
equivalence on normal forms, which would presumably give a decision
procedure for termination, if it were complete.
David
Email Gateway (Aug 22 2022 at 13:33):From: Lawrence Paulson <lp15@cam.ac.uk>
They may simply be referring to the fact that in most cases, once you have recursion, you can define enough number theory for Gödel’s theorem to apply. The need for termination proofs is quite another matter: accepting a function definition such as f(n) = Suc(f(Suc n)) can easily lead to inconsistency.
Larry
Last updated: May 06 2024 at 16:21 UTC