Normalisation, approximation and semantics for typeable combinator systems
File(s)DTR00-10.pdf (620.11 KB)
Technical report
Author(s)
van Bakel,S.
Fernndez,M.
Type
Report
Abstract
This paper studies normalization of typeable terms and the relation between approximation semantics and filter models for Combinator Systems. It presents notions of approximants for terms, intersection type assignment, and reduction on type derivations; the last will be proved to be strongly normalizable. With this result, it is shown that, for every typeable term, there exists an approximant with the same type, and a characterization of the normalization behaviour of terms using their assignable types is given. Then the two semantics are defined and compared, and it is shown that the approximants semantics is fully abstract but the filter semantics is not.
Date Issued
2000-01-01
Citation
Departmental Technical Report: 2000/10, 2000, pp.1-32
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
32
Journal / Book Title
Departmental Technical Report: 2000/10
Copyright Statement
© 2000 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
10