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.

The calculus of dependent lambda eliminations

2017 ◽  
Vol 27 ◽  
Author(s):  
AARON STUMP
Keyword(s):  
Type Theory ◽  
Lambda Calculus ◽  
Denotational Semantics ◽  
Prototype Implementation ◽  
Constructive Type Theory ◽  
Typed Lambda Calculus ◽  
Constructive Type

AbstractModern constructive type theory is based on pure dependently typed lambda calculus, augmented with user-defined datatypes. This paper presents an alternative called the Calculus of Dependent Lambda Eliminations, based on pure lambda encodings with no auxiliary datatype system. New typing constructs are defined that enable induction, as well as large eliminations with lambda encodings. These constructs are constructor-constrained recursive types, and a lifting operation to lift simply typed terms to the type level. Using a lattice-theoretic denotational semantics for types, the language is proved logically consistent. The power of CDLE is demonstrated through several examples, which have been checked with a prototype implementation called Cedille.

scholarly journals Provable isomorphisms of types

1992 ◽  
Vol 2 (2) ◽  
pp. 231-247 ◽  
Author(s):  
Kim B. Bruce ◽  
Roberto Di Cosmo ◽  
Giuseppe Longo
Keyword(s):  
Propositional Logic ◽  
Lambda Calculus ◽  
Close Relation ◽  
Typed Lambda Calculus ◽  
Definition Of

A constructive characterization is given of the isomorphisms which must hold in all models of the typed lambda calculus with surjective pairing. Using the close relation between closed Cartesian categories and models of these calculi, we also produce a characterization of those isomorphisms which hold in all CCC's. Using the correspondence between these calculi and proofs in intuitionistic positive propositional logic, we thus provide a characterization of equivalent formulae of this logic, where the definition of equivalence of terms depends on having “invertible” proofs between the two terms. Work of Rittri (1989), on types as search keys in program libraries, provides an interesting example of use of these characterizations.

Lambda calculus

2018 ◽  
Author(s):  
David Charles McCarty
Keyword(s):  
Twentieth Century ◽  
Functional Model ◽  
Lambda Calculus ◽  
Denotational Semantics ◽  
The Other ◽  
Finite Chain ◽  
Close Correspondence ◽  
Special Mention ◽  
Definition Of ◽  
Mathematical Operations

The lambda calculus presents a delimited formal setting for expressing and studying properties of mathematical operations and computer programs. Its syntactical unit is the term. Application terms tu represent supplying argument u to routine t. Abstraction terms λx. t (in which λx binds x in t) represent the explicit definition of an operation from a routine t. Term computation is by reduction: (λx. t) (u) reduces to t[x/u], the result of substituting u for x in t; this corresponds to operating with t on u. Terms are equal either when they differ only in bound variables or when one converts to the other via a finite chain of reductions and counter-reductions. There are two main varieties of lambda calculi: typed and untyped (or type-free). Any untyped term is applicable to any other and equality between such terms is undecidable. In the typed case, terms are indexed by types and application is permitted only when types conform. Here, equality is decidable. A. Church proposed formalisms for both varieties during the 1930s. He and his students S. Kleene and J. Rosser proved the early syntactical metatheorems linking the untyped calculus with computability theory. In 1969, D. Scott gave the first set-theoretic construction of a functional model of the untyped calculus; since then, many other models have been devised. As for the typed calculus, Gödel’s Dialectica interpretation inspired many of its applications to proof theory. Also, the idea, due to H. Curry and W. Howard, of using logical formulas as types reveals a close correspondence between typed terms and derivations in intuitionistic formal systems. In the last decades of the twentieth century, the lambda calculus and its models have been put to many uses in computer science, with functional programming and denotational semantics deserving special mention.

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 Backpropagation in the simply typed lambda-calculus with linear negation

2020 ◽  
Vol 4 (POPL) ◽  
pp. 1-27 ◽  
Author(s):  
Aloïs Brunel ◽  
Damiano Mazza ◽  
Michele Pagani
Keyword(s):  
Lambda Calculus ◽  
Typed Lambda Calculus

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.

scholarly journals L2-BETTI NUMBERS OF DISCRETE MEASURED GROUPOIDS

2005 ◽  
Vol 15 (05n06) ◽  
pp. 1169-1188 ◽  
Author(s):  
ROMAN SAUER
Keyword(s):  
Probability Space ◽  
Betti Numbers ◽  
Free Action ◽  
Countable Group ◽  
Equivalence Relations ◽  
Dimension Theory ◽  
Discrete Groups ◽  
Type Ii ◽  
Orbit Equivalent ◽  
Definition Of

There are notions of L2-Betti numbers for discrete groups (Cheeger–Gromov, Lück), for type II1-factors (recent work of Connes-Shlyakhtenko) and for countable standard equivalence relations (Gaboriau). Whereas the first two are algebraically defined using Lück's dimension theory, Gaboriau's definition of the latter is inspired by the work of Cheeger and Gromov. In this work we give a definition of L2-Betti numbers of discrete measured groupoids that is based on Lück's dimension theory, thereby encompassing the cases of groups, equivalence relations and holonomy groupoids with an invariant measure for a complete transversal. We show that with our definition, like with Gaboriau's, the L2-Betti numbers [Formula: see text] of a countable group G coincide with the L2-Betti numbers [Formula: see text] of the orbit equivalence relation [Formula: see text] of a free action of G on a probability space. This yields a new proof of the fact the L2-Betti numbers of groups with orbit equivalent actions coincide.

The Simply Typed Lambda Calculus

2013 ◽  
pp. 5-54
Author(s):  
Henk Barendregt ◽  
Wil Dekkers ◽  
Richard Statman
Keyword(s):  
Lambda Calculus ◽  
Typed Lambda Calculus
Sign in / Sign up

Export Citation Format

Share Document