Relative Properties of Frame Language  

作　　者：傅育熙 

出　　处：《Journal of Computer Science & Technology》1999年第4期320-327,共8页计算机科学技术学报（英文版）

摘　　要：The paper discusses semalltics of encodings in logical frameworkswhere equalities in object calculi are represented by families of types as the case inELF. The notion of Leibniz equality in a category is introduced. Two morphisms ina category are Leibniz equal if they are seen so by an internal category. The usualcategorical properties are then relativized to r-properties by requiring mediatingmorphisms to be unique up to some Leibniz equality. Using these terminologies,it is shown, by an example, that the term model of the encoding of an adequatelyrepresented object calculus is r-isomorphic to the term model of the object language.The paper discusses semalltics of encodings in logical frameworkswhere equalities in object calculi are represented by families of types as the case inELF. The notion of Leibniz equality in a category is introduced. Two morphisms ina category are Leibniz equal if they are seen so by an internal category. The usualcategorical properties are then relativized to r-properties by requiring mediatingmorphisms to be unique up to some Leibniz equality. Using these terminologies,it is shown, by an example, that the term model of the encoding of an adequatelyrepresented object calculus is r-isomorphic to the term model of the object language.

关 键 词：logical framework categorical semantics syntactical adequacy 

分 类 号：TP313[自动化与计算机技术—计算机软件与理论]