\documentstyle[11pt,fullpage]{article}
%
%
%    LaTeX  Macro File  
%
\newcommand{\mathify}[1]{\ifmmode{#1}\else\mbox{$#1$}\fi}
\long\def\comment#1{} % multi-line comments
\newtheorem{thm}{Theorem}[section]
\newtheorem{theorem}[thm]{Theorem}
\newtheorem{lemma}[thm]{Lemma}
\newtheorem{cor}[thm]{Corollary}
\newtheorem{corollary}[thm]{Corollary}
\newtheorem{claim}[thm]{Claim}
\newtheorem{prop}[thm]{Proposition}
\newtheorem{conj}[thm]{Conjecture}
\newtheorem{open}[thm]{Open Problem}
\newenvironment{definition}
  {\refstepcounter{thm}\begin{trivlist}\item[\hskip\labelsep{\bf Definition \thetheorem}]}{\end{trivlist}}
\newenvironment{remark}
  {\begin{trivlist}\item[\hskip\labelsep{\bf Remark:}]}{\end{trivlist}}
\newenvironment{example}
  {\begin{trivlist}\item[\hskip\labelsep{\bf Example:}]}{\end{trivlist}}


%------------------Fonts -----------------------------------------
\renewcommand{\i}[1]{{\it #1\/}}       % italics with space correction
\renewcommand{\c}[1]{{\sc #1}}       % small caps (eliminates \c as
				     % cedilla) 
\newcommand{\r}[1]{{\rm #1}}            % for roman font in math mode
\newcommand{\s}[1]{{\cal #1}}
\renewcommand{\b}[1]{\mathify{\bf #1}}
\newcommand{\bm}[1]{\mbox{\boldmath \mathify{#1}}}  % bold in math
						      % mode
\newcommand{\calg}[1]{{\cal #1}}          % caligraphic 
\newcommand{\q}[1]{``#1''}    % matching quotes for in-line quotation


% ------------------Latin abbreviations-------------------------------
\newcommand{\viz}{{\em viz.}}
\newcommand{\Viz}{{\em Viz.}}
\newcommand{\cf}{{\em c.f.\,}}
\newcommand{\Cf}{{\em Cf.}}
\newcommand{\ie}{{\em i.e.}}
\newcommand{\Ie}{{\em I.e.}}
\newcommand{\eg}{{\em e.g.}}
\newcommand{\Eg}{{\em E.g.}}
\newcommand{\etal}{{\em et al.}}

%-------------------New mathematics symbols---------------------------
\newfont{\mxth}{msam10}
\newfont{\myth}{msbm10}
\newcommand{\mathnat}{\mbox{{\myth \symbol{'116}}}}
\newcommand{\mathint}{\mbox{{\myth \symbol{'132}}}}
\newcommand{\mathbool}{\mbox{{\myth \symbol{'102}}}}
\newcommand{\mathreal}{\mbox{{\myth \symbol{'122}}}}
\newcommand{\Ldot}{\mbox{{\mxth \symbol{'005}}}}
\newcommand{\wigglyrightarrow}{\mbox{{\mxth \symbol{'040}}}}
\newcommand{\sqlambda}{\mbox{{\mxth \symbol{'150}}}}
\newcommand{\lcorner}{\mbox{{\mxth \symbol{'160}}}}
\newcommand{\rcorner}{\mbox{{\mxth \symbol{'161}}}}
\newcommand{\aarrow}{\mbox{{\mxth \symbol{'020}}}}   % double-head right arrow
\newcommand{\laarrow}{\mbox{{\mxth \symbol{'021}}}}  % double-head left arrow
\newcommand{\notarrow}{\mbox{{\myth \symbol{'071}}}} % crossed-out \rightarrow
\newcommand{\restr}{\mbox{{\mxth \symbol{'026}}}}    % restriction symbol
\newcommand{\dotlt}{\mbox{{\myth \symbol{'154}}}}    % < with a dot in
\newcommand{\notmod}{\mbox{{\myth \symbol{'062}}}}   % negated models
\newcommand{\monus}{{\dot{-}}}
\newcommand{\lthresh}{\mbox{{\mxth \symbol{'126}}}}
\newcommand{\Inclpred}{\mbox{{\mxth \symbol{'056}}}}
\newcommand{\inclpred}[1]{\;\Inclpred^{#1}\;}
\mathcode`:="603A  % treat : as punctuation instead of relation in
		   % math mode
\mathchardef\colon="303A	% relation colon


%-------------------Aliases for LaTeX math symbols-------------------

\newcommand{\tuple}[1]{\mathify{\left\langle #1 \right\rangle}}
\newcommand{\set}[1]{\mathify{ \{ #1 \} }}
\newcommand{\sle}{\sqsubseteq}
\newcommand{\gle}{\sqsupseteq}
\newcommand{\sge}{\sqsupseteq}
\newcommand{\keq}{\simeq}         % Kleene equality
\newcommand{\ceil}[1]{\mathify{\left\lceil #1 \right\rceil}}
\newcommand{\floor}[1]{\mathify{\left\lfloor #1 \right\rfloor}}
\newcommand{\logor}{\vee}
\newcommand{\logand}{\wedge}
\newcommand{\Logor}{\bigvee}
\newcommand{\Logand}{\bigwedge}
\newcommand{\logimply}{\Rightarrow}
\newcommand{\lognot}{\neg}
\newcommand{\imp}{\Rightarrow}
\newcommand{\univ}[2]{\forall #1. #2}
\newcommand{\exist}[2]{\exists #1. #2}
\newcommand{\fa}{\forall}
\newcommand{\te}{\exists}
\newcommand{\ts}{\vdash}
\newcommand{\dts}{\models}
\newcommand{\apply}{\mathrel{\bullet}}
\newcommand{\Lcal}{L}
\newcommand{\Tcal}{{\cal T}}
\newcommand{\Dcal}{{\cal D}}
\newcommand{\Union}{\bigcup}
\newcommand{\union}{\cup}
\newcommand{\intersect}{\cap}
\newcommand{\Lub}{\bigsqcup}
\newcommand{\lub}{\sqcup}
\newcommand{\glb}{\sqcap}
\newcommand{\Glb}{\bigsqcap}
\newcommand{\sims}{\rightleftharpoons}
\newcommand{\compose}{\circ}
\newcommand{\code}[1]{\lcorner #1 \rcorner}
\newcommand{\el}{\in}
\newcommand{\nel}{\not\in}
\newcommand{\ns}{\emptyset}

%------------------Kleene symbols------------------------------------
\makeatletter
\def\@versima#1#2{\lower1\p@\vbox{\baselineskip\z@skip\lineskip-1.5\p@
    \ialign{$\m@th#1\hfil##\hfil$\crcr#2\crcr\mathop{\sim}\crcr}}}
\def\oversima#1{\mathrel{\mathpalette\@versima#1}}
\def\@versimb#1#2{\lower2.5\p@\vbox{\baselineskip\z@skip\lineskip1\p@
    \ialign{$\m@th#1\hfil##\hfil$\crcr#2\crcr\mathop{\sim}\crcr}}}
\def\oversimb#1{\mathrel{\mathpalette\@versimb#1}}
\makeatother

\def\miseq{\oversima{{-\!\!\!\!-}}}
\def\misle{\oversimb{\sqsubset}}
\def\misge{\oversimb{\sqsupset}}
\newcommand{\kleq}{\mathify{\scriptstyle \misle}}
\newcommand{\kgeq}{\mathify{\scriptstyle \misge}}



%-------------------Rules---------------------------------------------

\newcommand{\axiom}[2]
{\[ \hbox to \columnwidth
    { \rlap{$#2$} \hfil {$ #1 $} \hfil }
\]}

\newcommand{\infrule}[4]
{\[ \hbox to \columnwidth 
    { \rlap{$#4$} \hfil $
      \frac {\strut\displaystyle #1 } {\strut\displaystyle #2 } \; \rlap{$#3$} $
      \hfil }
\]}
\newcommand{\infruletw}[4]
{\[ \hbox to \textwidth
    { \rlap{$#4$} \hfil $
      \frac {\strut\displaystyle #1 } {\strut\displaystyle #2 } \; \rlap{$#3$} $
      \hfil }
\]}

% axiom and inference rule macros for use in tables, etc.
% presumed in math mode #1=axiom, #2=side condition
\newcommand{\Axiom}[2]{
{\displaystyle\strut #1}\qquad\makebox[0pt][l]{\it #2}
}
% presumed in math mode #1=top, #2=bottom, #3=side condition
\newcommand{\Infrule}[3]{
{{\displaystyle\strut #1}\over{\displaystyle\strut #2}}\qquad\makebox[0pt][l]{\it #3}
}

%------------------Combinators for functional programming-------------

% Ordinary PCF
\newcommand{\TT}{\rlap{\rm t}\kern .5ex{\rm t}}
\newcommand{\ff}{\rlap{\rm f}\kern .5ex{\rm f}}
\newcommand{\Pred}{\mbox{\sf pred}}
\newcommand{\Succ}{\mbox{\sf succ}}
\newcommand{\pred}[1]{\mathify{\Pred(#1)}}
\renewcommand{\succ}[1]{\mathify{\Succ(#1)}}
\newcommand{\valueY}{\mbox{\sf Y}_v}
\newcommand{\Y}{\mbox{\sf Y}}
\newcommand{\Cond}{\mbox{\sf cond}}
\newcommand{\cond}[3]{\mathify{\Cond \: #1 \: #2 \: #3}}
\newcommand{\Ifz}{\mbox{\sf if0}}
\newcommand{\ifz}[3]{\mathify{\Ifz(#1,#2,#3)}}
\newcommand{\Pcond}{\mbox{\sf pcond}}
\newcommand{\pcond}[3]{\mathify{\Pcond \: #1 \: #2 \: #3}}
\newcommand{\Vcond}{\mbox{\sf vcond}}
\newcommand{\vcond}[3]{\mathify{\Vcond \: #1 \: #2 \: #3}}
\newcommand{\por}{\mbox{\sf por}}
\newcommand{\Unity}{\mbox{\bf unity}}
\newcommand{\Intro}{\mbox{\bf intro}}
\newcommand{\Elim}{\mbox{\bf elim}}
\newcommand{\Projo}[1]{\mbox{{\sf Proj}_{1}^{#1}}}
\newcommand{\Projt}[1]{\mbox{{\sf Proj}_{2}^{#1}}}
\newcommand{\Proji}[1]{\mbox{{\sf Proj}_{i}^{#1}}}
\newcommand{\Fst}{\mbox{\bf Fst}}
\newcommand{\Snd}{\mbox{\bf Snd}}
\newcommand{\Pair}{\it pr}
\newcommand{\fst}[1]{\mathify{(#1)_1}}
\newcommand{\snd}[1]{\mathify{(#1)_2}}
\newcommand{\pair}[1]{\Pair(#1)}
\newcommand{\Inl}{\mbox{\bf inl}}
\newcommand{\Inr}{\mbox{\bf inr}}
\newcommand{\Case}{\mbox{\bf case}}
\newcommand{\inl}[1]{\Inl(#1)}
\newcommand{\inr}[1]{\Inr(#1)}
\newcommand{\case}[3]{\Case(#1,#2,#3)}
\renewcommand{\int}{{\it int}}
\newcommand{\nat}{{\it nat}}
\newcommand{\bool}{{\it bool}}
\newcommand{\strng}{{\it string}}
\newcommand{\unit}{\mbox{\sf 1\hspace{-5.5pt}1}}
\newcommand{\subtp}{\mathify{\:<:\:}}
\def\Nat{\ifmmode%
\mathchoice{\mbox{\bf num}}{\mbox{\bf num}}%
{\mbox{\scriptsize\bf num}}{\mbox{\tiny\bf num}}%
\else\mbox{\bf num}%
\fi}
\def\Void{\ifmmode%
\mathchoice{\mbox{\bf void}}{\mbox{\bf void}}%
{\mbox{\scriptsize\bf void}}{\mbox{\tiny\bf void}}%
\else\mbox{\bf void}%
\fi}
\def\Unit{\ifmmode%
\mathchoice{\mbox{\bf unit}}{\mbox{\bf unit}}%
{\mbox{\scriptsize\bf unit}}{\mbox{\tiny\bf unit}}%
\else\mbox{\bf unit}%
\fi}



%------------------Judgements-----------------------------------------

\newcommand{\jdg}[2]{#1 \triangleright #2}
\newcommand{\term}[3]{#1 \triangleright #2 : #3}
\newcommand{\eqn}[4]{#1 \triangleright #2 = #3 \mathrel{:} #4}

%-------------------Lambda calculus stuff-----------------------------

\newcommand{\lam}[2]{\mathify{\lambda #1 \Ldot\: #2}}    % lambda notation
\newcommand{\subst}[3]{\mathify{#1[#3/#2]}}             % M[N/X]
\newcommand{\mapsubst}[3]{\mathify{#1[#2\mapsto #3]}}    % M[X |-> N]
\newcommand{\twosubst}[5]{\mathify{#1[#3/#2,#5/#4]}}   % M[X:=N,Y:=P]

% Observational congruence theories
\newcommand{\Obspcf}{\equiv_{name}}
\newcommand{\Obslazy}{\equiv_{lazy}}
\newcommand{\Obsvpcf}{\equiv_{val}}
\newcommand{\Obslin}{\equiv_{lin}}
\newcommand{\Obslepcf}{\sle_{name}}
\newcommand{\Obslevpcf}{\sle_{val}}
\newcommand{\Obslelazy}{\sle_{lazy}}
\newcommand{\Obslelin}{\sle_{lin}}


% Miscellaneous lambda calculus notations
\newcommand{\meanl}{[ \! [}
\newcommand{\meanr}{] \! ]}
\newcommand{\means}[1]{\meanl #1 \meanr}
\newcommand{\aro}{\mathop\rightarrow} % see pages 154-155 of TeX manual
\newcommand{\paro}{\mathop\rightharpoonup} 
\newcommand{\karo}{\mathop\Rightarrow} % see pages 154-155 of TeX manual
\newcommand{\cross}{\mathop\times}
\newcommand{\pto}{\mathop\rightharpoonup}
\newcommand{\haltsat}{\Downarrow}
\newcommand{\diverge}[1]{#1\!\uparrow}
\newcommand{\converge}[1]{#1\!\downarrow}
\newcommand{\redex}{\leadsto}
\newcommand{\red}{\rightarrow}
\newcommand{\reds}{\aarrow}
\newcommand{\all}[2]{\Pi #1\Ldot\;#2}
\newcommand{\lift}[1]{\mathify{#1_{\bot}}}

% For call-by-value calculus
\newcommand{\eqval}[2]{\mbox{\boldmath{$\lambda_{v}$}} \vdash #1 = #2}
\newcommand{\neqval}[2]{\mbox{\boldmath{$\lambda_{v}$}} \not\vdash #1 = #2}
\newcommand{\lval}{\mbox{\boldmath{$\lambda_{v}$}}}
\newcommand{\eval}[1]{Eval_{v}(#1)}
\newcommand{\evalv}[1]{Eval_{v}(#1)}
\newcommand{\evals}[1]{Eval_{s}(#1)}
\newcommand{\obsv}[2]{#1 \equiv_{v} #2}
\newcommand{\nobsv}[2]{#1 \not\equiv_{v} #2}
\newcommand{\obsvapprox}[2]{#1 \preceq_v #2}
\newcommand{\nobsvapprox}[2]{#1 \not\preceq_v #2}
\newcommand{\vred}{\rightarrow_v}
\newcommand{\vreds}{\aarrow_{v}}
\newcommand{\haltsatv}{\Downarrow_{v}}
\newcommand{\divergev}{\Uparrow_{v}}

% For call-by-name calculus
\newcommand{\beq}[2]{\mbox{\boldmath{$\lambda$}} \vdash #1 = #2}
\newcommand{\bneq}[2]{\mbox{\boldmath{$\lambda$}} \not\vdash #1 = #2}
\newcommand{\lcalc}{\mbox{\boldmath{$\lambda$}}}
\newcommand{\obsn}[2]{#1 \equiv_{ob}^{n} #2}
\newcommand{\nred}{\rightarrow_n}
\newcommand{\nreds}{\aarrow_{n}}
\newcommand{\evaln}[1]{Eval_{n}(#1)}
\newcommand{\haltsatn}{\Downarrow_{n}}
\newcommand{\divergen}{\Uparrow_{n}}


% For call-by-name with eta rule
\newcommand{\Int}{\mathify{\iota}}
\newcommand{\leta}{\mbox{\boldmath{$\lambda \eta$}}}
\newcommand{\Eqeta}{=_{\beta\eta}}
\newcommand{\eqeta}[2]{\mbox{\boldmath{$\lambda\eta$}} \vdash #1 = #2}
\newcommand{\neqeta}[2]{\mbox{\boldmath{$\lambda\eta$}} \not\vdash #1 = #2}
\newcommand{\etared}{\rightarrow_{\beta\eta}}
\newcommand{\etareds}{\aarrow_{\beta\eta}}
\newcommand{\etanf}[1]{\beta\eta\mbox{-{\sf nf}}(#1)}

%----------------------- Per stuff --------------------------------

\newcommand{\realfn}[3]{\mathify{[#1]^{#2,#3}}}  % the function
						 % realized by a no. 
\newcommand{\Sup}[1]{\mathify{{\it sup}_{#1}}}
\newcommand{\seq}[1]{\mathify{{\it Seq}(#1)}}

%----------------------- Categories -------------------------------

\newcommand{\Op}[1]{\mathify{{#1}^{\r{op}}}}
\newcommand{\id}[1]{\i{id}_{#1}}
\newcommand{\morph}[3]{\mathify{#2 \stackrel{#1}{\aro} #3}}
\newcommand{\invmorph}[3]{\mathify{#2 \stackrel{#1}{\leftarrow} #3}}
\newcommand{\transform}{\dot{\longrightarrow}}
\newcommand{\adj}{-\!\!\!-\!|}
\newcommand{\Exp}[2]{{\b{#2}}^{\b{#1}}}
\newcommand{\ep}[1]{\mathify{{\b{#1}}^{\r{ep}}}}
\newcommand{\colim}{\lim_{\leftarrow}}
\newcommand{\Expep}[2]{{({{\b{#2}}^{\r{ep}}})}^{({{\b{#1}}^{\r{ep}}})}}
\newcommand{\dbl}[1]{{#1}^{D}}

%----------------------- Miscellany --------------------

% For notation
\newenvironment{notation}
  {\begin{trivlist}\item[\hskip\labelsep{\bf Notation:}]}{\end{trivlist}}

% For proofs
% An endproof symbol  (a little solid black box)
\newcommand{\thmbox}
   {{\ \hfill\hbox{%
      \vrule width1.0ex height1.0ex
   }\parfillskip 0pt }}
\newcommand{\qed}{\thmbox}

\newenvironment{proof}
   {\par\noindent{\bf Proof }}{\thmbox\par}
\newenvironment{proofsketch}
   {\par\noindent{\bf Proof Sketch  }}{\thmbox\par}
\newenvironment{proofof}[1]
   {\par\noindent{\bf Proof of #1  }}{\thmbox\par}

\newcounter{case}
\newenvironment{caselist}{\begin{list}{{\em Case}\/ \arabic{case}:}{\usecounter{case}}}{\end{list}}
\newenvironment{induct}{\begin{quote}}{\end{quote}}
\newcommand{\basis}{{\em Basis}:\ }
\newcommand{\induction}{{\em Induction}:\ }








\title{Effective models of polymorphism, subtyping
and recursion\\
(extended abstract)}

\author{{\it John Mitchell}~\thanks{Supported in part by NSF Grant CCR-9303099 and a grant from the TRW Foundation.}
 \quad {\it Ramesh
Viswanathan}$^*$\\[2ex]
Department of Computer Science\\
Stanford University,\ 
Stanford, CA 94305\\
{\small\tt\{mitchell, vramesh\}@cs.stanford.edu}
}

\begin{document}

\maketitle

\begin{abstract}
We develop a class of models of polymorphism,
subtyping and recursion based on a combination of
traditional recursion theory and simple domain theory.
A significant property of our primary model is that
types are coded by natural numbers using any index of
their supremum operator. This leads to a distinctive
view of polymorphic functions that has many of the
usual parametricity properties.
It also gives a distinctive but entirely 
coherent interpretation of subtyping.
An alternate construction points out some peculiarities of computability
theory based on natural number codings. Specifically,
the polymorphic fixed point is computable by a single algorithm
at all types when we construct the model over untyped call-by-value 
lambda terms, but not when we use G\"odel numbers for 
computable functions. 
This is consistent with trends away from natural
numbers in the field of abstract recursion theory.
\end{abstract}


\section{Introduction}
\label{sec:intro}

The work described in this paper began with a very simple-minded
objective. This was to develop an elementary class of semantic 
models for polymorphism, subtyping and recursion based on ideas
from recursion theory instead of domain theory. 
Our driving intuition was that the compiler for a language
such as ML compiles each expression into a bit string that
could be regarded as the G\"odel code for some function,
pair, number, or other kind of datum, as appropriate.
For each type, we therefore have a set of G\"odel
numbers representing the elements of the type.
Since semantic models are intended to provide some
basis for equational reasoning, we must also define an 
equivalence relation on the set of G\"odel codes for each type. 
Our intention was therefore to define a membership predicate and
equivalence relation, which together give us a so-called partial
equivalence relation, for each type and take the resulting quotients
of subsets of the natural numbers as the \q{domains} of our model.

A representative sample of recent studies 
using partial equivalence relations were presented
at the 1990 IEEE Logic in Computer Science Conference. 
The first of three papers describes a special class of
partial equivalence relations over the natural
numbers called \i{extensional pers} \cite{FRMS},
the second uses partial equivalence relations
over partially-ordered domains instead of
natural numbers \cite{AbadiPlotkin}, and the third works in
the constructive setting of the \i{effective topos,}
which boils down to partial equivalence relations
over the natural numbers \cite{PhoaLICS}.  
Since our goal is to develop a semantic model that can be viewed
as a quotient of the result of compilation, the use of
pers over special partially-ordered domains does not meet our objectives.
While extensional pers do give us quotients of
sets  of bit-strings, the standard and expected representations
of basic datatypes such as natural numbers and booleans,
as well as type constructors such as products, function spaces and
lifting, require modification if they are to be ``extensional'' (in
the  technical sense of extensional pers).  
Therefore, as elaborated later in the paper, this model too does not 
have the basic properties we would like.
Our work is close in spirit to \cite{PhoaLICS}, although our 
``bottom-up'' development yields a model that seems quite different 
in technical detail.  

We begin with the category \b{Per} whose objects
(interpretation of types) are partial equivalence  relations over the
natural numbers and whose maps (interpretation of terms)
are computable functions, in the usual sense of computability theory.
While this category is a well-known model of polymorphism and
subtyping, it is not useful for interpreting recursion.
This is shown by defining a per $A$ of partial functions
and a total recursive $f$ on $A$ that has no fixed point.
(In other words, the recursion theorem does not hold for arbitrary
quotients of subsets of $\s{N}$.)
The counter example is based on intuition from domain
theory: if we order $A$ in the natural way, it is not ``complete''. 
This suggests that the appropriate way to extend the recursion
theorem to subquotients is by borrowing ideas from
domain theory. In the resulting combination of recursion-theoretic
and domain-theoretic techniques, it turns out that we need far
fewer ideas from domain theory than \cite{AbadiPlotkin,MitchBruce},
for example.
(Section~\ref{sec:compare} contains a more detailed
comparison with related work.)
 
Using essentially the same ``intrinsic order'' as \cite{AbadiPlotkin,PhoaLICS},
we identify a class of ``cpo-like'' pers, each such per $R$ having
a computable function $\Sup{R}$ that gives
the least upper bound of any constructible chain in $R$.
We call these \i{effective cpo's;} although the name is
similar, these are completely different from the effectively presented
cpo's described in \cite{GunterScott}, for example.
By a generalization of the Myhill-Shepherdson theorem from
recursion theory,
all computable functions between effective cpo's are continuous.  
If an effective cpo has a least element, then
the usual domain theoretic arguments give us an effective
least fixed point operator.

Serendipitously, almost all of our basic desiderata are satisfied
by this construction.
The natural numbers (discretely ordered) and other
basic data types are easily seen to be effective cpo's.
The usual product,  function space and other constructions
preserve the property of being an effective cpo.
Moreover, the intrinsic orderings turn out to be the usual 
``pointwise orderings'' of domain theory. 
Since it is easy to use the supremum operator
to compute a least fixed point, 
the full subcategory \b{ECpo} of effective cpo's
and computable functions gives us an elementary semantics of
first-order type operators and recursion. 


In the model using G\"odel numbers of partial recursive
functions, the interpretation of higher-order types requires
that we code types as natural numbers.  
The traditional approach, when we are not concerned with
recursion,  is to make the coding relation trivial, leading to an
interpretation of polymorphic types as intersection of infinite
indexed families.
However, the intersection of a constructive family
of effective cpo's is not necessarily an
effective cpo. We therefore represent a type
by any G\"odel code of its supremum operator,
producing an interpretation of a polymorphic type $\forall t.A(t)$ 
as the collection of recursive functions
mapping any supremum operator $\Sup{R}$ to an element of the per
$A(R)$. 
Fortunately, this interpretation of polymorphism still satisfies 
the expected parametricity principles.  
For example, we can show that the per $\forall t. t$ is empty and that
the only element of the per $\forall t. t \aro t$ is the identity
function.  
We can also define a $\forall^p$ quantifier where we interpret the
domain of quantification to be pointed effective cpos.  
The difference from the $\forall$ quantifier arises because the
code for a pointed effective cpo naturally gives both its least
element and its supremum operator.
Continuing our examination of parametricity properties,  
we show that the least fixed point operator is the only fixed point
operator of type $\forall^p t. (t\aro t)\aro t$.  
Due to least elements, the
type $\forall^p t.t$ becomes nonempty and $\forall^p t. (t \aro t)$
contains more than the identity function.  
In short, the $\forall$ quantifier supports the parametricity
principles of the system \b{F} while the $\forall^p$ quantifier
supports the parametricity principles of system \b{F} extended with
fixed points.

A standard method for obtaining recursive types, described in
\cite{SmPlt}, involves showing that suitable functors on
$\b{Cpo}$-enriched categories have initial $F$-algebras.  
To obtain analogous results, we work with \b{ECpo}-enriched 
categories whose homsets each form an effective cpo.
In addition, and in a departure from applications of
the Smyth-Plotkin method we have seen before, we ask
for functors that are
effective on objects in addition to morphisms.  
This means that a functor $F$ on \b{ECpo} is \i{effective} 
if the supremum
function on $F(R)$ is uniformly computable from the supremum
function on $R$. If each homset is also pointed, we have a
\b{PECpo}-enriched category.  As for morphisms in \b{Per}, we 
can show  that any effective functor is automatically locally
continuous (in the sense of \cite{SmPlt}) and thus any effective
functor between {\em effectively complete}\/ $\b{PECpo}$-enriched
categories has an initial  $F$-algebra.  Our categories \b{ECpo} and
\b{PECpo} can be shown to be effectively complete, as well as
\b{ECpo}-enriched and \b{PECpo}-enriched, respectively.
This gives us initial $F$-algebras for all effective functors.  
All of this feels relatively routine, once we have
the idea of realizers for effective cpos; we are simply
working out effective versions of the usual arguments.

In other per models, the interpretation of subtyping has
always been the subset relation on pers, namely, 
$R$ is a subtype of $S$ iff the membership predicate and 
equality relations of $R$ are subsets of those for $S$.
Intuitively, this means that a supertype may have more elements
than a subtype, but also distinct elements of a subtype
may become identified at a supertype. 
(It is argued elsewhere that this is very intuitive and
natural.)
In our model, we cannot simply follow this approach 
since we need coherence between the supremum operators
at subtype and supertype, and between least elements
if both are pointed.
More specifically, we say an 
effective cpo $R$ is a subtype of  effective cpo $S$ if in
addition to being a subset, 
the least upper bound of any increasing chain in $R$
is also a least upper bound in $S$.
Moreover, if $R$ is  pointed then
any index of the least element of $R$ must also be one for $S$.
All the usual examples of subtyping 
hold with our modified definition of subtyping. 
We also prove a strong form of coherence, namely, if two
terms of the same type yield the same untyped term when types
are erased, then their meanings are equal.

The interpretation is extended to higher-order polymorphism
and recursion in Section~\ref{sec:model}, 
where we use the category of
doubles of \b{ECpo}-enriched categories and symmetric functors.

We started off with the intent of forming an extensional
model by taking quotients of sets of bit strings 
(or G\"odel numbers of functions).
One reason for doing this was to obtain a close correspondence
with compilation, since the denotation of an expression could be 
viewed as the equivalence class of the bit string produced by 
compiling this expression.
However, a compiler for the kind of language we are interested 
in may generate code without using type information.
A reasonable compiler could parse expressions, annotate the
parse trees during type checking, but then discard or ignore
the type annotations during code generation.
A consequence is that we expected to find a
uniform, type-independent algorithm computing the
fixed point operator at each type. 
It is one of the most surprising aspects of
our effort that we were unable to accomplish this.
Specifically, in Section~\ref{sec:unifix}, 
we use computability arguments to show that there is no uniform supremum
operator and that no untyped fixed-point operator 
can be the index of the typed fixed-point operator
at each type.
The proof uses algorithms that apply
natural number operations such as equality test to the
G\"odel codes of function arguments.
This is allowed in per structures as long as the 
resulting functional has the right extensional behavior.

In response to our difficulties with natural number
codes,  Gordon Plotkin suggested using untyped 
call-by-value lambda terms instead.
The result, described in Section~\ref{sec:cbv}, 
is a very similar category of effective cpo's,
but with a single untyped term computing all fixed-points.
This suggests that compilation is more
profitably viewed as a translation to untyped lambda terms.
While we initially regarded bit strings as the result of 
compilation, we realize upon reflection that
the result of compiling a typed program is always
a \q{typed algorithm.} In other words,
although machine language allows us to do
bit string operations on function code, for example,
no such manipulation need occur in the object code
produced by compiling a typed program. 
Since natural numbers are distinct from function expressions
in the untyped call-by-value calculus, there is just enough
of an inherent type distinction to provide a uniform
fixed-point algorithm.
While this may be a slight surprise to computer scientists,
our eventual preference for call-by-value terms
appears consistent with the move away from
natural number coding in the field of recursion theory
(e.g., \cite{BarwiseAdmis}).


\section{Preliminaries}
\label{sec:prelim}

Let $\varphi_0, \varphi_1,\ldots$ be any enumeration of the partial
recursive functions.  We use $n \cdot m$ to denote $\varphi_n(m)$.
We use $\Pair$ for a computable pairing function on the natural
numbers and $(n)_1$ and
$(n)_2$ to denote the first and second projections of $n$.  
Let ${\cal N}$ denote the set of natural numbers.  A partial
equivalence relation (per) $R \subseteq {\cal N}\cross {\cal N}$ is 
a
symmetric transitive relation.  For any per $R$, $n:R$ 
denotes that $n\:R\: n$; for any $n:R$, $[n]_R$ denotes
the equivalence class $\set{m\ |\ n\: R\: m}$ and the set represented
by 
$R$ is 
defined to be $[R] = \set{[n]_R\ |\ n R n}$.  
We say that a natural number $n$ realizes an
element $a \in [R]$, $n\vdash_R a$, if $n \in a$.  A function $f$
(set-theoretic) from $[R]$ to $[S]$ is realized by a natural number
$n$, denoted by $n \vdash_{R,S} f$ if for all $a \in [R]$, $m \vdash_R
a$ we have that $n\cdot m 
\vdash_S f(a)$ and we call a function $f:[R]\aro [S]$ effective or
computable if 
it has a realizer.  We often omit the subscripts $R,S$ from
$n\vdash_{R,S} f$ when they are clear from the context.  We use
$\realfn{n}{R}{S}$ to denote the unique 
map from $[R]$ to $[S]$ that $n$ realizes, if it realizes one.  The
category $\b{Per}$ has as objects pers, and 
as morphisms from $R$ to $S$ the effective maps from $[R]$ to
$[S]$.  
For any set $B\subseteq {\cal N}$, we define the per $D_B =
\set{\tuple{n,n}\ |\ n \in B}$, the identity relation on $B$.
We use $N$ to denote the per $D_{\cal N}$ and $\unit$ to denote the
per $D_{\set{0}}$.  
If $R,S$ are pers, we define the pers $R\cross S, R\aro S, R\paro S$ by 
$n\: R\cross S\: m \mbox{ iff } (n)_1\:R\:(m)_1 \mbox{ and }
(n)_2\:S\:(m)_2, 
n\: R\aro S\: m  \mbox{ iff } \forall x,y\in {\cal N}.\ x\:R\:y \
\imp\ (n\cdot x)\: S\: (m\cdot y), 
n\: R\paro S\: m \mbox{ iff } \forall x,y\in {\cal N}.\
x\:R\:y \
\imp\ \converge{(n\cdot x)}\ \imp\ (n\cdot x)\: S\: (m\cdot y) 
$
where we use $(n\cdot x)\: S\: (m\cdot y)$ to mean that
$\converge{(n\cdot x)}$ and $\converge{(m\cdot y)}$ and they are
related in $S$.  We can define the lifting of a per $R$ as $\lift{R} =
\unit \paro R$.

Let $A$ be any set and $\vdash_A \subseteq {\cal N}\cross A$ be a
binary relation which we often call a realization relation.  
Recall
that $\vdash_A$ is {\em onto}\/ if for all $a\in A$, there is an $n$ with
$n\vdash_A a$ and a {\em function}\/ if whenever $n\vdash_A a, n
\vdash_A b$ we have that $a=b$.  Every onto function
$\vdash_A$ on a set $A$ gives rise to a per, namely,
$\set{\tuple{n,m}\ |\ n, m \vdash_A a,\ a\in A}$.  Suppose $\vdash_A$
is some fixed onto realization relation on a set $A$ and $\vdash_B$ is
another fixed onto realization relation on a set $B$.  We call a 
function (set-theoretic) $f:A\aro B$ {\em effective}\/ if 
there is an $n$ such that for all $a\in A, m \vdash_A a$ we have that
$n\cdot m \vdash_B f(a)$; we take $n$ to be the realizer of $f$.  We
also say that $f(a)$ is {\em effectively 
realizable}\/ from $a$ to mean that the function $f$ is effective.

\section{Fixed Points and Effective Cpos}
\label{sec:fix-point}

We begin by showing that the full category $\b{Per}$ is not suitable
for interpreting fixed points.  
\begin{example}[Failure of Fixed Points]
\label{ex:fail-fix}
Take $R$ to be the per $\unit$ and $S$ to be the per of partial
functions that are 
defined exactly on some finite prefix of the natural numbers.  
More formally, $S$ is defined by
$m\:S\:n$ iff \mbox{$\exists u \in {\cal N}\; \forall x < u\ ( m\cdot
x = n\cdot 
x )$} and \mbox{$
\forall x \geq u\ (\diverge{m\cdot x} \mbox{
and } \diverge{n\cdot x})$}.
Let $F$
be an index of the function, which on input $f:(R\paro S)$, returns an
index of 
the function, which on input $0:\unit$ returns an index of the
function which on input $n$ computes $g = f\cdot 0$ and returns $0$ if
$n=0$ and returns $g\cdot (n-1)$ otherwise.  It can be verified that
$F:(R\paro S)\aro (R\paro S)$ and that $\realfn{F}{(R\paro S)}{(R\paro
S)}$ has no fixed point.
\end{example}

An important idea in the above example is that if
we order the partial functions that are the elements of the per $S$ 
by the pointwise ordering, as we would in domain theory,
then $S$ is not a cpo.  Therefore, it seems natural to circumvent the
problem illustrated by the per $S$ by selecting a class of cpo-like
pers.  The first step is to associate an order with each per.
To define an ordering on the elements of a per $R$, we focus attention
on effective partial functions from $R$ to $\unit$.  Since, $\unit$
is a one-element per, the only significant behaviour of any $f:R \paro
\unit$ on an $x:R$ is its convergence.  We can thus think of $f:R
\paro \unit$ as a partial decision algorithm computing with
$R$-inputs or a {\em computable test}\/ on $R$, with convergence
announcing success.  We then 
consider an $x:R$ to be distinguishable from $y:R$ if there is a
computable test converging on $x$ and diverging on $y$.  Thus, an
$x:R$ has computationally no more information than
$y:R$ if $x$ is not computationally distinguishable from $y$.
Thus, for any per $R$ and $x,y:R$, we define
\[
x \leq_R y \;\mbox{ iff }\; \forall f:R\pto \unit.\; \converge{f\cdot x}
\mbox{ implies } \converge{f \cdot y}
\]
For $[x]_R, [y]_R \in [R]$, we define $[x]_R \leq_{[R]} [y]_R$ iff $x
\leq_R y$; $\leq_{[R]}$ is easily seen to be a preorder.

Taking this to be our {\em intrinsic ordering}\/, we consider the class
of 
pers whose intrinsic orderings are complete partial orders in the
internal language of the topos \b{Per}.  For any per $R$, define the
per $\seq{R}$ of {\em effective 
increasing sequences} as the largest subset of the per $N\aro R$ such
that $s:\seq{R}$
iff for all $n \in {\cal N}$, $s\cdot n \leq_R s\cdot (n+1)$.
We call a function (possibly partial) from $[{\it Seq}(R)]$ to $[R]$ a
{\em supremum}\/ function if it maps an element $[s]$ of $[{\it
Seq}(R)]$ to a least upper bound of $\set{[s\cdot n]_R\ |\ n \in {\cal
N}}$ with respect to the preorder $\leq_{[R]}$ if it exists and 
undefined otherwise.  If the preorder $\leq_{[R]}$ on $[R]$ is
antisymmetric, then there is a unique supremum function; in this case,
we denote it by ${\it sup}_R$.
We define a per $R$ to be an {\em effective cpo}\/ if
\begin{description}
\setlength{\itemsep}{0.25ex}
\item[Antisymmetry] 
For $a,b\in [R]$, if $a \leq_{[R]} b$ and $b \leq_{[R]} a$ then $a = b$.
\item[Computable Completeness]  
The supremum function ${\it sup}_R : [{\it Seq}(R)] \aro [R]$ is a
morphism in $\b{Per}$, \ie, it is {\em total}\/ and {\em effective}.
\end{description}

\begin{lemma}[Continuity]
\label{lem:fun-cont}
Suppose that $R,S$ are effective cpos.  Then any effective $f:[R]\aro
[S]$ is continuous, i.e., if $s:\seq{R}$ then
$f(\Sup{R}([s]_{\seq{R}})) = 
\Sup{S}(f\compose \realfn{s}{N}{R})$.  
\end{lemma}
By analogy with ordinary cpos, we say that an effective cpo $R$ is 
{\em pointed}\/ if $[R]$ contains a least element with respect to the 
intrinsic order $\leq_{[R]}$; we denote its least
equivalence class by $\bot_R$.  

\begin{lemma}[Fixed Points]
\label{lem:fix-point}
Suppose that $R$ is a pointed effective cpo.  Every effective $f:[R]\aro
[R]$ has a least fixed point with respect to the ordering $\leq_{[R]}$. 
The function ${\it fix}_R: [R\aro R] \aro [R]$ mapping
realizers for morphisms to their least fixed point is effective and 
is effectively 
realizable from $\Sup{R}$ and $\bot_R$.  
\end{lemma}

While our assumptions on the properties of an effective cpos were
important to our proof of the existence of a computable fixed point
operator, we can also show that they are the weakest
conditions possible.  
We can construct a per $R$ whose intrinsic order is not antisymmetric,
and 
a per $S$ whose intrinsic order is antisymmetric and for which
$\Sup{S}$ is total but not effective; 
both $R$ and $S$ can be 
shown not to admit any effective fixed point operator.  It can also
be seen that a per that is not pointed cannot admit a fixed point
operator.  


The basic constructions on pers all yield effective
cpos.  For any $B \subseteq {\cal N}$, the intrinsic order on the
per $D_B$ 
is easily seen to be discrete and hence an effective cpo trivially and it
is pointed iff $|B|=1$; we now state the closure under the other
constructions.

\begin{prop}[Product Spaces]
\label{prop:prod-eff}
If $R,S$ are pers then $x \leq_{R\cross S} y$ iff $\fst{x} \leq_R
\fst{y}$ and $\snd{x}\leq_S \snd{y}$.  Thus, if $R$ and $S$ are
effective cpos then $R \cross S$ is an effective cpo, with
$\Sup{R\cross S}$ effectively realizable from $\Sup{R}$ and $\Sup{S}$.
If $R,S$ 
are pointed then $R
\cross S$ is pointed with $\bot_{R\cross S}$
effectively realizable from $\bot_R, \bot_S$.
\end{prop}
\begin{prop}[Total Function Spaces]
\label{prop:total-eff}
If $R,S$ are pers and $S$ is an effective cpo, then $f \leq_{R\aro
S} g$ iff $\forall x:A. f\cdot x \leq_S g\cdot x$.
Thus, if $R$ and $S$ are
effective cpos then $R \aro S$ is an effective cpo, with
$\Sup{R\aro S}$ effectively realizable from $\Sup{S}$.  If $S$ is
pointed then 
$R\aro S$ is pointed with $\bot_{R\aro S}$ effectively realizable from
$\bot_S$. 
\end{prop}
\begin{prop}[Partial Function Spaces]
\label{prop:partial-eff}
If $R,S$ are pers and $S$ is an effective cpo, then $f \leq_{R\paro
S} g$ iff $\forall x:A. \converge{f\cdot x} \imp f\cdot x \leq_S
g\cdot x$ 
Thus, if $R$ and $S$ are
effective cpos then $R \paro S$ is an effective cpo, with
$\Sup{R\paro S}$ computable from $\Sup{S}$.  The per $R\paro S$ is
always pointed with $\bot_{R\paro S}$ realized by the index of the
function ``$\lambda x \in {\cal N}. \mbox{diverge}$'' independent of
$R,S$. 
\end{prop}

While the proof of the ``pointwise'' 
intrinsic ordering for products is standard (\cf \cite{AbadiPlotkin})
and is true for arbitrary pers,
the intrinsic ordering for the pers $R\aro S, R\paro S$ is pointwise
only when the per $S$ is an effective cpo.  
An important point to note about the closure of effective cpos under
these operations, as given by the above propositions, is that it is
constructive, \ie, the supremum 
operator for the product or function space pers of $R,S$  can be
computed from the supremum operator for $R$ and $S$.  
Since lifting is defined
using partial 
functions, it follows that effective cpos are closed under lifting as
well. 

\section{Polymorphism}
\label{sec:poly}

Let $\r{ECpo}$ and $\r{PECpo}$ be the set of all effective cpos and
pointed effective cpos respectively.  
Define an {\em effective set}\/ to be a set $K$ equipped with an {\em
onto}\/
binary relation $\vdash_{K} \subseteq {\cal N}\cross K$.  For any
function ${\cal C}:K \aro \r{ECpo}$, we can define the per
$\forall^K({\cal C})$ as follows:
\[
f\; \forall^K({\cal C})\; g\ \ \mbox{ iff }\ \ \forall a \in K, x,y
\in {\cal N}\ \ x,y \vdash_K a \imp (f \cdot x)\; {\cal 
C}(a)\; (g \cdot y)
\]
It is easy to see that $\forall^K({\cal C})$ is symmetric and
transitive, \ie, that it is a per.  
We take $\r{ECpo}$ to be an effective set with $n \vdash_{\r{ECpo}} R$
iff $n \vdash_{\seq{R},R} \Sup{R}$.  And, we consider $\r{PECpo}$ an
effective set with $n \vdash_{\r{PECpo}} R$ iff $\fst{n}
\vdash_{\r{ECpo}} R$ and $\snd{n} \vdash_R \bot_R$.  Essentially the
realizers for $\r{ECpo}$ and $\r{PECpo}$ are proofs, in the internal
language of the effective topos, of the membership of a per in the
particular subset.
The following
lemma shows that if ${\cal C}$ is
an effective map (as defined in Section \ref{sec:prelim}) from $K$ to
$\r{ECpo}$ then 
$\forall^K({\cal C})$ is an effective cpo.  As usual, we also give the
conditions under which it is pointed. 

\begin{lemma}[Higher-Order Polymorphism]
\label{lem:univ-eff}
Let ${\cal C}:K\aro \r{ECpo}$ be an effective map.  Then \\
$f \leq_{\forall^K({\cal C})} g$ iff $\forall a \in K,
x \in {\cal N}\ \ x \vdash_K a \imp (f \cdot x)
\leq_{{\cal C}(a)} (g \cdot x)
$.
Thus, 
$\forall^K({\cal C})$ is an effective cpo with $\Sup{\forall^K({\cal C})}$
effectively realizable from ${\cal C}$.  If ${\cal C}$ induces an
effective map 
from $K$ to $\r{PECpo}$ then
$\forall^K({\cal C})$ is pointed with 
$\bot_{\forall^K({\cal C})}$ effectively realizable from the effective
map ${\cal C}:K \aro \r{PECpo}$.  
\end{lemma}
As particular instances of Lemma \ref{lem:univ-eff}, we can define
constructors $\forall^{\r{ECpo}}$ which we denote
$\forall$, and $\forall^{\r{PECpo}}$ which we denote $\forall^p$,
yielding effective cpos.
The following proposition shows that in this semantics of
polymorphism as well, the type $\forall t.t$ is empty and $\forall
t.(t\aro t)$ only contains the identity function.  It thus suggests
that all the usual parametricity principles are validated even by this
interpretation of polymorphism that is 
less ``uniform'' than intersection.  Essentially, parametricity in our
context arises from the fact that the realization relations
$\vdash_{\r{ECpo}}, \vdash_{\r{PECpo}}$ are {\em not functions}\/  ---
thus, any element of the polymorphic per must
behave uniformly on all pers that admit common realizers for their
supremum functions.

\begin{prop}[Parametricity]
\label{prop:parametricity}
For $\s{I}:ECpo\aro ECpo$ defined by $\s{I}(R) = R$, there is no $n$
with $n:\forall({\cal I})$.  For $\s{F}:ECpo\aro ECpo$ defined by
$\s{F}(R) = R\aro R$, if $n:\forall(\s{F})$ then for any effective cpo
$R$, 
natural number $x$, if $x \vdash \Sup{R}$ then $n\cdot x \vdash_R
\id{R}$.  
\end{prop}

Turning next to the $\forall^p$ quantifier, 
consider the map ${\cal C}:\r{PECpo} 
\aro \r{ECpo}$ given by ${\cal C}(R) = (R\aro R)\aro R$ which is
effective by Proposition \ref{prop:total-eff}. 
By Lemma \ref{lem:fix-point} we have a realizer ${\it fix}:
\forall^p({\cal 
C})$, which computes the least fixed point at every pointed type.  The
following 
proposition shows that this is the {\em only}\/ fixed
point operator of this polymorphic type:
\begin{prop}[Polymorphic Fixed Point]
\label{prop:least-fix-only-fix}
Consider the effective map ${\cal C}:\r{PECpo}\aro \r{ECpo}$ given by
${\cal C}(R) = (R\aro R)\aro R$.  Then we have a realizer ${\it
fix}:\forall^p({\cal C})$ computing the least fixed point at every
pointed type.  Further, suppose that we have an
$f:\forall^p({\cal C})$ such that for any pointed effective cpo $R$,
and $x \vdash \Sup{R}, b \vdash \bot_R$ we have that $(f \cdot
\pair{x,b}) = n$ such that for any $g:R\aro R$, $n\cdot g\; R\; g\cdot
(n\cdot g)$, \ie, $f$ is a fixed point operator.  Then $f\;
\forall^p({\cal C})\; {\it fix}$. 
\end{prop}
Just like Proposition \ref{prop:parametricity}, we can prove that
the type $\forall^p t. t$ has exactly one element and the type
$\forall^p t. (t\aro t)$ has exactly two elements; the polymorphic
operator $\forall^p$ thus supports the parametricity principles of
system \b{F} extended with recursion on values.

\section{Recursive Types}

A standard method for obtaining recursive types is that given by 
\cite{SmPlt} which shows that suitable functors on $\b{Cpo}$-enriched
categories admit recursive solutions.  While these results are not 
directly applicable to the category of effective cpos, we obtain
analogous results by 
considering everything ``effectively'' and reformulating the framework
and 
results of \cite{SmPlt} for a suitable notion of effectivity.  The
main departure from earlier work in this regard (\eg,
\cite{AbadiPlotkin}) is that effectiveness of a functor is a condition
on its behaviour on objects in addition to arrows.


Let $\b{C}$ be a category.  We call it {\em effective}\/ if it is
equipped 
with a realization relation, $\vdash_{\b{C}}$, on objects and
morphisms that is {\em onto on objects}\/ and an {\em onto function on
each homset}, with identity morphisms effectively realizable from the
objects and composition effective; define effective functors
between effective categories in the obvious way.  By the condition on 
$\vdash_{\b{C}}$, 
we can define a per
corresponding to each homset as in Section
\ref{sec:prelim}. We say that \b{C} is an 
\b{ECpo}-enriched category if the per corresponding to each homset
$\b{C}(A,B)$ is an effective cpo with its supremum function 
effectively realizable from the objects $A,B$; this is of course just
the internal proof 
that every 
homset is a cpo.  
Define the category $\ep{C}$ whose 
objects are those of \b{C} and whose morphisms are embedding-projection
pairs (while the embeddings and projections determine each other
uniquely, they may not necessarily do so effectively; it therefore
does not suffice to consider the subcategory of only embeddings or
projections).  As for morphisms in \b{Per}, any effective functor
between two 
\b{Ecpo}-enriched categories is automatically 
locally continuous in
the sense of \cite{SmPlt}.  Call
an 
effective category \b{C} a 
\b{PECpo}-enriched category if it is an \b{ECpo}-enriched category and the
per corresponding to each homset $\b{C}(A,B)$ is pointed with its least
element effectively realizable from the objects
$A,B$.  

\begin{lemma}[Recursive Solutions]
\label{lem:rec-object}
Suppose that $\b{C}$ is an effectively $\Op{\bm{\omega}}$-complete,
\b{PECpo}-enriched category with a terminal object $\bot$ and 
such 
that composition in $\b{C}$ is left-strict, \ie, for any
$\morph{f}{A}{B}$ we have $\bot_{B,C} \circ f = \bot_{A,C}$.  Then
for any  
effective functor $F:\ep{C} \aro \ep{C}$, we have an 
object $\mu(F)$ in \b{C} and morphisms ${\it fold}^F:F(\mu(F))\aro
\mu(F), {\it unfold}^F:\mu(F)\aro F(\mu(F))$ with ${\it fold}^F, {\it
unfold}^F$ constituting an isomorphism pair in \b{C}.  Moreover, 
the object 
$\mu(F)$ and the morphisms ${\it fold}^F, {\it unfold}^F$ are 
effectively realizable from the effective functor $F$.
\end{lemma}



Define \b{ECpo} to be
the full subcategory of \b{Per}, of the effective cpos.  The
realization relation on objects of $\b{ECpo}$ is as in Section
\ref{sec:poly} for \r{ECpo} and on morphisms as in Section
\ref{sec:prelim}.  Take $\b{PECpo}$ to be the full
subcategory of \b{ECpo} of pointed effective cpos with the realization
relation on objects as in Section \ref{sec:poly} for \r{PECpo}.
\begin{lemma}
\label{lem:ecpo-complete}
The categories \b{ECPo} and \b{PECpo} are effectively
$\Op{\bm{\omega}}$-complete.   
\end{lemma}
By Proposition \ref{prop:total-eff}, \b{ECpo} is
an \b{ECpo}-enriched category and $\b{PECpo}$ is a \b{PECpo}-enriched
category; it can also be seen that $\b{PECpo}$ satisfies the other
conditions of Lemma \ref{lem:rec-object}.  Hence, any effective
functor $F:\ep{ECpo}\aro \ep{ECpo}$ that induces an effective functor
from $\ep{PECpo}$ to $\ep{PECpo}$ has a recursive solution.  This
condition on the preservation of pointedness is not an accident of our
method of constructing recursive solutions; there are 
functors that do not map pointed pers to pointed pers and provably
cannot have any recursive solutions.

\section{Subtyping}
\label{sec:subtyping}

Suppose we have pers $R,S$ with $R \subseteq S$ as relations.  Since
the index of $\lam{x\in {\cal N}}{x}$ realizes an effective map from
$R$ to $S$, we have by Lemma
\ref{lem:fun-cont}, that if $x \leq_R y$ then $x \leq_S y$.  Thus, if $R
\subseteq S$, then $\seq{R} \subseteq \seq{S}$.  
For effective cpos $R,S$, we define that $R$ is a subtype of $S$,
denoted $R \subtp S$, iff  
$R \subseteq S$,
if $n \vdash
\Sup{R}$ and $s:\seq{R}$ then $n \cdot s \vdash \Sup{S}(s)$,
\comment{
for any $n:\seq{R}$, $\Sup{R}([n]_{\seq{R}}) \subseteq
\Sup{S}([n]_{\seq{S}})$,
} and
if $R$ is pointed and $n \vdash_R \bot_R$ then $S$ is pointed with $n
\vdash_S \bot_S$.
Essentially then, $R$ is a subtype of $S$, if the
proof of any
``interesting property'' in $R$ is also a proof in $S$; the interesting
properties in our context being membership in a per, equality in a per,
and membership in the subcategories \b{ECpo}, \b{PECpo}.  
This notion of subtyping is reflexive and transitive and one obtains
all the usual subtyping relations between the various type
constructors.  We can define the per ${\it Top} = {\cal N}\cross
{\cal N}$ as the supertype of all types.  


\section{A Model of $F\omega$ with recursion and subtyping} 
\label{sec:model}

We can present our semantics as a categorical version of \cite{BMM}
with 
additional structure for the distinction between types and pointed
types, fixed points at pointed types, higher-order polymorphism and
recursive solutions for
maps from pointed kinds to pointed kinds.  At a first 
approximation, 
we can take the category for kinds to be the category of all
\b{ECpo}-enriched categories and effective functors, and take the
categories \b{ECpo} and \b{PECpo} to interpret types and pointed types
respectively.  The 
problem with this is that type operators such as $\aro$ cannot be
expressed as covariant functors and are thus not morphisms of this
category. 
Inspired by \cite{AbadiPlotkin}, we
consider doubles of categories and symmetric functors;
our main technical contribution is that we exhibit 
a 
cartesian 
closed structure, which allows us to give a categorical semantics of 
$\b{F\omega}$ and recursive kinds.

Let ${\cal K}$ be the category whose objects are $\dbl{\b{C}}$ for
$\b{C}$ an effectively $\Op{\bm{\omega}}$-complete, \b{ECpo}-enriched
category
with terminal object and left-strict composition (which categories we
henceforth abbreviate as ``good'' categories), and whose morphisms
are effective symmetric functors.   We can define the product of
$\dbl{\b{C}}, \dbl{\b{D}}$ itself as the double of another ``good''
category and similarly for exponentials; this establishes ${\cal K}$
to be cartesian-closed.  
We take types to be the object $\dbl{\b{ECpo}}$ and pointed types to
be $\dbl{\b{PECpo}}$.  
By extending the definitions of all
the 
semantic constructions  
given in earlier sections on objects to  
morphisms in the standard way, we can define them as symmetric
effective functors into $\dbl{\b{ECpo}}$ as well as $\dbl{\b{PECpo}}$
describing their behaviour as type constructors as well as pointed
type constructors.

We interpret terms as effective natural transformations 
between 
appropriate 
functors (essentially, dropping the ``double'' on their domain and
range).
The  
term constructors arise from the adjunctions expressing the cartesian
closure of 
\b{ECpo}, the natural transformations asserting that the functor
$\lift{(\cdot)}$ is a monad, the natural isomorphism between $R\paro S$ 
and $R\aro \lift{S}$, and $\forall^{\b{C}}$ as a right adjoint to the
diagonal functor.
Finally, by Lemma \ref{lem:fix-point} the morphism ${\it
fix}^R$ is effectively realizable from $R$ and by Lemma
\ref{lem:rec-object} 
the 
morphisms
${\it fold}^F, {\it unfold}^F$ are effectively realizable from $F$; we
can also prove that 
they are 
natural in $R$ and $F$ respectively which gives their
interpretations as effective natural 
transformations.  
It turns out that except for the fixed
point operator and the isomorphism pair between a recursive kind and
its unfolding, every other term constructor arises from a {\em
uniform}\/ natural transformation.  

We define the subtyping relation for objects of $\b{ECpo}$ as in
Section \ref{sec:subtyping}.  Usually, coherence of a semantics (in
the presence of subtyping) means 
that the meaning of a term 
does not depend on its typing derivation.  Inspite of a fixed
point operator whose interpretation depends on the type, we can prove
a 
stronger form of coherence for our semantics.  Informally, we can show
that if for two 
terms $M,N$ of 
type $\sigma$ their erasures are the same then $\means{M:\sigma} =
\means{N:\sigma}$, \ie, their meanings are the same at type $\sigma$.
We show this property for fixed points and the
isomorphism pair between a recursive type and its unfolding;
since the interpretation of all other
term constructors arises from uniform natural transformations,  our
coherence theorem 
asserting the equality of the meaning of two terms with the same
erasure at a particular type follows.

\section{Uniform Fixed Point Realizer}
\label{sec:unifix}
We first investigate the existence of a uniform realizer for all
supremum functions.  The following lemma shows that this is impossible
even for 
$\lift{N}, \lift{(N\paro N)}$.  
\begin{lemma}[Failure of Uniform Suprema]
\label{lem:fail-sup}
There is no natural number $f$ such that $f \vdash \Sup{N}$ and $f
\vdash \Sup{N\paro N}$, \ie, such that if $s:\seq{N}$ then
$f \cdot s \vdash_N \Sup{N}(s)$ and if $s:\seq{N\paro N}$ then $f
\cdot s  
\vdash_{N\paro N} \Sup{N\paro N}(s)$.
\end{lemma}
\begin{corollary}
\label{cor:fail-sup}
There is no natural number $f$ such that $f \vdash \Sup{\lift{N}}$ and
$f \vdash \Sup{\lift{(N \paro N)}}$.
\end{corollary}
Next, we focus on uniformly computing fixed points of
$f:(R\paro S)\aro 
(R\paro S)$ for effective cpos $R,S$. 
A natural candidate for a uniform fixed point operator is the index,
$Y$, of the untyped call-by-value fixed point operator (also given by
the first recursion theorem
\eg, see \cite{Cutland}).
Of course, untyped lambda calculus abounds with other fixed point
operators 
(\cf \cite{Bar}); the following definition captures the essential
property of any untyped fixed point operator.
\begin{definition}
\label{def:untyped-fix}
A natural number $f$ is an {\em untyped fixed point operator}\/ if for
any $n:N\aro N$ we have 
$f \cdot n \; (N\paro N)\; n\cdot (f\cdot n)$.  
\end{definition}
\begin{lemma}[Failure of Untyped Fixed Points]
\label{lem:fail-Y}
Consider any untyped fixed point operator $f$.
Suppose that $R,S$ are pers with $\neg (k (R\paro S) k)$, for some
$k\in {\cal N}$.  Then there
is an $e:(R\paro S)\aro (R\paro S)$ with $\neg (f \cdot e (R\paro S)
f \cdot e)$.  Thus, $f$ does not even realize a morphism from
$((R\paro S)\aro (R\paro 
S))$ to $(R\paro S)$ and hence cannot realize a fixed point operator for
the per $R\paro S$. 
\end{lemma}
In particular, the index $Y$ cannot be a
realizer for the fixed point operator on all $R\paro S$.  
The definition of $e$, in the proof of Lemma \ref{lem:fail-Y},
uses an equality test on its argument $y$
which essentially depends on the fact that realizers for
functions ($y:R\paro S$ in this case) are accessible as realizers of
natural 
numbers and thus 
susceptible to equality tests.  In Section
\ref{sec:cbv} we show that this is the only reason for the
failure of $Y$ as a fixed point operator.


\section{Effective Cpos over Lambda Terms}
\label{sec:cbv}

We consider an untyped call-by-value $\lambda$-calculus that has term
constants corresponding to numerals and some basic 
operations on natural numbers.  It thus
corresponds closely to the ``turing machine'' application operation on
G\"odel numbers, 
except for 
introducing a distinction 
between codes of natural numbers (numerals) and codes of functions
($\lambda$-abstractions).  We take the partial combinatory algebra
whose 
elements are observational congruence classes of the terms of the
calculus 
and consider effective cpos over them.  We inherit all the
results from previous 
sections on effective cpos over natural numbers, since their proofs
only use 
computability arguments, and all computable
functions are expressible in this calculus.

We can show that the untyped term $Y =
\lam{f}{(\lam{x}{f\:(\lam{z}{x x z})})\:(\lam{x}{f\:(\lam{z}{x x
z})})}$ 
is a realizer for the least fixed point operator ${\it fix}^{R\paro
S}$ for any effective cpos $R,S$, using 
the observational preorder $\sle$ on terms.  The partial combinatory
algebra, equipped with this ordering, is not a cpo; however, 
if $a_n, n
\in {\cal N}$ are 
such that $a_n \sle a_{n+1}$, 
we  
denote its least upperbound by  $\Lub_n a_n$ when it exists. 
For any effective cpo $R$, we can prove the remarkable property that 
if $s:\seq{R}$ is an
increasing  
sequence such that $s\cdot n \sle s\cdot
(n+1)$ then $\Lub_n (s\cdot n) \vdash_R \Sup{R}(s)$, \ie, 
if an
increasing sequence is also an increasing sequence with respect to 
$\sle$ then its supremum in 
the effective cpo must be the equivalence class of the least upper 
bound with respect to the global ordering.  Now, consider the
elements $F_n$ defined by $F_0 = 
\lam{f}{\Omega}$, where $\Omega$ is any divergent term and $F_{n+1} =
\lam{f}{ f\;(\lam{z}{F_n\;f\; z})}$.  Because of the distinction
between numerals and $\lambda$-abstractions, $F_n
\sle 
F_{n+1}$ and $Y = \Lub_n F_n$.  We also have that
$F_n:((R\paro  
S)\aro (R\paro S))\aro (R\paro S)$ and that ${\it fix}^{R\paro S} =
\Sup{((R\paro S)\aro (R\paro S))\aro (R\paro S)}(s)$ where $s$ is the
sequence with $s\cdot n = F_n$.  From all this it follows that $Y
\vdash {\it fix}^{R\paro S}$.  

\section{Comparison with related work}
\label{sec:compare}
From domain theory, we have several classes of domain
models of polymorphism and recursion. The first are
the universal domains. A general construction explored
in \cite{AmBrLongo86} interprets types as the finitary projections
over a universal domain. Since types are domains,
recursion is straightforward. An alternative model
in essentially the same spirit uses the closures of $P\omega$
\cite{Scott76,McCracken,BMM}.
Two models that are not based on universal domains
are the coherent spaces of Girard \cite{Girard86}
and the related use of $dI$-domains
developed in \cite{CGW89}.
In each of these cases, we would interpret subtyping 
by selecting a class of continuous ``subtype maps.''
However, since there is no general characterization
of subtyping, this would have to be done on an
\i{ad hoc} basis for each model. An example study
identifying the linear maps between $dI$-domains
as candidate subtype maps is \cite{BreazuCGS91}.

The alternatives to these domain models all use
partial equivalence relations. The per models
fall into two groups, one using pers over domains
and the other pers over the natural numbers.
Some constructions in the first group are
explained in \cite{AbadiPlotkin,Amadio,Cardone,MitchBruce}.
The most sophisticated construction is \cite{AbadiPlotkin},
which uses an intrinsic order similar to the present paper, but
in addition to being a cpo, the pers need to 
satisfy other conditions (\eg, uniformity).
In as much as 
the model presented in Section \ref{sec:cbv} works with only the
simple conditions of being an effective cpo and is a semantics of
polymorphism and recursion with uniform fixed points, 
these additional
conditions on pers seem to be a direct consequence of working
over specially constructed domains.

There are two previous models using pers over the
natural numbers. The more accessible is the 
class of extensional pers \cite{FRMS}.
Unfortunately, the property of being an extensional per is not 
categorical as evidenced by the fact that the class of extensional
pers is not closed under recursive isomorphism.
More importantly from our point of view, 
the natural interpretations of basic datatypes such as
natural numbers and booleans also fail to be 
extensional (in the technical sense of ``extensional pers'').
The extensional pers are also not closed under the natural 
constructions of products, total function spaces and 
partial function spaces.  
Hence one uses variants of these operations that work but 
seem to have no natural explanation.
In short, although the development of extensional pers is
mathematically elegant and rich, these pers do not support
our motivating intuition for preferring per models
over the natural numbers.  

The final class of models involve the development of
domains within the effective topos \cite{Hyland82,Hyland87}.
The main idea, as explained briefly in \cite{PhoaLICS}
and elaborated in \cite{PhoaThesis,Hyland92,HylandRR90}
is to carry out the usual development of
domain theory within a constructive set theory that may
be interpreted over pers.
This leads to a class of domain-like pers that
are essentially the same as our effective cpos.
However, the class of maps, interpretation of
lifting, and fixed-point operators 
are technically different from ours.
In particular, it does not seem that polymorphism
is interpreted by considering supremum operators
as the realizers of domains.  
There is also a model over untyped 
call-by-name lambda-terms in \cite{PhoaThesis}, using
pers that have an order property defined using a specific
per $\omega$ and its completion $\bar{\omega}$.
The main difference is that our definition of effective cpo,
which implies Phoa's condition on relations, 
makes sense for any partial combinatory algebra, while
Phoa's condition appears specific to  lambda terms.

{\small
\bibliographystyle{alpha}
\bibliography{/u/ftp/pub/jcm/bib}
}

\end{document}
