## Abstract

In a typing system, there are two approaches that may be taken to the

notion of equality. One can use some external relation of

convertibility defined on the terms of the grammar, such as

beta-convertibility or beta-eta-convertiblity; or one can

introduce a judgement form for equality into the rules of the typing

system itself.

For quite some time, it has been an open problem whether the two systems

produced by these two choices are equivalent. This problem is

essentially the problem of proving the Subject Reduction property

holds in the system with judgemental equality.

In this paper, we shall

prove that the equivalence holds for all functional Pure Type

Systems (PTSs). The proof essentially consists of proving the

Church-Rosser Theorem for a typed version of parallel one-step

reduction. This method should generalise easily to many typing

systems which satisfy the Uniqueness of Types property.

notion of equality. One can use some external relation of

convertibility defined on the terms of the grammar, such as

beta-convertibility or beta-eta-convertiblity; or one can

introduce a judgement form for equality into the rules of the typing

system itself.

For quite some time, it has been an open problem whether the two systems

produced by these two choices are equivalent. This problem is

essentially the problem of proving the Subject Reduction property

holds in the system with judgemental equality.

In this paper, we shall

prove that the equivalence holds for all functional Pure Type

Systems (PTSs). The proof essentially consists of proving the

Church-Rosser Theorem for a typed version of parallel one-step

reduction. This method should generalise easily to many typing

systems which satisfy the Uniqueness of Types property.

Original language | English |
---|---|

Pages (from-to) | 219-246 |

Number of pages | 28 |

Journal | Journal of Functional Programming |

Volume | 16 |

Issue number | 2 |

DOIs | |

Publication status | Published - 2006 |

## Keywords

- type theory
- pure type systems
- subject reduction