桜井 貴文

It is observed that the proof of strong normalizability of typed terms of typed λ-calculus looks like the process of the model construction. The observation is clarified by the works of Hyland and Ong [8], Altenkirch [2], Stefanova and Geuvers [15], and so on. The model of Hyland and Ong is based on PL-category [14] and the model of Altenkirch or Stefanova and Geuvers is a non-categorical model that is specially designed for this purpose. In this paper, we will construct yet another categorical model for the second order λ-calculus — a non-extensional PL-category. To demonstrate the significance of the non-extensional model, we will give a model in which we can carry out the proof of the uniqueness of the β-normal form. The non-extensionality comes from the use of semi-adjoint for interpretation of abstraction and application (uncurry).