Lambda Calculus, Type Theory, and Natural Language II

2007 ◽  
Vol 18 (2) ◽  
pp. 203-203
Author(s):  
C. Fox ◽  
M. Fernandez ◽  
S. Lappin
Keyword(s):  
Natural Language ◽  
Type Theory ◽  
Lambda Calculus

Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention

2021 ◽  
pp. 1-20
Author(s):  
Ernesto Copello ◽  
Nora Szasz ◽  
Álvaro Tasistro
Keyword(s):  
Type Theory ◽  
Lambda Calculus ◽  
Proof Assistant ◽  
First Order ◽  
Constructive Type Theory ◽  
Fundamental Part ◽  
Constructive Type ◽  
Free Variables ◽  
The Church ◽  
Theoretical Results

Abstarct We formalize in Constructive Type Theory the Lambda Calculus in its classical first-order syntax, employing only one sort of names for both bound and free variables, and with α-conversion based upon name swapping. As a fundamental part of the formalization, we introduce principles of induction and recursion on terms which provide a framework for reproducing the use of the Barendregt Variable Convention as in pen-and-paper proofs within the rigorous formal setting of a proof assistant. The principles in question are all formally derivable from the simple principle of structural induction/recursion on concrete terms. We work out applications to some fundamental meta-theoretical results, such as the Church–Rosser Theorem and Weak Normalization for the Simply Typed Lambda Calculus. The whole development has been machine checked using the system Agda.

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 Some Lambda Calculus and Type Theory Formalized

1997 ◽  
Vol 4 (51) ◽  
Author(s):  
James McKinna ◽  
Robert Pollack
Keyword(s):  
Type Theory ◽  
Operational Semantics ◽  
Lambda Calculus ◽  
Type Systems ◽  
Formal Proof ◽  
Type Checking ◽  
Formal Development ◽  
Formal Definitions ◽  
Pure Type Systems ◽  
System F

"This paper is about our hobby." That is the first sentence of [MP93], the first report on our formal development of lambda calculus and type theory, written in autumn 1992. We have continued to pursue this hobby on and off ever since, and have developed a substantial body of formal knowledge, including Church-Rosser and standardization<br />theorems for beta reduction, and the basic theory of<br />Pure Type Systems (PTS) leading to the strengthening theorem and type checking algorithms for PTS. Some of this work is reported in [MP93, vBJMP94, Pol94b, Pol95]. In the present paper we survey this work, including some new proofs, and point out what we feel has been learned about the general issues of formalizing mathematics. On the technical side, we describe an abstract, and simplified, proof of standardization for beta reduction, not previously published, that does<br />not mention redex positions or residuals. On the general issues, we emphasize the search for formal definitions that are convenient for formal proof and convincingly represent the intended informal concepts. The LEGO Proof Development System [LP92] was used to check the work in an implementation of the Extended Calculus of Constructions<br />(ECC) with inductive types [Luo94]. LEGO is a refinement style<br />proof checker, publicly available by ftp and WWW, with a User's Manual [LP92] and a large collection of examples. Section 1.3 contains information on accessing the formal development described in this paper. Other interesting examples formalized in LEGO include program specification and data refinement [Luo91], strong normalization of System F [Alt93], synthetic domain theory [Reu95, Reu96], and operational semantics for imperative programs [Sch97].

scholarly journals Probabilistic Type Theory and Natural Language Semantics

2015 ◽  
Vol 10 ◽  
Author(s):  
Robin Cooper ◽  
Simon Dobnik ◽  
Shalom Lappin ◽  
Staffan Larsson
Keyword(s):  
Natural Language ◽  
Programming Languages ◽  
Type Theory ◽  
Probabilistic Reasoning ◽  
Syntactic Structure ◽  
Formal Semantics ◽  
Semantic Interpretation ◽  
Semantic Learning ◽  
History Of ◽  
Learning And Cognition

Type theory has played an important role in specifying the formal connection between syntactic structure and semantic interpretation within the history of formal semantics. In recent years rich type theories developed for the semantics of programming languages have become influential in the semantics of natural language. The use of probabilistic reasoning to model human learning and cognition has become an increasingly important part of cognitive science. In this paper we offer a probabilistic formulation of a rich type theory, Type Theory with Records (TTR), and we illustrate how this framework can be used to approach the problem of semantic learning. Our probabilistic version of TTR is intended to provide an interface between the cognitive process of classifying situations according to the types that they instantiate, and the compositional semantics of natural language.

scholarly journals Static and dynamic vector semantics for lambda calculus models of natural language

2019 ◽  
Vol 6 (2) ◽  
pp. 319 ◽  
Author(s):  
Mehrnoosh Sadrzadeh ◽  
Reinhard Muskens
Keyword(s):  
Natural Language ◽  
Lambda Calculus
Sign in / Sign up

Export Citation Format

Share Document