scholarly journals INTERSECTION TYPE SYSTEM AND LAMBDA CALCULUS WITH DIRECTOR STRINGS

2019 ◽  
Author(s):  
Xinxin Shen ◽  
Kougen Zheng
Keyword(s):  
Type System ◽  
Lambda Calculus

Coherence of subsumption, minimum typing and type-checking in F ≤

1992 ◽  
Vol 2 (1) ◽  
pp. 55-91 ◽  
Author(s):  
Pierre-Louis Curien ◽  
Giorgio Ghelli
Keyword(s):  
Normal Form ◽  
Type System ◽  
Lambda Calculus ◽  
Complete Information ◽  
Second Order ◽  
Semantic Interpretation ◽  
Type Checking ◽  
Rewriting System ◽  
Different Types ◽  
Rewriting Rules

A subtyping relation ≤ between types is often accompanied by a typing rule, called subsumption: if a term a has type T and T≤U, then a has type U. In presence of subsumption, a well-typed term does not codify its proof of well typing. Since a semantic interpretation is most naturally defined by induction on the structure of typing proofs, a problem of coherence arises: different typing proofs of the same term must have related meanings. We propose a proof-theoretical, rewriting approach to this problem. We focus on F≤, a second-order lambda calculus with bounded quantification, which is rich enough to make the problem interesting. We define a normalizing rewriting system on proofs, which transforms different proofs of the same typing judgement into a unique normal proof, with the further property that all the normal proofs assigning different types to a given term in a given environment differ only by a final application of the subsumption rule. This rewriting system is not defined on the proofs themselves but on the terms of an auxiliary type system, in which the terms carry complete information about their typing proof. This technique gives us three different results:— Any semantic interpretation is coherent if and only if our rewriting rules are satisfied as equations.— We obtain a proof of the existence of a minimum type for each term in a given environment.— From an analysis of the shape of normal form proofs, we obtain a deterministic typechecking algorithm, which is sound and complete by construction.

Operations on records

1991 ◽  
Vol 1 (1) ◽  
pp. 3-48 ◽  
Author(s):  
Luca Cardelli ◽  
John C. Mitchell
Keyword(s):  
Type System ◽  
Lambda Calculus ◽  
Object Oriented ◽  
Order Type ◽  
Second Order ◽  
Typed Lambda Calculus ◽  
Semantic Models ◽  
Object Oriented Languages

We define a simple collection of operations for creating and manipulating record structures, where records are intended as finite associations of values to labels. A second-order type system over these operations supports both subtyping and polymorphism. We provide typechecking algorithms and limited semantic models.Our approach unifies and extends previous notions of records, bounded quantification, record extension, and parametrization by row-variables. The general aim is to provide foundations for concepts found in object-oriented languages, within a framework based on typed lambda-calculus.

scholarly journals A Complete Calculus of Monotone and Antitone Higher-Order Functions

10.29007/3n54 ◽  
2018 ◽  
Author(s):  
Thomas Icard ◽  
Lawrence Moss
Keyword(s):  
Type System ◽  
Lambda Calculus ◽  
Higher Order ◽  
Typed Lambda Calculus ◽  
Higher Order Functions

This paper adds monotonicity and antitonicity information to the typed lambda calculus, thereby providing a foundation for the Monotonicity Calculus first developed by van Benthem and others. We establish properties of the type system, propose a syntax, semantics, and proof calculus, and prove completeness for the calculus with respect to hierarchies of monotone and antitone functions over base preorders.

Linearization of the lambda-calculus and its relation with intersection type systems

2004 ◽  
Vol 14 (5) ◽  
pp. 519-546 ◽  
Author(s):  
MÁRIO FLORIDO ◽  
LUÍS DAMAS
Keyword(s):  
Programming Languages ◽  
Functional Programming ◽  
Type System ◽  
Lambda Calculus ◽  
Type Systems ◽  
Functional Programming Languages

In this paper we present a notion of expansion of a term in the lambda-calculus which transforms terms into linear terms. This transformation replaces each occurrence of a variable in the original term by a fresh variable taking into account non-trivial implications in the structure of the term caused by these simple replacements. We prove that the class of terms which can be expanded is the same of terms typable in an Intersection Type System, i.e. the strongly normalizable terms. We then show that expansion is preserved by weak-head reduction, the reduction considered by functional programming languages.

scholarly journals Transforming Dependency Structures to Logical Forms for Semantic Parsing

2016 ◽  
Vol 4 ◽  
pp. 127-140 ◽  
Author(s):  
Siva Reddy ◽  
Oscar Täckström ◽  
Michael Collins ◽  
Tom Kwiatkowski ◽  
Dipanjan Das ◽  
...  
Keyword(s):  
Type System ◽  
Lambda Calculus ◽  
Syntactic Analysis ◽  
Strong Type ◽  
Semantic Parsing ◽  
Syntactic Structures ◽  
Formal Mechanism ◽  
Dependency Trees ◽  
Dependency Structures ◽  
Grammar Formalisms

The strongly typed syntax of grammar formalisms such as CCG, TAG, LFG and HPSG offers a synchronous framework for deriving syntactic structures and semantic logical forms. In contrast—partly due to the lack of a strong type system—dependency structures are easy to annotate and have become a widely used form of syntactic analysis for many languages. However, the lack of a type system makes a formal mechanism for deriving logical forms from dependency structures challenging. We address this by introducing a robust system based on the lambda calculus for deriving neo-Davidsonian logical forms from dependency trees. These logical forms are then used for semantic parsing of natural language to Freebase. Experiments on the Free917 and Web-Questions datasets show that our representation is superior to the original dependency trees and that it outperforms a CCG-based representation on this task. Compared to prior work, we obtain the strongest result to date on Free917 and competitive results on WebQuestions.

scholarly journals An error-tolerant type system for variational lambda calculus

2012 ◽  
Vol 47 (9) ◽  
pp. 29-40 ◽  
Author(s):  
Sheng Chen ◽  
Martin Erwig ◽  
Eric Walkingshaw
Keyword(s):  
Type System ◽  
Lambda Calculus

scholarly journals The algebraic lambda calculus

2009 ◽  
Vol 19 (5) ◽  
pp. 1029-1059 ◽  
Author(s):  
LIONEL VAUX
Keyword(s):  
Vector Space ◽  
Natural Extension ◽  
Type System ◽  
Lambda Calculus ◽  
Simple Type ◽  
Linear Combinations ◽  
Fixed Set ◽  
Definition Of

We introduce an extension of the pure lambda calculus by endowing the set of terms with the structure of a vector space, or, more generally, of a module, over a fixed set of scalars. Moreover, terms are subject to identities similar to the usual pointwise definition of linear combinations of functions with values in a vector space. We then study a natural extension of beta reduction in this setting: we prove it is confluent, then discuss consistency and conservativity over the ordinary lambda calculus. We also provide normalisation results for a simple type system.

Sign in / Sign up

Export Citation Format

Share Document