Categorical properties of logical frameworks
YUXI FU a1 fn1
a1 Department of Computer Science, University of Manchester, Manchester M13 9PL, England
In this paper we define a logical framework, called &;lambda;TT, that is well suited for semantic analysis. We introduce the notion of a fibration [script L]1 : [script F]1 [longrightarrow A: long right arrow] [script C] 1 being internally definable fn3 in a fibration [script L]2 : [script F]2 [longrightarrow A: long right arrow] [script C] 2. This notion amounts to distinguishing an internal category L in [script L]2 and relating [script L]1 to the externalization of L through a pullback. When both [script L]1 and [script L]2 are term models of typed calculi [script L]1 and [script L]2, respectively, we say that [script L]1 is an internal typed calculus definable in the frame language [script L]2. We will show by examples that if an object language is adequately represented in [lambda]TT, then it is an internal typed calculus definable in the frame language [lambda]TT. These examples also show a general phenomenon: if the term model of an object language has categorical structure S, then an adequate encoding of the language in [lambda]TT imposes an explicit internal categorical structure S in the term model of [lambda]TT and the two structures are related via internal definability. Our categorical investigation of logical frameworks indicates a sensible model theory of encodings.(Received March 8 1993)
(Revised October 18 1995)
Present address: Department of Computer Science, Shanghai Jiao Tong University, 1954 Hua Shan Road, Shanghai 200030, People's Republic of China.
fn1 During the preparation of this paper, the author was supported by the CLICS-II project. In the later stage of the preparation, he was under the 863 Project.
fn3 The definability as used in this paper should not be confused with Bénabou's ‘definability’ (Bénabou 1985).