On the action of the implicative closure operator on the set of partial functions of the multivalued logic

2021 ◽  
Vol 31 (3) ◽  
pp. 155-164
Author(s):  
Sergey S. Marchenkov

Abstract On the set P k ∗ $\begin{array}{} \displaystyle P_k^* \end{array}$ of partial functions of the k-valued logic, we consider the implicative closure operator, which is the extension of the parametric closure operator via the logical implication. It is proved that, for any k ⩾ 2, the number of implicative closed classes in P k ∗ $\begin{array}{} \displaystyle P_k^* \end{array}$ is finite. For any k ⩾ 2, in P k ∗ $\begin{array}{} \displaystyle P_k^* \end{array}$ two series of implicative closed classes are defined. We show that these two series exhaust all implicative precomplete classes. We also identify all 8 atoms of the lattice of implicative closed classes in P 3 ∗ $\begin{array}{} \displaystyle P_3^* \end{array}$ .

2002 ◽  
Vol 41 (01) ◽  
pp. 3-13 ◽  
Author(s):  
M. Schäfers

SummaryNuclear cardiological procedures have paved the way for non-invasive diagnostics of various partial functions of the heart. Many of these functions cannot be visualised for diagnosis by any other method (e. g. innervation). These techniques supplement morphological diagnosis with regard to treatment planning and monitoring. Furthermore, they possess considerable prognostic relevance, an increasingly important issue in clinical medicine today, not least in view of the cost-benefit ratio.Our current understanding shows that effective, targeted nuclear cardiology diagnosis – in particular for high-risk patients – can contribute toward cost savings while improving the quality of diagnostic and therapeutic measures.In the future, nuclear cardiology will have to withstand mounting competition from other imaging techniques (magnetic resonance imaging, electron beam tomography, multislice computed tomography). The continuing development of these methods increasingly enables measurement of functional aspects of the heart. Nuclear radiology methods will probably develop in the direction of molecular imaging.


1986 ◽  
Vol 21 (6) ◽  
pp. 61-62
Author(s):  
T Vasak

2021 ◽  
Vol 8 (8) ◽  
pp. 2004216
Author(s):  
Sae Byeok Jo ◽  
Joohoon Kang ◽  
Jeong Ho Cho

2021 ◽  
Vol 179 (1) ◽  
pp. 59-74
Author(s):  
Josef Šlapal

In this paper, we propose new definitions of digital Jordan curves and digital Jordan surfaces. We start with introducing and studying closure operators on a given set that are associated with n-ary relations (n > 1 an integer) on this set. Discussed are in particular the closure operators associated with certain n-ary relations on the digital line ℤ. Of these relations, we focus on a ternary one equipping the digital plane ℤ2 and the digital space ℤ3 with the closure operator associated with the direct product of two and three, respectively, copies of this ternary relation. The connectedness provided by the closure operator is shown to be suitable for defining digital curves satisfying a digital Jordan curve theorem and digital surfaces satisfying a digital Jordan surface theorem.


2017 ◽  
Vol 29 (1) ◽  
pp. 67-92 ◽  
Author(s):  
JAMES CHAPMAN ◽  
TARMO UUSTALU ◽  
NICCOLÒ VELTRI

The delay datatype was introduced by Capretta (Logical Methods in Computer Science, 1(2), article 1, 2005) as a means to deal with partial functions (as in computability theory) in Martin-Löf type theory. The delay datatype is a monad. It is often desirable to consider two delayed computations equal, if they terminate with equal values, whenever one of them terminates. The equivalence relation underlying this identification is called weak bisimilarity. In type theory, one commonly replaces quotients with setoids. In this approach, the delay datatype quotiented by weak bisimilarity is still a monad–a constructive alternative to the maybe monad. In this paper, we consider the alternative approach of Hofmann (Extensional Constructs in Intensional Type Theory, Springer, London, 1997) of extending type theory with inductive-like quotient types. In this setting, it is difficult to define the intended monad multiplication for the quotiented datatype. We give a solution where we postulate some principles, crucially proposition extensionality and the (semi-classical) axiom of countable choice. With the aid of these principles, we also prove that the quotiented delay datatype delivers free ω-complete pointed partial orders (ωcppos).Altenkirch et al. (Lecture Notes in Computer Science, vol. 10203, Springer, Heidelberg, 534–549, 2017) demonstrated that, in homotopy type theory, a certain higher inductive–inductive type is the free ωcppo on a type X essentially by definition; this allowed them to obtain a monad of free ωcppos without recourse to a choice principle. We notice that, by a similar construction, a simpler ordinary higher inductive type gives the free countably complete join semilattice on the unit type 1. This type suffices for constructing a monad, which is isomorphic to the one of Altenkirch et al. We have fully formalized our results in the Agda dependently typed programming language.


Sign in / Sign up

Export Citation Format

Share Document