# Axiomatisation in the presence of recursion

I read Klaus Havelund's thesis on the Fork Calculus:

http://havelund.com/Publications/thesis.ps

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?

## migrated from cstheory.stackexchange.comMay 31 '16 at 3:05

This question came from our site for theoretical computer scientists and researchers in related fields.

• 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 May 31 '16 at 3:10
• that is exactly my question, I do not know what did the author mean here – Gergely May 31 '16 at 9:24