Endotypes of partial equivalence relations

2021 ◽  
Author(s):  
Yurii Zhuchok ◽  
Olena Toichkina
Keyword(s):  
Equivalence Relations ◽  
Partial Equivalence Relations

Least fixpoints of endofunctors of cartesian closed categories

1993 ◽  
Vol 3 (2) ◽  
pp. 229-257 ◽  
Author(s):  
J. Lambek
Keyword(s):  
Propositional Calculus ◽  
Second Order ◽  
Equivalence Relations ◽  
Cartesian Closed Category ◽  
Closed Category ◽  
Congruence Relations ◽  
Partial Recursive Functions ◽  
Cartesian Closed Categories ◽  
Partial Equivalence Relations ◽  
Cartesian Closed

Least fixpoints are constructed for finite coproducts of definable endofunctors of Cartesian closed categories that have weak polynomial products and joint equalizers of arbitrary families of pairs of parallel arrows. Both conditions hold in PER, the category whose objects are partial equivalence relations on N, and whose arrows are partial recursive functions. Weak polynomial products exist in any cartesian closed category with a finite number of objects as well as in any model of second order polymorphic lambda calculus: that is, in the proof theory of any second order positive intuitionistic propositional calculus, but such a category need not have equalizers. However, any finite coproduct of definable endofunctors of a cartesian closed category with weak polynomial products will have a least fixpoint in a larger category with equalizers whose objects are right ideals (or sieves) of modulo certain congruence relations, and whose arrows are induced from .

Building domains from graph models

1992 ◽  
Vol 2 (3) ◽  
pp. 277-299 ◽  
Author(s):  
Wesley Phoa
Keyword(s):  
Internal Structure ◽  
Set Theory ◽  
Category Theory ◽  
Domain Theory ◽  
Equivalence Relations ◽  
Graph Models ◽  
Constructive Set Theory ◽  
Partial Equivalence Relations

In this paper we study partial equivalence relations (PERs) over graph models of the λcalculus. We define categories of PERs that behave like predomains, and like domains. These categories are small and complete; so we can solve domain equations and construct polymorphic types inside them. Upper, lower and convex powerdomain constructions are also available, as well as interpretations of subtyping and bounded quantification. Rather than performing explicit calculations with PERs, we work inside the appropriate realizability topos: this is a model of constructive set theory in which PERs, can be regarded simply as special kinds of sets. In this framework, most of the definitions and proofs become quite smple and attractives. They illustrative some general technicques in ‘synthetic domain theory’ that rely heavily on category theory; using these methods, we can obtain quite powerful results about classes of PERs, even when we know very little about their internal structure.

Higher-order intersection types and multiple inheritance

1996 ◽  
Vol 6 (5) ◽  
pp. 469-501 ◽  
Author(s):  
Adriana B. Compagnoni ◽  
Benjamin C. Pierce
Keyword(s):  
Structural Properties ◽  
Object Oriented ◽  
Natural Generalization ◽  
Higher Order ◽  
Object Oriented Programming ◽  
Equivalence Relations ◽  
Semantic Model ◽  
Multiple Inheritance ◽  
Intersection Types ◽  
Partial Equivalence Relations

We study a natural generalization of SystemFωwith intersection types, establishing basic structural properties and constructing a semantic model based on partial equivalence relations to prove the soundness of typing. As an application of this calculus, we define a simple typed model of object-oriented programming with multiple inheritance.

scholarly journals Layered Predicates

1992 ◽  
Vol 21 (423) ◽  
Author(s):  
Flemming Nielson ◽  
Hanne Riis Nielson
Keyword(s):  
Equivalence Relations ◽  
Substitution Property ◽  
Structural Induction ◽  
Major Application ◽  
Partial Equivalence Relations ◽  
Definition Of

We review the concept of logical relations and how they interact with structural induction, furthermore we give examples of their use, and of particular interest is the combination with the PER-idea (partial equivalence relations). This is then generalized to Kripke logical relations; the major application is to show that in combination with the PER-idea this solves the problem of establishing a substitution property in a manner oonducive to structural induction. Finally we introduce the concept of Kripke-layered predicates; this allows a modular definition of predicates and supports a methodology of ''proofs in stages'' where each stage forcuses on only one aspect and thus is more manageable. All of these techniques have been tested and refined in ''realistic applications'' that have been documented elsewhere.

scholarly journals The Meaning of Types From Intrinsic to Extrinsic Semantics

2000 ◽  
Vol 7 (32) ◽  
Author(s):  
John C. Reynolds
Keyword(s):  
Lambda Calculus ◽  
Denotational Semantics ◽  
Equivalence Relations ◽  
Typed Lambda Calculus ◽  
Partial Equivalence Relations ◽  
Definition Of

A definition of a typed language is said to be "intrinsic" if it assigns<br />meanings to typings rather than arbitrary phrases, so that ill-typed<br />phrases are meaningless. In contrast, a definition is said to be "extrinsic"<br />if all phrases have meanings that are independent of their typings,<br />while typings represent properties of these meanings.<br />For a simply typed lambda calculus, extended with recursion, subtypes,<br />and named products, we give an intrinsic denotational semantics<br />and a denotational semantics of the underlying untyped language. We<br />then establish a logical relations theorem between these two semantics,<br />and show that the logical relations can be "bracketed" by retractions<br />between the domains of the two semantics. From these results, we<br />derive an extrinsic semantics that uses partial equivalence relations.

Weakly precomplete equivalence relations in the Ershov hierarchy

2019 ◽  
Vol 58 (3) ◽  
pp. 297-319
Author(s):  
N. A. Bazhenov ◽  
B. S. Kalmurzaev
Keyword(s):  
Equivalence Relations ◽  
Ershov Hierarchy
Sign in / Sign up

Export Citation Format

Share Document