Extensional PERs

In the paper "Extensional PERs" by P. Freyd, P. Mulry, G. Rosolini and D. Scott, a category C of "pointed complete extensional PERs" and computable maps is introduced to provide an instance of an algebraically compact category relative to a restricted class of functors. Algebraic compactness is a synthetic condition on a category which ensures solutions of recursive equations involving endofunctors of the category. We extend that result to include all internal functors on C when C is viewed as a full internal category of the effective topos. This is done using two general results: one about internal functors in general, and one about internal functors in the effective topos. The paper "Extensional PERs" by P.Freyd, P.Mulry, G.Rosolini and D.Scott [2] identifies a reflective subcategory of the category of PERs, namely the category C of pointed CEPERs

• Type: Conference
• Year: 1990
• Where: LICS
• Authors: Peter J. Freyd, P. Mulry, Giuseppe Rosolini, Dana S. Scott
• Keywords: Algebraic Compactness, Automated Reasoning, Extensional Pers, Internal Functors, LICS 1990