Cyc­lic Proofs in Brief

Cyc­lic proofs are an al­tern­at­ive to tra­di­tional proof trees where, in­stead, the graph of proof nodes may con­tain cycles. Re­cently, many cyc­lic proof sys­tems have been de­velopped for lo­gics with some no­tion of a fixed-­point such as those with in­duct­ive defined pre­dic­ates or do­mains, in­clud­ing my CycleQ sys­tem de­signed for cyc­lic equa­tional reas­on­ing over func­tional pro­grams.

Of course, not all such proof graphs will cor­res­pond to valid ar­gu­ments as a node may be trivial jus­ti­fied by it­self. Thus cyc­lic proof the­ory dis­tin­guishes between pre-­proofs that are loc­ally well-­formed but have no other re­quire­ments and proper proofs that have an ad­di­tional global cor­rect­ness prop­erty. The well-­formed­ness of a pre-­proof means that the premises of a given node jus­tify its con­clu­sion. If we could per­form well-­foun­ded in­duc­tion of the proof tree, this prop­erty would be suf­fi­cient as an in­valid con­clu­sion re­quires an in­valid premise and so on un­til we reach a leaf and thus have a con­tra­dic­tion. For cyc­lic proofs, however, we per­form well-­foun­ded in­duc­tion not over the proof tree it­self but over the in­stances re­quired of proof nodes. The global cor­rect­ness prop­erty en­sure that the re­quired in­stances are well-­foun­ded so that we can ap­peal to a sim­ilar ar­gu­ment and jus­tify the valid­ity of each proof node by des­cent in­finie. In­tu­it­ively, for any given in­stance of a proof node in a proper cyc­lic proof, we can ex­tract a cor­res­pond­ing fi­nite proof tree.

Curry­-Howard Cor­res­pond­ence

This may seem like a rather ob­scure area of proof the­ory but ac­tu­ally has a very close cor­res­pond­ence to every­day com­pon­ents of func­tion pro­grams. To un­der­stand this con­nec­tion we must first rev­ist the curry­-howard cor­res­pond­ence which in­ter­prets pro­pos­i­tions as types and their proofs as pro­grams of that type. For ex­ample, to prove \(p \wedge q\) it is ne­ces­sary to provide a proof of both p and q hence the tuple con­structor cap­tures con­junc­tion:

and :: p -> q -> (p, q)
and p q = (p, q)

Sim­il­arly, the im­pli­ci­ation is in­ter­preted as the func­tion ar­row (i.e. if you give me a proof of the hy­po­thes­is, I will give you a proof of the con­clu­sion), dis­junc­tion as the cop­roduct type, uni­ver­sal quan­ti­fic­a­tion as poly­morph­ism or de­pend­ent types, and so on…

Where this gets in­ter­est­ing, however, is in the in­ter­pret­a­tion of proof-by-in­duc­tion. The in­duc­tion prin­ciple for nat­ural num­bers is cap­tured the fol­low­ing im­plic­a­tion:

\[ (P(0) \wedge \forall k.\, P(k) \Rightarrow P(k+1)) \Rightarrow \forall n.\, P(n) \]

Trans­lat­ing this for­mula across the Curry­-Howard cor­res­pond­ence, gives us the type (n :: Nat) -> p 0 -> (for­all k. p k -> p (k + 1)) -> p n where p :: Nat -> Type is the pre­dic­ate in ques­tion. Clearly, there is only one nat­ural defin­i­tion for a func­tion of this type that makes the un­der­ly­ing idea of proof-by-in­duc­tion ex­pli­cit:

in­duct :: (n :: Nat) -> p 0 -> (for­all k. p k -> p (k + 1)) -> p n
in­duct 0 base hyp = base
in­duct (n + 1) base hyp =
  let pn :: pn
      pn = in­duct n base hyp 
   in hyp pn

To get an in­tu­ition for the be­ha­viour of this func­tion by drop­ping the de­pend­ent types and sup­pose p is simply a pro­pos­i­tion, we get the fol­low­ing func­tion:

foldN :: Nat -> p -> (p -> p) -> p
foldN 0 base hyp = base
foldN (n + 1) base hyp =
  let pn :: p
      pn = foldN n base hyp
   in hyp pn

i.e. the elim­in­ator for nat­ural num­bers. The same cor­res­pond­ence ap­plied to other in­duct­ive data­type. For ex­ample, struc­tural in­duc­tion over lists is in­ter­preted com­pu­ta­tion­ally as the stand­ard foldr func­tion.

Stand­ard proof sys­tems with in­duc­tion rules (or ax­ioms) posit the ex­ist­ence of such elim­in­at­ors that can be used in other code. Their sound­ness is de­rived from the fact that the proof can­not be re­curs­ive and can only use these pre-­de­termined re­cur­sion com­bin­at­ors. Cyc­lic pre-­proofs, on the other hand, are func­tional pro­grams with gen­eral re­cur­sion. The global cor­rect­ness cri­ter­ia, as­sert­ing the re­quired in­stances of proof nodes forms well-­foun­ded se­quences, cor­res­ponds to the fact that the pro­gram is ter­min­at­ing.

Im­plic­a­tions for Global Cor­rect­ness Check­ing

The ori­ginal mech­an­ism for de­term­in­ing the sound­ness of a cyc­lic pre-­proof was to use Bü­chi auto­mata to cap­ture the pos­sible paths throught the proof (i.e. runs of the pro­gram) and show that each of these have an in­fin­tely de­creas­ing value. This pro­cess is costly as it re­quires con­struct­ing the com­ple­ment of a Bü­chi auto­mata, which is doubly ex­po­nen­tial in the size of the proof.

Us­ing the cor­res­pond­ence with ter­min­a­tion of func­tion pro­grams, however, opens up the pos­sib­il­ity of us­ing ef­fi­cient ter­min­a­tion tools to jus­tify cyc­lic proofs such as size-change based ter­min­a­tion. This is the ap­proach we em­ploy in the CycleQ the­orem prover.