Motivated by the recent interest in models of guarded (co-)recursion, we study their equational properties. We formulate axioms for guarded fixpoint operators generalizing the axioms of iteration theories of Bloom and Ésik. Models of these axioms include both standard (e.g., cpo-based) models of iteration theories and models of guarded recursion such as complete metric spaces or the topos of trees studied by Birkedal et al. We show that the standard result on the satisfaction of all Conway axioms by a unique dagger operation generalizes to the guarded setting. We also introduce the notion of guarded trace operator on a category, and we prove that guarded trace and guarded fixpoint operators are in one-to-one correspondence. Our results are intended as first steps leading, hopefully, towards future description of classifying theories for guarded recursion.
2
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
Although in 1977 V.B. Shehtman constructed the first Kripke incomplete intermediate logic, no-one in the known literature has completed his work by constructing a continuum of such logics. After a substantial reminder on how an incomplete logic can be obtained, I will construct a sequence of frames similar to those used by Jankov and Fine. None of these frames can be reduced by a p-morphism to another; at the same time, there are no p-morphisms from generated subframes of the Fine frame onto any frame from the considered sequence. All of the frames satisfy all of Shehtman's axioms. Therefore, by using the characteristic formulas of the frames from the sequence it is possible to obtain the desired conclusion.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.