Paper Info
Title
Kripke models and the (in)equational logic of the second-order λ-calculus
Abstract
We define a new class of Kripke structures for the second-order λ-calculus, and investigate the soundness and completeness of some proof systems for proving inequalities (rewrite rules) as well as equations. The Kripke structures under consideration are equipped with preorders that correspond to an abstract form of reduction, and they are not necessarily extensional. A novelty of our approach is that we define these structures directly as functors A: W → Preor equipped with certain natural transformations corresponding to application and abstraction (where W is a preorder, the set of worlds, and Preor is the category of preorders). We make use of an explicit construction of the exponential of functors in the Cartesian-closed category PreorW, and we also define a kind of exponential ΠΦ(As)s ϵ T to take care of type abstraction. However, we strive for simplicity, and we only use very elementary categorical concepts. Consequently, we believe that the models described in this paper are more palatable than abstract categorical models which require much more sophisticated machinery (and are not models of rewrite rules anyway). We obtain soundness and completeness theorems that generalize some results of Mitchell and Moggi to the second-order λ-calculus, and to sets of inequalities (rewrite rules).
Year
DOI
Venue
1997
10.1016/S0168-0072(96)00039-5
Annals of Pure and Applied Logic
Keywords
Field
DocType
equational logic,lambda calculus,natural transformation,second order
Kripke structure,Discrete mathematics,Abstraction,Algebra,Categorical variable,Preorder,Functor,Soundness,Equational logic,Completeness (statistics),Mathematics
Journal
Volume
Issue
ISSN
84
3
0168-0072
Citations 
PageRank 
References 
0
0.34
10
Authors
1
Name
Order
Citations
PageRank
Jean H. Gallier1749111.86