Email Gateway (Aug 18 2022 at 12:08): Email Gateway (Aug 18 2022 at 12:08):From: li yongjian <lyj238@gmail.com>
hi:
I may ask a stupid question, here I want to know the meanings of the
saying " Coinduction and induction are a parir of duals". Does this
means that if we define
a set S inductively, then we can define (-S) coinductively?
For example, in the Auth lib, we define
the function parts inductively as follows:
consts parts :: "msg set => msg set"
inductive "parts H"
intros
Inj [intro]: "X \<in> H ==> X \<in> parts H"
Fst: "{|X,Y|} \<in> parts H ==> X \<in> parts H"
Snd: "{|X,Y|} \<in> parts H ==> Y \<in> parts H"
Body: "Crypt K X \<in> parts H ==> X \<in> parts H"
So there should be a coinductive defintion for a function
not_parts such that not_parts H= - (parts H)?
But I have not find how to give a coinductive definition for
not_parts ?
Who can give such a defintion of not_parts ?
or I have sth wrong with the meaning of the dualilty between induction
and coinduction.
regards!
Email Gateway (Aug 18 2022 at 12:31):From: Tjark Weber <webertj@in.tum.de>
Li,
if f is a monotone function (on a Boolean algebra, say), then
-(lfp f) = gfp g,
where g(x) := -f(-x).
Best,
Tjark
Last updated: Nov 21 2024 at 12:39 UTC