A construction of non-well-founded sets within Martin-Löf's type theory

1989 ◽  
Vol 54 (1) ◽  
pp. 57-64 ◽  
Author(s):  
Ingrid Lindström
Keyword(s):  
Equivalence Relation ◽  
Type Theory ◽  
Additional Condition ◽  
Complete System ◽  
Definition Of ◽  
Induction Scheme

AbstractIn this paper, we show that non-well-founded sets can be defined constructively by formalizing Hallnäs' limit definition of these within Martin-Löfs theory of types. A system is a type W together with an assignment of and to each ∝ ∈ W. We show that for any system W we can define an equivalence relation =w such that ∝ =w ß ∈ U and =w is the maximal bisimulation. Aczel's proof that CZF can be interpreted in the type V of iterative sets shows that if the system W satisfies an additional condition (*), then we can interpret CZF minus the set induction scheme in W. W is then extended to a complete system W* by taking limits of approximation chains. We show that in W* the antifoundation axiom AFA holds as well as the axioms of CFZ−.

Fundamental relations and identities of fuzzy hyperalgebras

2021 ◽  
pp. 1-10
Author(s):  
Narjes Firouzkouhi ◽  
Abbas Amini ◽  
Chun Cheng ◽  
Mehdi Soleymani ◽  
Bijan Davvaz
Keyword(s):  
Universal Algebra ◽  
Equivalence Relation ◽  
Polynomial Function ◽  
Equivalence Relations ◽  
Fundamental Relation ◽  
Term Function ◽  
Biological Phenomena ◽  
Definition Of

Inspired by fuzzy hyperalgebras and fuzzy polynomial function (term function), some homomorphism properties of fundamental relation on fuzzy hyperalgebras are conveyed. The obtained relations of fuzzy hyperalgebra are utilized for certain applications, i.e., biological phenomena and genetics along with some elucidatory examples presenting various aspects of fuzzy hyperalgebras. Then, by considering the definition of identities (weak and strong) as a class of fuzzy polynomial function, the smallest equivalence relation (fundamental relation) is obtained which is an important tool for fuzzy hyperalgebraic systems. Through the characterization of these equivalence relations of a fuzzy hyperalgebra, we assign the smallest equivalence relation α i 1 i 2 ∗ on a fuzzy hyperalgebra via identities where the factor hyperalgebra is a universal algebra. We extend and improve the identities on fuzzy hyperalgebras and characterize the smallest equivalence relation α J ∗ on the set of strong identities.

Cubical Agda: A dependently typed programming language with univalence and higher inductive types

2021 ◽  
Vol 31 ◽  
Author(s):  
ANDREA VEZZOSI ◽  
ANDERS MÖRTBERG ◽  
ANDREAS ABEL
Keyword(s):  
Programming Language ◽  
Type Theory ◽  
Type Checking ◽  
Dependent Type Theory ◽  
Wide Range ◽  
General Schema ◽  
Direct Definition ◽  
Inductive Types ◽  
Definition Of ◽  
Cubical Type Theory

Abstract Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types (HITs). This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of HITs. These new primitives allow the direct definition of function and propositional extensionality as well as quotient types, all with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. The adoption of cubical type theory extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.

scholarly journals Quotienting the delay monad by weak bisimilarity

2017 ◽  
Vol 29 (1) ◽  
pp. 67-92 ◽  
Author(s):  
JAMES CHAPMAN ◽  
TARMO UUSTALU ◽  
NICCOLÒ VELTRI
Keyword(s):  
Computer Science ◽  
Equivalence Relation ◽  
Type Theory ◽  
Partial Functions ◽  
Homotopy Type Theory ◽  
Inductive Type ◽  
Alternative Approach ◽  
The One ◽  
Axiom Of Countable Choice

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.

A TYPE-FREE THEORY OF HALF-MONOTONE INDUCTIVE DEFINITIONS

1995 ◽  
Vol 06 (03) ◽  
pp. 203-234 ◽  
Author(s):  
YUKIYOSHI KAMEYAMA
Keyword(s):  
Type Theory ◽  
Characteristic Point ◽  
Logical Theory ◽  
Inductive Definition ◽  
Program Extraction ◽  
First Order ◽  
Inductive Definitions ◽  
Free Theory ◽  
Program Proof ◽  
Definition Of

This paper studies an extension of inductive definitions in the context of a type-free theory. It is a kind of simultaneous inductive definition of two predicates where the defining formulas are monotone with respect to the first predicate, but not monotone with respect to the second predicate. We call this inductive definition half-monotone in analogy of Allen’s term half-positive. We can regard this definition as a variant of monotone inductive definitions by introducing a refined order between tuples of predicates. We give a general theory for half-monotone inductive definitions in a type-free first-order logic. We then give a realizability interpretation to our theory, and prove its soundness by extending Tatsuta’s technique. The mechanism of half-monotone inductive definitions is shown to be useful in interpreting many theories, including the Logical Theory of Constructions, and Martin-Löf’s Type Theory. We can also formalize the provability relation “a term p is a proof of a proposition P” naturally. As an application of this formalization, several techniques of program/proof-improvement can be formalized in our theory, and we can make use of this fact to develop programs in the paradigm of Constructive Programming. A characteristic point of our approach is that we can extract an optimization program since our theory enjoys the program extraction theorem.

A proof of the cut-elimination theorem in simple type theory

1973 ◽  
Vol 38 (2) ◽  
pp. 215-226
Author(s):  
Satoko Titani
Keyword(s):  
Boolean Algebra ◽  
Type Theory ◽  
Arbitrary Number ◽  
Formal System ◽  
Cut Elimination ◽  
Simple Type ◽  
Inductive Definition ◽  
Simple Type Theory ◽  
Maximal Ideals ◽  
Definition Of

In [4], I introduced a quasi-Boolean algebra, and showed that in a formal system of simple type theory, from which the cut rule is omitted, wffs form a quasi-Boolean algebra, and that the cut-elimination theorem can be formulated in algebraic language. In this paper we use the result of [4] to prove the cut-elimination theorem in simple type theory. The theorem was proved by M. Takahashi [2] in 1967 by using the concept of Schütte's semivaluation. We use maximal ideals of a quasi-Boolean algebra instead of semivaluations.The logical system we are concerned with is a modification of Schütte's formal system of simple type theory in [1] into Gentzen style.Inductive definition of types.0 and 1 are types.If τ1, …, τn are types, then (τ1, …, τn) is a type.Basic symbols.a1τ, a2τ, … for free variables of type τ.x1τ, x2τ, … for bound variables of type τ.An arbitrary number of constants of certain types.An arbitrary number of function symbols with certain argument places.

scholarly journals Transporting functions across ornaments

2014 ◽  
Vol 24 (2-3) ◽  
pp. 316-383 ◽  
Author(s):  
PIERRE-ÉVARISTE DAGAND ◽  
CONOR McBRIDE
Keyword(s):  
Type Theory ◽  
Structured Data ◽  
Dependent Types ◽  
Natural Numbers ◽  
Code Reuse ◽  
Domain Specific ◽  
Definition Of ◽  
The Relationship ◽  
Do So ◽  
Structural Invariants

AbstractProgramming with dependent types is a blessing and a curse. It is a blessing to be able to bake invariants into the definition of datatypes: We can finally write correct-by-construction software. However, this extreme accuracy is also a curse: A datatype is the combination of a structuring medium together with a special purpose logic. These domain-specific logics hamper any attempt to reuse code across similarly structured data. In this paper, we capitalise on the structural invariants of datatypes. To do so, we first adapt the notion of ornament to our universe of inductive families. We then show how code reuse can be achieved by ornamenting functions. Using these functional ornaments, we capture the relationship between functions such as the addition of natural numbers and the concatenation of lists. With this knowledge, we demonstrate how the implementation of the former informs the implementation of the latter: The users can ask the definition of addition to be lifted to lists and they will only be asked the details necessary to carry on adding lists rather than numbers. Our presentation is formalised in the type theory with a universe of datatypes and all our constructions have been implemented as generic programs, requiring no extension to the type theory.

Extending Gödel's negative interpretation to ZF

1975 ◽  
Vol 40 (2) ◽  
pp. 221-229 ◽  
Author(s):  
William C. Powell
Keyword(s):  
Set Theory ◽  
Type Theory ◽  
Stable Sets ◽  
Class Theory ◽  
Heyting Arithmetic ◽  
Inner Model ◽  
Order Arithmetic ◽  
Definition Of ◽  
Excluded Middle ◽  
Negative Sense

In [5] Gödel interpreted Peano arithmetic in Heyting arithmetic. In [8, p. 153], and [7, p. 344, (iii)], Kreisel observed that Gödel's interpretation extended to second order arithmetic. In [11] (see [4, p. 92] for a correction) and [10] Myhill extended the interpretation to type theory. We will show that Gödel's negative interpretation can be extended to Zermelo-Fraenkel set theory. We consider a set theory T formulated in the minimal predicate calculus, which in the presence of the full law of excluded middle is the same as the classical theory of Zermelo and Fraenkel. Then, following Myhill, we define an inner model S in which the axioms of Zermelo-Fraenkel set theory are true.More generally we show that any class X that is (i) transitive in the negative sense, ∀x ∈ X∀y ∈ x ¬ ¬ x ∈ X, (ii) contained in the class St = {x: ∀u(¬ ¬ u ∈ x→ u ∈ x)} of stable sets, and (iii) closed in the sense that ∀x(x ⊆ X ∼ ∼ x ∈ X), is a standard model of Zermelo-Fraenkel set theory. The class S is simply the ⊆-least such class, and, hence, could be defined by S = ⋂{X: ∀x(x ⊆ ∼ ∼ X→ ∼ ∼ x ∈ X)}. However, since we can only conservatively extend T to a class theory with Δ01-comprehension, but not with Δ11-comprehension, we will give a Δ01-definition of S within T.

Tychonoff's theorem in the framework of formal topologies

1997 ◽  
Vol 62 (4) ◽  
pp. 1315-1332 ◽  
Author(s):  
Sara Negri ◽  
Silvio Valentini
Keyword(s):  
Type Theory ◽  
Constructive Proof ◽  
Topological Product ◽  
Essential Difference ◽  
Constructive Type Theory ◽  
Constructive Type ◽  
Definition Of ◽  
The Axiom Of Choice ◽  
Inductive Property ◽  
Formal Topology

In this paper we give a constructive proof of the pointfree version of Tychonoff's theorem within formal topology, using ideas from Coquand's proof in [7]. To deal with pointfree topology Coquand uses Johnstone's coverages. Because of the representation theorem in [3], from a mathematical viewpoint these structures are equivalent to formal topologies but there is an essential difference also. Namely, formal topologies have been developed within Martin Löf's constructive type theory (cf. [16]), which thus gives a direct way of formalizing them (cf. [4]).The most important aspect of our proof is that it is based on an inductive definition of the topological product of formal topologies. This fact allows us to transform Coquand's proof into a proof by structural induction on the last rule applied in a derivation of a cover. The inductive generation of a cover, together with a modification of the inductive property proposed by Coquand, makes it possible to formulate our proof of Tychonoff s theorem in constructive type theory. There is thus a clear difference to earlier localic proofs of Tychonoff's theorem known in the literature (cf. [9, 10, 12, 14, 27]). Indeed we not only avoid to use the axiom of choice, but reach constructiveness in a very strong sense. Namely, our proof of Tychonoff's theorem supplies an algorithm which, given a cover of the product space, computes a finite subcover, provided that there exists a similar algorithm for each component space.

scholarly journals Univalent categories and the Rezk completion

2015 ◽  
Vol 25 (5) ◽  
pp. 1010-1039 ◽  
Author(s):  
BENEDIKT AHRENS ◽  
KRZYSZTOF KAPULKIN ◽  
MICHAEL SHULMAN
Keyword(s):  
Category Theory ◽  
Type Theory ◽  
Dependent Type Theory ◽  
Equivalence Of Categories ◽  
Segal Spaces ◽  
Definition Of ◽  
Categorical Semantics ◽  
Univalent Foundations ◽  
Dependent Type

We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition of ‘category’ for which equality and equivalence of categories agree. Such categories satisfy a version of the univalence axiom, saying that the type of isomorphisms between any two objects is equivalent to the identity type between these objects; we call them ‘saturated’ or ‘univalent’ categories. Moreover, we show that any category is weakly equivalent to a univalent one in a universal way. In homotopical and higher-categorical semantics, this construction corresponds to a truncated version of the Rezk completion for Segal spaces, and also to the stack completion of a prestack.

DETERMINISTIC AND NON-DETERMINISTIC ASYNCHRONOUS AUTOMATIC STRUCTURES

1992 ◽  
Vol 02 (03) ◽  
pp. 297-305 ◽  
Author(s):  
MICHAEL SHAPIRO
Keyword(s):  
Equivalence Relation ◽  
Automatic Structures ◽  
Fellow Traveller ◽  
Automatic Structure ◽  
Definition Of ◽  
Fellow Traveller Property

Following the definition of asynchronous automatic structures in [3], we define non-deterministic asynchronous automatic structures and characterize these in terms of the asynchronous fellow traveller property. We show that any group with a non-deterministic asynchronous automatic structure has an asynchronous automatic structure. Non-deterministic asynchronous automatic structures are a labor saving method of showing that a group has an asynchronous automatic structure. They also allow one to define an equivalence relation on the class of non-deterministic asynchronous automatic structures which descends to the subclasses of deterministic asynchronous automatic structures and synchronous automatic structures.

Sign in / Sign up

Export Citation Format

Share Document