\documentclass[12pt,titlepage]{article} \usepackage{amsmath} \usepackage{mathrsfs} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} \usepackage{mathtools} \usepackage{graphicx} \usepackage{color} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage{xparse} \usepackage{hyperref} %----Macros---------- % % Unresolved issues: % % \righttoleftarrow % \lefttorightarrow % % \color{} with HTML colorspec % \bgcolor % \array with options (without options, it's equivalent to the matrix environment) % Of the standard HTML named colors, white, black, red, green, blue and yellow % are predefined in the color package. Here are the rest. \definecolor{aqua}{rgb}{0, 1.0, 1.0} \definecolor{fuschia}{rgb}{1.0, 0, 1.0} \definecolor{gray}{rgb}{0.502, 0.502, 0.502} \definecolor{lime}{rgb}{0, 1.0, 0} \definecolor{maroon}{rgb}{0.502, 0, 0} \definecolor{navy}{rgb}{0, 0, 0.502} \definecolor{olive}{rgb}{0.502, 0.502, 0} \definecolor{purple}{rgb}{0.502, 0, 0.502} \definecolor{silver}{rgb}{0.753, 0.753, 0.753} \definecolor{teal}{rgb}{0, 0.502, 0.502} % Because of conflicts, \space and \mathop are converted to % \itexspace and \operatorname during preprocessing. % itex: \space{ht}{dp}{wd} % % Height and baseline depth measurements are in units of tenths of an ex while % the width is measured in tenths of an em. \makeatletter \newdimen\itex@wd% \newdimen\itex@dp% \newdimen\itex@thd% \def\itexspace#1#2#3{\itex@wd=#3em% \itex@wd=0.1\itex@wd% \itex@dp=#2ex% \itex@dp=0.1\itex@dp% \itex@thd=#1ex% \itex@thd=0.1\itex@thd% \advance\itex@thd\the\itex@dp% \makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}} \makeatother % \tensor and \multiscript \makeatletter \newif\if@sup \newtoks\@sups \def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}% \def\reset@sup{\@supfalse\@sups={}}% \def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else% \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}% \else \append@sup#2 \@suptrue \fi% \expandafter\mk@scripts\fi} \def\tensor#1#2{\reset@sup#1\mk@scripts#2_/} \def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2% \reset@sup\mk@scripts#3_/} \makeatother % \slash \makeatletter \newbox\slashbox \setbox\slashbox=\hbox{$/$} \def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$} \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa \copy\slashbox \kern-\@tempdima \box\@tempboxa} \def\slash{\protect\itex@pslash} \makeatother % math-mode versions of \rlap, etc % from Alexander Perlis, "A complement to \smash, \llap, and lap" % http://math.arizona.edu/~aprl/publications/mathclap/ \def\clap#1{\hbox to 0pt{\hss#1\hss}} \def\mathllap{\mathpalette\mathllapinternal} \def\mathrlap{\mathpalette\mathrlapinternal} \def\mathclap{\mathpalette\mathclapinternal} \def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}} \def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}} \def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}} % Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2} \let\oldroot\root \def\root#1#2{\oldroot #1 \of{#2}} \renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}} % Manually declare the txfonts symbolsC font \DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n} \SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n} \DeclareFontSubstitution{U}{txsyc}{m}{n} % Manually declare the stmaryrd font \DeclareSymbolFont{stmry}{U}{stmry}{m}{n} \SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n} % Manually declare the MnSymbolE font \DeclareFontFamily{OMX}{MnSymbolE}{} \DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n} \SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n} \DeclareFontShape{OMX}{MnSymbolE}{m}{n}{ <-6> MnSymbolE5 <6-7> MnSymbolE6 <7-8> MnSymbolE7 <8-9> MnSymbolE8 <9-10> MnSymbolE9 <10-12> MnSymbolE10 <12-> MnSymbolE12}{} % Declare specific arrows from txfonts without loading the full package \makeatletter \def\re@DeclareMathSymbol#1#2#3#4{% \let#1=\undefined \DeclareMathSymbol{#1}{#2}{#3}{#4}} \re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46} \re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12} \re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64} \re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6} \re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77} \re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77} \makeatother % \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE \makeatletter \def\Decl@Mn@Delim#1#2#3#4{% \if\relax\noexpand#1% \let#1\undefined \fi \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}} \def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}} \def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}} \Decl@Mn@Open{\llangle}{mnomx}{'164} \Decl@Mn@Close{\rrangle}{mnomx}{'171} \Decl@Mn@Open{\lmoustache}{mnomx}{'245} \Decl@Mn@Close{\rmoustache}{mnomx}{'244} \makeatother % Widecheck \makeatletter \DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}} \def\@widecheck#1#2{% \setbox\z@\hbox{\m@th$#1#2$}% \setbox\tw@\hbox{\m@th$#1% \widehat{% \vrule\@width\z@\@height\ht\z@ \vrule\@height\z@\@width\wd\z@}$}% \dp\tw@-\ht\z@ \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@ \setbox\tw@\hbox{% \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box \tw@}}}% {\ooalign{\box\tw@ \cr \box\z@}}} \makeatother % \mathraisebox{voffset}[height][depth]{something} \makeatletter \NewDocumentCommand\mathraisebox{moom}{% \IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{% \IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}% }{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}% \mathpalette\@temp{#4}} \makeatletter % udots (taken from yhmath) \makeatletter \def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.} \mkern2mu\raise4\p@\hbox{.}\mkern1mu \raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}} \makeatother %% Fix array \newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}} %% \itexnum is a noop \newcommand{\itexnum}[1]{#1} %% Renaming existing commands \newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}} \newcommand{\widevec}{\overrightarrow} \newcommand{\darr}{\downarrow} \newcommand{\nearr}{\nearrow} \newcommand{\nwarr}{\nwarrow} \newcommand{\searr}{\searrow} \newcommand{\swarr}{\swarrow} \newcommand{\curvearrowbotright}{\curvearrowright} \newcommand{\uparr}{\uparrow} \newcommand{\downuparrow}{\updownarrow} \newcommand{\duparr}{\updownarrow} \newcommand{\updarr}{\updownarrow} \newcommand{\gt}{>} \newcommand{\lt}{<} \newcommand{\map}{\mapsto} \newcommand{\embedsin}{\hookrightarrow} \newcommand{\Alpha}{A} \newcommand{\Beta}{B} \newcommand{\Zeta}{Z} \newcommand{\Eta}{H} \newcommand{\Iota}{I} \newcommand{\Kappa}{K} \newcommand{\Mu}{M} \newcommand{\Nu}{N} \newcommand{\Rho}{P} \newcommand{\Tau}{T} \newcommand{\Upsi}{\Upsilon} \newcommand{\omicron}{o} \newcommand{\lang}{\langle} \newcommand{\rang}{\rangle} \newcommand{\Union}{\bigcup} \newcommand{\Intersection}{\bigcap} \newcommand{\Oplus}{\bigoplus} \newcommand{\Otimes}{\bigotimes} \newcommand{\Wedge}{\bigwedge} \newcommand{\Vee}{\bigvee} \newcommand{\coproduct}{\coprod} \newcommand{\product}{\prod} \newcommand{\closure}{\overline} \newcommand{\integral}{\int} \newcommand{\doubleintegral}{\iint} \newcommand{\tripleintegral}{\iiint} \newcommand{\quadrupleintegral}{\iiiint} \newcommand{\conint}{\oint} \newcommand{\contourintegral}{\oint} \newcommand{\infinity}{\infty} \newcommand{\bottom}{\bot} \newcommand{\minusb}{\boxminus} \newcommand{\plusb}{\boxplus} \newcommand{\timesb}{\boxtimes} \newcommand{\intersection}{\cap} \newcommand{\union}{\cup} \newcommand{\Del}{\nabla} \newcommand{\odash}{\circleddash} \newcommand{\negspace}{\!} \newcommand{\widebar}{\overline} \newcommand{\textsize}{\normalsize} \renewcommand{\scriptsize}{\scriptstyle} \newcommand{\scriptscriptsize}{\scriptscriptstyle} \newcommand{\mathfr}{\mathfrak} \newcommand{\statusline}[2]{#2} \newcommand{\tooltip}[2]{#2} \newcommand{\toggle}[2]{#2} % Theorem Environments \theoremstyle{plain} \newtheorem{theorem}{Theorem} \newtheorem{lemma}{Lemma} \newtheorem{prop}{Proposition} \newtheorem{cor}{Corollary} \newtheorem*{utheorem}{Theorem} \newtheorem*{ulemma}{Lemma} \newtheorem*{uprop}{Proposition} \newtheorem*{ucor}{Corollary} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{example}{Example} \newtheorem*{udefn}{Definition} \newtheorem*{uexample}{Example} \theoremstyle{remark} \newtheorem{remark}{Remark} \newtheorem{note}{Note} \newtheorem*{uremark}{Remark} \newtheorem*{unote}{Note} %------------------------------------------------------------------- \begin{document} %------------------------------------------------------------------- \section*{partial combinatory algebra} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{constructivism_realizability_computability}{}\paragraph*{{Constructivism, Realizability, Computability}}\label{constructivism_realizability_computability} [[!include constructivism - contents]] \hypertarget{contents}{}\section*{{Contents}}\label{contents} \noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak \noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak \noindent\hyperlink{functional_completeness}{Functional completeness}\dotfill \pageref*{functional_completeness} \linebreak \noindent\hyperlink{examples_of_combinators}{Examples of combinators}\dotfill \pageref*{examples_of_combinators} \linebreak \noindent\hyperlink{examples_of_pcas}{Examples of PCAs}\dotfill \pageref*{examples_of_pcas} \linebreak \noindent\hyperlink{realizability_toposes}{Realizability toposes}\dotfill \pageref*{realizability_toposes} \linebreak \noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{idea}{}\subsection*{{Idea}}\label{idea} A partial combinatory algebra is a generalization of a model of the [[untyped lambda calculus]] allowing for application to be only partially defined. It is often expressed as an algebraic abstraction of [[combinatory logic]]. \hypertarget{definition}{}\subsection*{{Definition}}\label{definition} The following definitions are taken from \hyperlink{Hofstra}{Hofstra}. A \emph{partial applicative structure} is a set equipped with a partial binary operation \begin{displaymath} m \colon A \times A \to A \end{displaymath} An [[function application|application]] of $m$ is indicated by juxtaposition: $a b$ denotes $m(a, b)$ if (and only if) $m(a, b)$ is defined, i.e., if $(a, b)$ belongs to the [[domain]] of $m$. \emph{Homomorphisms} between partial applicative structures $A, B$ are defined to be total functions $f \colon A \to B$ such that $f(a b) = f(a)f(b)$, meaning the right side is defined whenever the left side is. In other words, in the locally posetal [[bicategory]] of sets and [[relation|relations]], we have a 2-cell \begin{displaymath} \itexarray{ A \times A & \stackrel{f \times f}{\to} & B \times B \\ m \downarrow & \leq & \downarrow m \\ A & \underset{f}{\to} & B } \end{displaymath} By convention, unbracketed juxtapositions are associated to the left, so that for example $x y z$ means $(x y)z$. If $A$ is a partial applicative structure and $\mathbf{Magma}(A)$ is the free [[magma]] on the underlying set of $A$, then we have an evident partial function \begin{displaymath} \alpha \colon \mathbf{Magma}(A) \to A \end{displaymath} which evaluates binary words in $A$ as elements in $A$, whenever possible, using the partial applicative structure and induction on the structure of the word. \begin{defn} \label{}\hypertarget{}{} A partial applicative structure $A$ is a \emph{partial combinatory algebra} (a \textbf{PCA}) if there are elements $k, s \in A$ such that \begin{itemize}% \item For all $a, b \in A$, $k a$ and $k a b$ are defined and $k a b = a$. \item For all $a, b \in A$, $s a$ and $s a b$ are defined and for all $c$, $(a c)(b c)$ is defined if and only if $s a b c$ is defined, and $s a b c = (a c)(b c)$. \end{itemize} A \emph{homomorphism} of PCA's is a homomorphism of the underlying partial applicative structures. A \emph{total} combinatory algebra is a PCA $A$ whose application $m \colon A \times A \to A$ is a total function. \end{defn} Note that appropriate elements $k$, $s$ are not considered part of the structure (to be preserved under homomorphism) -- here one is interested only in the property that such elements exist. Indeed, they need not be uniquely determined within the PCA. \hypertarget{functional_completeness}{}\subsection*{{Functional completeness}}\label{functional_completeness} The definition of PCA given above is traditional but somewhat opaque at first glance. The real point of the definition is that a PCA is the same thing as a partial applicative structure $A$ that enjoys a \emph{functional completeness} property, in the following sense. Let $X$ be a countably infinite set of ``variables'', and let $A[X]$ denote the [[magma]] freely generated from the disjoint sum $A + X$. Each term $t$, i.e., each element $t \in A[X]$, has finitely many $x_i \in X$ occurring inside it; these are called the \emph{free variables} of $t$, and we write $FV(t)$ for the set of free variables. If $FV(t) \subseteq \{x_0, x_1, \ldots, x_n\}$, then we can think of $t$ as giving a partially defined function in $n+1$ variables. That is, we may consider $t$ as a term of $\mathbf{Magma}(A + \{x_0, \ldots, x_n\})$, and (partially) define the [[substitution]] $t[a_0/x_0, \ldots, a_n/x_n]$ where $a_0, \ldots, a_n$ are elements of $A$, by evaluating at $t$ of the composite \begin{displaymath} \mathbf{Magma}(A + \{x_0, \ldots, x_n\}) \stackrel{\mathbf{Magma}(\phi)}{\to} \mathbf{Magma}(A) \stackrel{\alpha}{\to} A \end{displaymath} where $\phi(x_i) = a_i$ and is elsewhere the identity. Then, we say $A$ is \emph{functionally complete} if every term $t \in A[X]$, viewed as a partial operation on $A$, is represented by some element in $A$. To be precise: for each term $t$ with $FV(t) \subseteq \{x_0, \ldots, x_n\}$, there exists an element $a \in A$ such that \begin{itemize}% \item For all $a_0, \ldots, a_{n-1} \in A$, $a a_0 \ldots a_{n-1}$ is defined; \item For all $a_0, \ldots, a_n \in A$, $t[a_0/x_0, \ldots, a_n/x_n]$ is defined precisely when $a a_0 \ldots a_n$ is defined, and these two elements are equal. \end{itemize} For example, if $k$, $s$ are elements which realize $A$ as a PCA, then $k$ represents the term $t = x_0$ viewed as belonging to $\mathbf{Magma}(A + \{x_0, x_1\})$, and $s$ represents the term $(x_0 x_2)(x_1 x_2)$ viewed as belonging to $\mathbf{Magma}(A + \{x_0, x_1, x_2)\}$. \begin{theorem} \label{}\hypertarget{}{} A partial combinatory algebra is functionally complete. \end{theorem} \begin{proof} The idea is to simulate $\lambda$-abstraction $\lambda x. t$, where $x \in X$ is a variable and $t$ is a term, by induction on $t$. Indeed, given elements $k, s$ that realize $A$ as a PCA, put \begin{displaymath} \itexarray{ \lambda x. x & \coloneqq & s k k & \\ \lambda x. t & \coloneqq & k t & if x \notin FV(t) \\ \lambda x. t t' & \coloneqq & s(\lambda x. t)(\lambda x. t') } \end{displaymath} One then proves equality of partial functions $(\lambda x. t)(a) = t[a/x]$, by induction on $t$. \end{proof} \hyperlink{Hofstra}{Hofstra} \emph{defines} a PCA to be a functionally complete partial applicative structure. This is an unbiased definition, in the sense that it does not privilege certain elements $k$, $s$ (or, for that matter, any other system of combinators that provide functional completeness). \hypertarget{examples_of_combinators}{}\subsubsection*{{Examples of combinators}}\label{examples_of_combinators} \begin{enumerate}% \item Let us check that $s k k$ indeed represents the identity function $I$. This is trivial: we have, for any $a \in A$, equalities between defined terms \begin{displaymath} s k k a = (k a)(k a) = a. \end{displaymath} \item Consider the second projection function, corresponding to $x_1 \in \mathbf{Magma}(A + \{x_0, x_1\})$. Thinking in terms of $\lambda$-terms, this is represented by $\lambda x. \lambda y. y = \lambda x. s k k = k(s k k)$, or $k I$. In other words, we calculate \begin{displaymath} k I a b = ((k I) a) b = I b = b. \end{displaymath} \item Following the proof of functional completeness, we have \begin{displaymath} \lambda x. x x = s(\lambda x. x)(\lambda x. x) = s I I \end{displaymath} \item Finally, consider the classical construction of the [[fixed-point combinator]], $Y = \lambda y. (\lambda x. y(x x))(\lambda x. y(x x))$. We have firstly \begin{displaymath} \lambda x. y(x x) = s(\lambda x. y)(\lambda x. x x) = s(k y)(s I I) \end{displaymath} which means \begin{displaymath} \itexarray{ Y & = & \lambda y. (s I I)(s(k y)(s I I)) \\ & = & s(\lambda y. s I I)(\lambda y. s(k y)(s I I)) \\ & = & s(k (s I I))(s(\lambda y. s(k y))(\lambda y. s I I) \\ & = & s(k (s I I))(s(s (k s)(\lambda y. k y)))(k (s I I)) \\ & = & s(k (s I I))(s(s (k s)(s(k k)I)))(k (s I I)) } \end{displaymath} \end{enumerate} \hypertarget{examples_of_pcas}{}\subsection*{{Examples of PCAs}}\label{examples_of_pcas} \begin{enumerate}% \item (Kleene's first algebra.) Suppose given a coding of all [[partial recursive functions]] of the form $\mathbb{N}^k \to \mathbb{N}$ (ranging over $k = 0, 1, 2, \ldots$) by elements of $\mathbb{N}$, and a coding of elements of $\mathbb{N}^k$ over all $k$ by elements of $\mathbb{N}$. Define a partial applicative structure \begin{displaymath} \mathbb{N} \times \mathbb{N} \to \mathbb{N} \end{displaymath} where $p q = \{p\}([q])$ whenever the right side is defined, where $\{p\}$ is the $p^{th}$ partial recursive function and $[q]$ is the $q^{th}$ tuple. It may be checked that $k$ and $s$, defined extensionally in the obvious way, are partial recursive functions, so we get in this way a PCA. \item Suppose we have a [[cartesian closed category]] generated by an object $X$ such that $X \times X$ and $X^X$ are retracts of $X$. Then elements $1 \to X$ form a PCA, in fact a total combinatory algebra, where the applicative structure is \begin{displaymath} X \times X \stackrel{r \times 1_X}{\to} X^X \times X \stackrel{eval}{\to} X \end{displaymath} for some chosen retraction $r$. In other words, models of the untyped [[lambda calculus]] give PCA's. \item [[Kleene's second algebra]]. \end{enumerate} \hypertarget{realizability_toposes}{}\subsection*{{Realizability toposes}}\label{realizability_toposes} From any PCA, a corresponding ``[[realizability]] [[tripos]]'' can be constructed, from which, in turn, a corresponding ``realizability topos'' can be constructed, as outlined in the article on [[tripos|triposes]]. A preliminary technical task is to encode pairing and unpairing functions by elements of $A$. By this we mean functions $p \colon A \times A \to A$, $l \colon A \to A$, $r \colon A \to A$ such that for all $(a, a') \in A \times A$, we have $(a, a') = (l(p(a, a')), r(p(a, a')))$. One way of doing this is to put \begin{itemize}% \item $p = \lambda x. \lambda y. \lambda z. z x y$ \item $l = \lambda p. p(\lambda x. \lambda y. x)$ \item $r = \lambda p. p(\lambda x. \lambda y. y)$ \end{itemize} whereupon we may calculate \begin{displaymath} \itexarray{ p a a' & = & \lambda z. z a a' \\ l(p a a') & = & (\lambda z. z a a')(\lambda x. \lambda y. x) \\ & = & (\lambda x. \lambda y. x) a a' \\ & = & (\lambda y. a) a' = a } \end{displaymath} \begin{displaymath} \itexarray{ r(p a a') & = & (\lambda z. z a a')(\lambda x. \lambda y. y) \\ & = & (\lambda x. \lambda y. y) a a' \\ & = & (\lambda y. y) a' = a' } \end{displaymath} That out of the way, let $P(A)$ be the power set of $A$ and let $X$ be a set. Put a preorder structure on $P(A)^X$ as follows: given $f, g \in P(A)^X$, let $Hom(f, g)$ be the set of $a$ in $A$ such that for all $x$ in $X$ and $a'$ in $f(x)$, $a a'$ is defined (that is, $a$ is applicable to $a'$), and $a a'$ is an element of $g(x)$. We can turn this into a preorder by taking $f \leq g$ just in case $Hom(f, g)$ is inhabited. \begin{theorem} \label{}\hypertarget{}{} The preorder $P(A)^X$ has finite products, finite coproducts, and is cartesian closed. In other words, the preorder $P(A)^X$ is a [[Heyting prealgebra]]. \end{theorem} \begin{proof} An initial object is given by the constant function taking each $x$ to the empty subset $\emptyset \subseteq A$, and a terminal object is given by the constant function taking each $x$ to the full subset $A \subseteq A$. Take $f, g \colon X \to P(A)$. For binary products, define \begin{displaymath} (f \wedge g)(x) = \{p a a' | a \in f(x) \wedge a' \in g(x)\} \end{displaymath} Notice that $l$ realizes $f \wedge g \leq f$ (since $l (p a a') = a$), and similarly $r$ realizes $f \wedge g \leq g$. Furthermore, suppose given $h \colon X \to P(A)$, and that $t \in A$ realizes $h \leq f$ and $u \in A$ realizes $h \leq g$. Then \begin{displaymath} v = \lambda b. p (t b)(u b) \end{displaymath} realizes $h \leq f \wedge g$. Thus $f \wedge g$ is a product in the preorder. For binary coproducts, define \begin{displaymath} (f \vee g)(x) = \{p l a | a \in f(x)\} \cup \{p r a' | a' \in g(x)\} \end{displaymath} Then $p l$ realizes $f \leq f \vee g$ and $p r$ realizes $g \leq f \vee g$. Furthermore, suppose $t$ realizes $f \leq h$ and $u$ realizes $g \leq h$. Then \begin{displaymath} v = \lambda b. l(b)(p(t(r b))(u(r b))) \end{displaymath} realizes $f \vee g \leq h$. Indeed, we have \begin{displaymath} \itexarray{ v(p l a) & = & l(p l a)(p(t(r(p l a)))(u(r(p l a)))) \\ & = & l(p(t a)(u a)) \\ & = & t a } \end{displaymath} and similarly $v(p r a') = u a'$. In either case, we see $v(b)$ lives in $h(x)$ for any $b \in (f \vee g)(x)$. For cartesian closure, define \begin{displaymath} (f \Rightarrow g)(x) = \{a' | \forall a \in f(x) a' a \downarrow \wedge a' a \in g(x)\} \end{displaymath} where $a' a \downarrow$ is standard shorthand for ``$a' a$ is defined''. Then for any $f$ and $g$, the combinator $\lambda b. l(b)r(b)$ realizes $(f \Rightarrow g) \wedge f \leq g$, and the combinator $\lambda b. \lambda a. p a b$ realizes $g \leq f \Rightarrow (f \wedge g)$. \end{proof} For any function $f \colon X \to Y$, it is immediate that \begin{displaymath} P(A)^f \colon P(A)^Y \to P(A)^X \end{displaymath} is a functor preorder map that preserves Heyting prealgebra structure. Furthermore, in the case of a projection map $f \colon Z \times Y \to Y$, there will be left and right adjoints to $P(A)^f \colon P(A)^Y \to P(A)^{Z \times Y} (\cong (P(A)^Z)^Y)$, as induced by the union and intersection maps from $P(A)^Z$ to $P(A)$. \hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts} \begin{itemize}% \item [[combinatory logic]] \item [[realizability]] \item [[Turing category]] \end{itemize} [[!include computable mathematics -- table]] \hypertarget{references}{}\subsection*{{References}}\label{references} \begin{itemize}% \item Pieter J.W. Hofstra, \emph{Partial Combinatory Algebras and Realizability Toposes}, (\href{http://mysite.science.uottawa.ca/phofstra/}{web}) (\href{http://www.google.com/url?sa=t&rct=j&q=&esrc=s&source=web&cd=2&ved=0CF8QFjAB&url=http%3A%2F%2Fmysite.science.uottawa.ca%2Fphofstra%2FKananaskis.pdf&ei=georUITcEebV0QGctIGwDg&usg=AFQjCNFywYRYAfzrgHFq5AsaBZ5li_qfyQ&sig2=BCT05ts3GBLntD2VZazC4w}{pdf}) \end{itemize} Lecture notes include \begin{itemize}% \item [[Andrej Bauer]], section 2 of \emph{Realizability as connection between constructive and computable mathematics}, in T. Grubba, P. Hertling, H. Tsuiki, and [[Klaus Weihrauch]], (eds.) \emph{CCA 2005 - Second International Conference on Computability and Complexity in Analysis}, August 25-29,2005, Kyoto, Japan, ser. Informatik Berichte, , vol. 326-7/2005. FernUniversit\"a{}t Hagen, Germany, 2005, pp. 378--379. (\href{http://math.andrej.com/data/c2c.pdf}{pdf}) \end{itemize} [[!redirects combinatory algebra]] [[!redirects partial combinatory algebra]] [[!redirects partial combinatory algebras]] [[!redirects Kleene's first algebra]] [[!redirects Kleene's first partial combinatory algebra]] [[!redirects realizability tripos]] [[!redirects PCA]] [[!redirects PCAs]] \end{document}