Pure Type System conversion is always typable

AbstractPure Type Systems are usually described in two different ways, one that uses an external notion of computation like beta-reduction, and one that relies on a typed judgment of equality, directly in the typing system. For a long time, the question was open to know whether both presentations described the same theory. A first step towards this equivalence has been made by Adams for a particular class ofPure Type Systems(PTS) called functional. Then, his result has been relaxed to all semi-full PTSs in previous work. In this paper, we finally give a positive answer to the general question, and prove that equivalence holds for any Pure Type System.

Download Full-text

ON THE CONSERVATIVITY OF LEIBNIZ EQUALITY

International Journal of Foundations of Computer Science ◽

10.1142/s0129054198000325 ◽

1998 ◽

Vol 09 (04) ◽

pp. 431-454

Author(s):

M. P. A. SELLINK

Keyword(s):

Type System ◽

Type Systems ◽

Order Theory ◽

Second Order ◽

First Order ◽

Pure Type ◽

First Order Theory ◽

Pure Type Systems ◽

Leibniz Equality

We embed a first order theory with equality in the Pure Type System λMON2 that is a subsystem of the well-known type system λPRED2. The embedding is based on the Curry-Howard isomorphism, i.e. → and ∀ coincide with → and Π. Formulas of the form [Formula: see text] are treated as Leibniz equalities. That is, [Formula: see text] is identified with the second order formula ∀ P. P(t1)→ P(t2), which contains only →'s and ∀'s and can hence be embedded straightforwardly. We give a syntactic proof — based on enriching typed λ-calculus with extra reduction steps — for the equivalence between derivability in the logic and inhabitance in λMNO2. Familiarity with Pure Type Systems is assumed.

Download Full-text

Reduction Strategies for Program Extraction

CLEI electronic journal ◽

10.19153/cleiej.6.1.2 ◽

2018 ◽

Vol 6 (1) ◽

Author(s):

Maribel Fernandez ◽

Ian Mackie ◽

Paula Severi ◽

Nora Szasz

Keyword(s):

Type System ◽

Lambda Calculus ◽

General Setting ◽

Type Systems ◽

Program Extraction ◽

Pure Type ◽

Typed Lambda Calculus ◽

Reduction Strategies ◽

Pure Type Systems ◽

Reduction Relation

We introduce Pure Type Systems with Pairs generalising earlier work on program extraction in Typed Lambda Calculus. We model the process of program extraction in these systems by means of a reduction relation called o-reduction, and give strategies for Bo-reduction which will be useful for an implementation of a proof assistant. More precisely, we give an algorithm to compute theo-normal form of a term in Pure Type System with Pairs, and show that this defines a prejection from Pure Type Systems with Pairs to standart Pure Type Systems. This result shows that o-reduction is an operational description of aprgram extraction that is independent of the particular Typed Lambda Calculus specified as a Pure Typoe System. For B-reduction, we define weak and strong reduction strategies using Interaction Nets, generalising well-know efficient strategies for the l-calculus to the general setting of Pure Type Systems.

Download Full-text