Affiliations: Prolog Development Center A/S, H.J. Holst Vej 3-5A, DK-2605 Brøndby, Denmark. Email: [email protected] | DIKU, University of Copenhagen, DK-2100 Copenhagen, Denmark. Email: [email protected]
Abstract: We present new sound and complete axiomatizations of type equality and subtype inequality for a first-order type language with regular recursive types. The rules are motivated by coinductive characterizations of type containment and type equality via simulation and bisimulation, respectively. The main novelty of the axiomatization is the fixpoint rule (or coinduction principle). It states that from A,P $\vdash$ P one may deduce A $\vdash$ P, where P is either a type equality τ = τ' or type containment τ ≤ τ' and the proof of the premise must be contractive in a sense we define in this paper. In particular, a proof of A, P $\vdash$ P using the assumption axiom is not contractive. The fixpoint rule embodies a finitary coinduction principle and thus allows us to capture a coinductive relation in the fundamentally inductive framework of inference systems. The new axiomatizations are more concise than previous axiomatizations, particularly so for type containment since no separate axiomatization of type equality is required, as in Amadio and Cardelli's axiomatization. They give rise to a natural operational interpretation of proofs as coercions. In particular, the fixpoint rule corresponds to definition by recursion. Finally, the axiomatization is closely related to (known) efficient algorithms for deciding type equality and type containment. These can be modified to not only decide type equality and type containment, but also construct proofs in our axiomatizations efficiently. In connection with the operational interpretation of proofs as coercions this gives efficient (O(n2) time) algorithms for constructing efficient coercions from a type to any of its supertypes or isomorphic types. More generally, we show how adding the fixpoint rule makes it possible to characterize inductively a set that is coinductively defined as the kernel (greatest fixed point) of an inference system.
