L¿$l<$ R¿$r<$ C¿$c<$

# Native Type Theory

Christian Williams University of California, Riverside, US
<EMAIL_ADDRESS>Pyrofex Corporation, Utah, US Michael Stay Pyrofex
Corporation, Utah, US<EMAIL_ADDRESS>
###### Abstract

Native type systems are those in which type constructors are derived from term
constructors, as well as the constructors of predicate logic and
intuitionistic type theory. We present a method to construct native type
systems for a broad class of languages, $\lambda$-theories with equality, by
embedding such a theory into the internal language of its topos of presheaves.
Native types provide total specification of the structure of terms; and by
internalizing transition systems, native type systems serve to reason about
structure and behavior simultaneously. The construction is functorial, thereby
providing a shared framework of higher-order reasoning for many languages,
including programming languages.

##  1 Introduction

Type theory is growing as a guiding philosophy in the design of programming
languages. However in practice, type systems are heterogeneous, and there are
no standard ways to reason across languages. We present a functorial method to
enhance a language with “its own internal logic”, using tools and ideas of
category theory.

Categorical logic unifies languages: virtually any formalism, from monoids to
dependent type theory, can be modelled by structured categories [18]. By doing
so, we inherit a wealth of tools from category theory. In particular, we can
generate expressive type systems by composing two known ideas.

${{\lambda\mathtt{theory}}}$${{\mathtt{topos}}}$${{\mathtt{type\;system}}}$$\scriptstyle{\mathscr{P}}$$\scriptstyle{\mathscr{L}}$

The first is the presheaf construction $\mathscr{P}$ [9, Ch. 8]; it preserves
product, equality, and function types. The second is the language of a topos
$\mathscr{L}$ [18, Ch. 11]. The composite is 2-functorial, so that
translations between languages induce translations between type systems.

Note — This idea is quite simple; in fact it was considered more than fifty
years ago by Scott [32]. Native type theory simply gives a name to the
language of presheaves on theories; we aim to demonstrate its utility, and
advocate for real-world application of categorical logic.

The type system is native in the sense that type constructors are derived from
term constructors, plus those of predicate logic and (co/inductive)
intuitionistic type theory. For example, the following predicate on processes
in a concurrent language (ex. 5) is effectively a compile-time firewall.

$\begin{array}[]{l}\mathsf{sole.in}(\alpha)\;:=\;\;\;\nu\mathtt{X}.\;(\mathtt{in}(\alpha,\mathtt{N}\to\mathtt{X})\;|\;\mathtt{P})\land\neg[\mathtt{in}(\neg[\alpha],\mathtt{N}\to\mathtt{P})\;|\;\mathtt{P}]\\\
\textit{Can input on channels in type $\alpha$ and cannot input on
$\neg\alpha$, and continues as such.}\end{array}$

Native type theory is intended to be a practical method to equip programming
languages with a shared system of higher-order reasoning. The authors believe
that the potential applications are significant and broad, and we encourage
community development.

###  1.1 Motivation and implementation

As software systems become increasingly complex, it is critical to develop
adequate frameworks for reasoning about code systematically across languages.
By generating type systems for programming languages, native type theory can
improve control, reasoning, and communication of systems.

For example, web browsers use the dynamic, weakly-typed language of
JavaScript. Companies have recognized that correct and maintainable code
requires static type checking. Microsoft’s TypeScript [7], Facebook’s Flow
[2], and Google’s Closure Compiler [3] are multi-million dollar efforts to
retrofit JavaScript with a strong, static type system; yet none of these is
sound. When presented as a structured $\lambda$-theory [6], JavaScript has a
native type system which is sound by construction.

Native type theory is intended to be implemented as a development environment,
based on a library of formal semantics and translations, in which one can
program in languages enhanced by their native type systems. Code can be
written in the same way, but enriched with predicates and dependent types,
both (1) to condition existing codebases and (2) to expand software
capability.

To this end, we plan to leverage progress in language specification. K
Framework [5] is a formal verification tool which is used to give complete
semantics of many popular languages, including JavaScript, C, Java, Python,
Haskell, LLVM, Solidity, and more. These specifications can be presented as
$\lambda$-theories with equality ($\S$2), and input to native type theory.

The type system generated can then be used for many purposes, e.g. to query
codebases. The search engine Hoogle [4] queries Haskell libraries by function
signature. This idea can be expanded to many languages and strengthened by
more expressive types. If $\varphi:\mathtt{S}\to\mathsf{Prop}$ is a predicate
on $\mathtt{S}$-terms and $\psi:\mathtt{T}\to\mathsf{Prop}$ is one on
$\mathtt{T}$-terms, e.g. a security property, we can form the type of programs
$\mathtt{S}\to\mathtt{T}$ for which substituting $\varphi$ entails $\psi$
($\S$3.1, def. 14).

$[\varphi,\psi]:=\\{\lambda x.c:\mathtt{S}\to\mathtt{T}\;|\;\forall
p:\mathtt{S}.\;\varphi(p)\Rightarrow\psi(c[p/x])\\}$

Of course, the full applications of native type systems require substantial
development. Most basic is the need for efficient type-checking, but this is
well-studied [33]. For usability, there will need to be libraries of native
types, so programmers can express useful ideas without overly complex
formulae.

The larger endeavor, to create a framework for reasoning across many
languages, calls for developing a public library of both formal semantics and
translations between languages.

###  1.2 Organization and contribution

Our goal is to demonstrate that composing two categorical ideas can be highly
useful to computer science. In the process we emphasize many ideas that may be
“known” in theory but are not widely known nor used in practice. The main
original contribution is that by internalizing transition systems in
$\lambda$-theories, native type systems can reason about both the structure
and behavior of terms simultaneously.

$\S$2 Structured $\lambda$-theories. We define $\lambda$-theories with
equality as cartesian closed categories with pullbacks, and we interpret the
internal language as simply-typed $\lambda$-calculus combined with the syntax
of generalized algebraic theories [13].

Theories ordinarily model the structure of programs, while behavior is
modelled separately [36]; but in fact transition systems can be modelled as
internal categories. The concept of “language equipped with a notion of
behavior” motivates the 2-category of structured $\lambda$-theories. We define
the $\uprho\pi$-calculus [27], a concurrent language with reflection, as our
running example for native types.

$\S$3 Logic in a presheaf topos. A $\lambda$-theory $\mathsf{T}$ embeds into a
presheaf topos $\mathscr{P}(\mathsf{T})$, and we develop its internal
language. Predicates on the sorts of $\mathsf{T}$ form a $\lambda$-theory
$\omega\mathsf{T}$ which refines the entire language; refined binding is then
applied to condition program input ($\S$5).

We show that the predicate and codomain fibrations of
$\mathscr{P}(\mathsf{T})$ form a “cosmic” higher-order dependent type theory
(HDT), and this construction is 2-functorial.

Hence native type theory is the composite 2-functor

${{\lambda\mathrm{Thy}_{\\_}{=}^{\mathsf{op}}}}$${{\mathrm{Topos}}}$${{\mathrm{HDT}\Sigma.}}$$\scriptstyle{\mathscr{P}}$$\scriptstyle{\mathscr{L}}$

This extends to structured $\lambda$-theories, i.e. the arrow 2-categories
over this composite.

$\S$4 Native type theory. The native type system of a $\lambda$-theory
$\mathsf{T}$ is presented as the internal language of the presheaf topos,
$\mathscr{L}\mathscr{P}(\mathsf{T})$. The system is an extension of higher-
order dependent type theory [18], as in the Calculus of Constructions [14]. We
present the system as generated by $\mathsf{T}$, and give the rules for types
and terms, as well as those for functoriality.

$\S$5 Applications. We explore a few kinds of applications: conditioning term
behavior, with subgraphs of rewrite systems and modalities, and deriving
behavioral equivalence; conditioning program input with refined binding, and
reasoning about contexts with predicate homs; and translating types across
programming paradigms. The scope of applications is beyond what can be given
here.

##  2 Structured lambda-theories

Simply-typed $\lambda$-calculus is the language of products and functions. It
is regarded as the foundation of computer science [11] and much of modern
programming [16].

The syntax of a language can be modelled by a syntactic category, in which an
object is a sorted variable context, a morphism is a term constructor, and
composition is substitution. The $\lambda$-calculus is the syntax of cartesian
closed categories [20].

A particular $\lambda$-calculus or $\lambda$-theory is presented by sorts,
constructors, and equations. This is just like presenting an algebraic
structure such as groups, but with higher-order constructors (ex. 5,
$\mathsf{input}$). References for the syntax and semantics of simply-typed
$\lambda$-calculus are [15, Ch. 4] and [18, Ch. 2]. To save space in
presentations, we denote products by $\mathtt{S},\mathtt{T}$ and functions by
$[\mathtt{S}\to\mathtt{T}]$.

The main rules of a $\lambda$-theory define how to construct and use
functions.

$\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}\quad\quad\quad\quad\quad\quad\quad\quad\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}$

######  Definition 1.

A $\lambda$-theory with equality is a cartesian closed category with
pullbacks, also known as a “properly cartesian closed category” [19]. The
2-category of $\lambda$-theories with equality, finitely continuous closed
functors, and natural transformations is $\lambda\mathrm{Thy}_{\\_}{=}.$

The syntax of a $\lambda$-theory with equality can be derived from its
subobject fibration having fibered equality [18, Ch. 3]. We interpret the
language as simply-typed $\lambda$-calculus combined with the syntax of
generalized algebraic theories [13], which provide indexed sorts.

$\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}$

$\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}$

Indexed sorts are highly expressive. If we take the source map of a graph
$s:\mathtt{E}\to\mathtt{V}$ as an indexed sort, then $s(v)$ is the sort of
edges out of a vertex — i.e., the behavior of a term.

Henceforth, “$\lambda$-theory” means $\lambda$-theory with equality.

###  $\lambda$-theories with behavior

What $\lambda$-theories do not explicitly represent is the process of
computation. In practice, computing consists not of equations but transitions.
There are many ways to model the behavior of languages [36], but the
operational semantics of higher-order languages is still in development [17].
We introduce a method of representing behavior internally.

A language with a rewrite system can be modelled by a $\lambda$-theory
$\mathsf{T}$ with an internal category, which includes constructors and
equations to specify the interaction between rewrites and constructors, a.k.a.
the operational semantics. First, here is the theory of categories.

######  Definition 2.

$\mathsf{Th.Cat}$

$\begin{array}[]{rlcrlcrcl}\mathtt{Hom}:&\mathtt{E}\to\mathtt{V},\mathtt{V}&&;_{\\_}{abc}:&\mathtt{Hom}(a,b),\mathtt{Hom}(b,c)\to\mathtt{Hom}(a,c)&&(e_{\\_}1;e_{\\_}2);e_{\\_}3&=&e_{\\_}1;(e_{\\_}2;e_{\\_}3)\\\
&&&\mathtt{id}_{\\_}a:&1\to\mathtt{Hom}(a,a)&&\mathtt{id}_{\\_}a;e=e&&e;\mathtt{id}_{\\_}b=e\end{array}$

Given $(a,b):\Gamma\to\mathtt{V},\mathtt{V}$ we denote
$e:\Gamma\to\mathtt{Hom}(a,b)$ by $e(\vec{x}):a(\vec{x})\leadsto b(\vec{x}).$

Note — Though composition is useful, we often want to reason about “basic
rewrites” or single-step computations. For most of the paper we will simply
use an internal graph. It is easy to combine both approaches, by
distinguishing one sort for edges and one sort for morphisms.

Operational semantics describes how term constructors interact with the
transition system [36]: given a constructor
$\mathtt{f}:\prod\mathtt{S}_{\\_}i\to\mathtt{T}$ and terms
$v_{\\_}i:\mathtt{S}_{\\_}i$ with edges $e_{\\_}{ij}:v_{\\_}i\leadsto
w_{\\_}{ij}$, what is the behavior of $\mathtt{f}(v_{\\_}1,\dots,v_{\\_}n)$?

$\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}$

To specify this interaction, we take the source map
$s:\mathtt{E}\to\mathtt{S}$ as an indexed sort $\mathtt{S}^{\ast}(x)$; then
$\mathtt{S}^{\ast}(v)$ are the edges with source $v$. This allows us to define
operational semantics in a $\lambda$-theory.

######  Definition 3.

Let $\mathsf{T}$ be a $\lambda$-theory with sorts $\mathtt{S}_{\\_}i$,
constructors
$\mathtt{f}_{\\_}{ij}:\prod_{\\_}j\mathtt{S}_{\\_}{ij}\to\mathtt{S}_{\\_}i$,
and graphs for each sort. A behavior rule for a term constructor
$\mathtt{f}:\prod\mathtt{S}_{\\_}i\to\mathtt{S}$ is a constructor

$\mathsf{R}(\mathtt{f})_{\\_}{\vec{v}}:\prod\mathtt{S}^{\ast}_{\\_}i(v_{\\_}i)\to\mathtt{S}^{\ast}(\mathtt{f}(\vec{v}))$

such that
$\mathsf{R}(\mathtt{f})_{\\_}{\vec{v}}(e_{\\_}1,\dots,e_{\\_}n):\mathtt{f}(\vec{v})\leadsto\mathtt{g}(\vec{e})$,
where $\mathtt{g}:\prod\mathtt{S}^{\ast}_{\\_}i(v_{\\_}i)\to\mathtt{S}$.

An operational semantics for $\mathsf{T}$ is for each sort a family of edges
$\\{\mathtt{r}_{\\_}{ij}(\vec{x}):\mathtt{a}_{\\_}{ij}(\vec{x})\leadsto\mathtt{b}_{\\_}{ij}(\vec{x}):\mathtt{E}_{\\_}{\mathtt{S}_{\\_}i}\\}$
and for some term constructors a behavior rule
$\\{\langle\mathtt{f}_{\\_}{ij},\mathsf{R}(\mathtt{f}_{\\_}{ij})\rangle\\}$.
This defines a subtheory $\mathsf{O}(\mathsf{T})\to\mathsf{T}$.

######  Theorem 4.

Behavior rules correspond to GSOS rules [36] for deterministic labelled
transition systems. The general case can be derived using an internal relation
on $\mathtt{V},\mathtt{A},\mathtt{V}$, where $\mathtt{A}$ is a sort of
actions.

Hence, internal operational semantics are equivalent to GSOS distributive
laws. Providing a novel perspective to a basic topic in computer science, this
connection warrants exploration in future work.

By representing behavior internally, we will see that

native type systems reason about both the structure and behavior of terms.

For example, there can be a predicate for “contexts $\lambda
x.c:\mathtt{S}\to\mathtt{T}$ such that if $a:\mathtt{S}$ satisfies $\varphi$
then for all $e_{\\_}i:c[a/x]\leadsto b$ if $\psi_{\\_}i(b)$ then no step of
$e$ satisfies $\epsilon$”. Combining both kinds of reasoning is extremely
expressive, and the applications in $\S$5 provide only a modest glimpse.

######  Example 5.

$\uprho\pi$-calculus $\mathsf{Th}.\uprho\pi$ (polyadic)

The $\uprho\pi$-calculus or reflective higher-order $\pi$-calculus [27] is a
concurrent language succeeding the $\pi$-calculus [29]. It is the language of
the blockchain platform RChain [8].

The $\uprho\pi$-calculus has sorts $\mathtt{P}$ and $\mathtt{N}$ for processes
and names, which act as code and data respectively. Reference $@$ and execute
$\ast$ transform one into the other. Terms are built up from the null process
$\mathtt{0}$ by parallel $-|-$, output $\mathtt{out}$, and input
$\mathtt{in}$. The basic rule is $\mathtt{comm}$: an output and input process
in parallel on the same name can communicate, transfering a list of processes
as data.

$\begin{array}[]{rlcrlcrl}\mathtt{0}:&1\to\mathtt{P}&&-|-:&\mathtt{P},\mathtt{P}\to\mathtt{P}&&(\mathtt{P},-|-,\mathtt{0})&\text{commutative
monoid}\\\
@:&\mathtt{P}\to\mathtt{N}&&\mathtt{out}_{\\_}k:&\mathtt{N},\mathtt{P}^{k}\to\mathtt{P}&&\mathtt{run}:&\mathtt{P}\to\mathtt{E}\\\
\ast:&\mathtt{N}\to\mathtt{P}&&\mathtt{in}_{\\_}k:&\mathtt{N},[\mathtt{N}^{k}\to\mathtt{P}]\to\mathtt{P}&&\mathtt{comm}_{\\_}k:&\mathtt{N},\mathtt{P}^{k},[\mathtt{N}^{k}\to\mathtt{P}]\to\mathtt{E}\end{array}$
$\begin{array}[]{rcl}\mathtt{comm}_{\\_}k(n,\vec{q_{\\_}i},\lambda\vec{x_{\\_}i}.p)&:&\mathtt{out}(n,\vec{q_{\\_}i})\;|\;\mathtt{in}(n,\lambda\vec{x_{\\_}i}.p)\leadsto
p[@q_{\\_}i/x_{\\_}i]\\\ \mathtt{run}(p)&:&\ast(@p)\leadsto p\end{array}$
$\begin{array}[]{lclcl}(s,t):\mathtt{E}\to\mathtt{P},\mathtt{P}&&\mathtt{par}_{\\_}l:\mathtt{E},\mathtt{P}\to\mathtt{E}&&\mathtt{par}_{\\_}l(\mathtt{r},q):s(\mathtt{r})|q\leadsto
t(\mathtt{r})|q\\\
\mathtt{par}_{\\_}r:\mathtt{P},\mathtt{E}\to\mathtt{E}&&\mathtt{par}_{\\_}r(p,\mathtt{r})=\mathtt{par}_{\\_}l(\mathtt{r},p)&&\mathtt{par}_{\\_}l\;\;\;\text{c.
monoid action of }\mathtt{P}\mbox{ on }\mathtt{E}\end{array}$

The $\uprho\pi$-calculus is our running example of a $\lambda$-theory. In the
native type system $\mathscr{L}\mathscr{P}(\mathsf{T})$ ($\S$4) of
$\mathsf{T}=\mathsf{Th}.\uprho\pi$, a predicate on names
$\alpha:y\mathtt{N}\to\mathsf{Prop}$ is called a namespace [26], and a
predicate on processes $\varphi:y\mathtt{P}\to\mathsf{Prop}$ is called a
codespace.

In distinguishing internal graphs and edge constructors for the behavior of
terms, we should also require that morphisms of “theories with behavior”
should respect this structure. We generalize to define “structure” as any
$\lambda$-theory morphism into $\mathsf{T}$.

######  Definition 6.

A structured $\lambda$-theory is a $\lambda$-theory with equality $\mathsf{T}$
equipped with a morphism $\tau:\mathsf{S}\to\mathsf{T}$. The 2-category of
$\mathsf{S}$-structured $\lambda$-theories is the strict coslice 2-category
$\mathsf{S}/\lambda\mathrm{Thy}_{\\_}=$. The 2-category of all structured
$\lambda$-theories is the strict arrow 2-category
$[\mathrm{I},\lambda\mathrm{Thy}_{\\_}=]$.

Because native type theory is functorial, a structure
$\tau:\mathsf{S}\to\mathsf{T}$ translates types of $\mathsf{T}$ into types of
$\mathsf{S}$. For including behavior, this simply distinguishes the
“behavioral” types; for more complex structures, the translation may be highly
expressive. As the concept is very general, we give a few more examples.

######  Example 7.

Sorting A polyadic language such as the $\uprho\pi$-calculus can be refined
with many sorts of name, and name sorts given sorted arities for input and
output. This is used by Milner [29] to designate channels to send and receive
certain kinds of data.

Sorting is a structure
$\sigma:S(\mathsf{Th}.\uprho\pi)\to\mathsf{Th}.\uprho\pi$, where the fiber
over $\mathtt{N}$ is the set of name sorts, and the fibers over
$\mathtt{in}_{\\_}k$ and $\mathtt{out}_{\\_}k$ are the sorted inputs and
outputs with total arity $k$.

The native type system of the structured $\lambda$-theory contains and
converts between the sorted and unsorted language. By functoriality, the type
system expands to the 2-category of all sorted $\uprho\pi$-calculi.

######  Example 8.

Encoding Because a structure is simply a morphism of $\lambda$-theories, we
can consider any translation $\tau:\mathsf{S}\to\mathsf{T}$ as a structured
$\lambda$-theory. This can be understood as compiling or encoding the programs
of $\mathsf{S}$ into those of $\mathsf{T}$.

For example if we encode a complex language like C++ into a simpler language
like name-passing $\lambda$-calculus, then we can identify a type of
$\lambda$-term with good properties and take its preimage along $\tau$ to form
a type of well-behaved C++ programs.

Another example is mapping a theory into a computing environment, such as a
virtual machine. This allows for reasoning about both languages and their
implementation.

From a structured $\lambda$-theory we derive a native type system, using the
presheaf construction, and demonstrate how it can be used to reason about the
structure and behavior of terms.

##  3 The Logic of a Presheaf Topos

Topos theory [23] expands the domain of predicate logic and intuitionistic
type theory [24] beyond sets and functions. Most useful is the fact that every
category embeds into a topos. For any $\lambda$-theory, the internal language
of its presheaf topos is its native type system.

Let $\mathsf{T}$ be a $\lambda$-theory. The category of presheaves is the
functor category $[\mathsf{T}^{\mathsf{op}},\mathrm{Set}]$, denoted
$\mathscr{P}(\mathsf{T})$. This defines a 2-functor to elementary toposes and
geometric morphisms

$\mathscr{P}:\lambda\mathrm{Thy}_{\\_}=^{\mathsf{op}}\to\mathrm{Topos}\quad\quad\mathscr{P}(\mathsf{F})=(\mathrm{Lan}_{\\_}\mathsf{F}\dashv\mathsf{F}^{\ast}):[\mathsf{T}^{\mathsf{op}},\mathrm{Set}]\to[\mathsf{S}^{\mathsf{op}},\mathrm{Set}].$

where $\mathrm{Lan}_{\\_}\mathsf{F}$ is left Kan extension [22, Ch. 10] and
$\mathsf{F}^{\ast}$ is precomposition by $\mathsf{F}:\mathsf{S}\to\mathsf{T}$.

A presheaf is a context-indexed set of data on the sorts of a theory. The
canonical example is a representable presheaf, of the form
$\mathsf{T}(-,\mathtt{S})$, which indexes all terms of sort $\mathtt{S}$. The
Yoneda embedding
$y:\mathsf{T}\to\mathscr{P}(\mathsf{T})::\mathtt{S}\mapsto\mathsf{T}(-,\mathtt{S})$
preserves limits and internal homs.

A subobject classifier is an object $\Omega$ with a natural isomorphism
$\mathrm{c}:\mathsf{T}(-,\Omega)\simeq\mathrm{Sub}(-):\mathsf{T}^{\mathsf{op}}\to\mathrm{Pos}.$
We may denote $\Omega$ as $\mathsf{Prop}$; this is its role in the type
system: a predicate is a morphism $\varphi:A\to\Omega$, and the comprehension
of $\varphi$ is the subobject
$\mathrm{c}(\varphi)\;:=\;\\{a:A\;|\;\varphi(a)\\}\rightarrowtail A.$

A topos is a $\lambda$-theory with equality with a subobject classifier. For
presheaves, the hom and subobject classifier are defined
$[P,Q](\mathtt{S})=\mathscr{P}(\mathsf{T})(y(\mathtt{S})\times P,Q)$ and
$\Omega(\mathtt{S})=\\{\varphi\rightarrowtail y(\mathtt{S})\\}.$

The values of $\Omega$ can be understood as
$\Omega(\mathtt{S})\simeq\\{\text{sieves on }\mathtt{S}\\}.$ A sieve on
$\mathtt{S}$ is a set of morphisms into $\mathtt{S}$ closed under
precomposition. A simple example is a principal sieve
$\langle\mathtt{f}\rangle:\Omega(\mathtt{T})$ generated by
$\mathtt{f}:\mathtt{S}\to\mathtt{T}$.

$\langle\mathtt{f}\rangle(\mathtt{R})=\\{t:\mathtt{R}\to\mathtt{T}\;|\;\exists
u^{\prime}\mathtt{R}\to\mathtt{S}.\;\mathtt{f}(u)=t\\}$

A sieve can be understood as a set of shapes of abstract syntax tree with
(sorted) holes for leaves, closed under substitution. These are the basic
objects of reasoning in native type theory, as they are predicates on
representable presheaves.

######  Example 9.

In the $\uprho\pi$-calculus (ex. 5) we can define a context
$c(n):\mathtt{P}\to\mathtt{P}$ which replicates processes on a name
$n:1\to\mathtt{N}$.

$\begin{array}[]{llcll}c(n)&:=\mathtt{in}(n,\lambda x.\\{\mathtt{out}(n,\ast
x)\;|\ast x\\})&&!(-)(n)&:=\mathtt{out}(n,\\{c(n)|-\\})\;|\;c(n).\end{array}$

One can check that $!(p)(n)\;\;\leadsto\;\;!(p)(n)\;|\;p$ for any process $p$.
The sieve $\langle!(-)(n)\rangle:\Omega(\mathtt{P})$ consists of processes
which replicate on the name $n$ by the above method.

For simpler formulae, we denote the values of a presheaf by
$A_{\\_}\mathtt{S}:=A(\mathtt{S})$, and the action of
$u:\mathtt{R}\to\mathtt{S}$ by $-\cdot u:=A(u):A(\mathtt{S})\to
A(\mathtt{R})$. For $\varphi:A\to\mathsf{Prop}$ we denote
$\varphi_{\\_}\mathtt{S}^{a}:=\varphi(\mathtt{S})(a)$; more generally for any
$p:P\to A$ we denote $p_{\\_}\mathtt{S}^{a}:=p_{\\_}\mathtt{S}^{-1}(a)$ as the
fiber over $a$ ($\S$3.2). Finally, sorts and term constructors are identified
with their images under $y$, so $\mathtt{S}$ will mean $y\mathtt{S}$ when
applicable.

###  3.1 The predicate fibration

For any $\lambda$-theory $\mathsf{T}$, there is a “category of predicates”
$\Omega\mathscr{P}(\mathsf{T})$ over $\mathscr{P}(\mathsf{T})$ where the fiber
over each presheaf is its poset of predicates. Quantification gives adjoints
to change-of-base between fibers; we show that moreover the domain is
cartesian closed, complete and cocomplete. The structure of this fibration
provides higher-order predicate logic of the presheaves on $\mathsf{T}$.

We use $\Omega^{A}$ to denote the poset of predicates $\varphi:A\to\Omega$,
ordered by entailment. The predicate functor of $\mathscr{P}(\mathsf{T})$ is
$\Omega^{(-)}:\mathscr{P}(\mathsf{T})^{\mathsf{op}}\to\mathrm{Pos}.$ For
$f:A\to B$, precomposition of predicates corresponds to preimage of
subobjects. This is written as substitution $\varphi[f]:=\Omega^{f}(\varphi)$.

Substitution can be understood as pattern-matching.

######  Example 10.

For a $\uprho\pi$-calculus predicate $\varphi:y(\mathtt{P})\to\mathsf{Prop}$,
substitution by $y(\mathtt{in}):y(\mathtt{N})\times
y([\mathtt{N},\mathtt{P}])\to y(\mathtt{P})$ is the query “inputting on what
name-context pairs yield property $\varphi$?”

$\varphi[\mathtt{in}]_{\\_}\mathtt{S}=\\{\mathtt{S}\vdash(n,\lambda
x.p):\mathtt{N},[\mathtt{N}\to\mathtt{P}]\;|\;\varphi(\mathtt{in}(n,\lambda
x.p))\\}$

Each poset $\Omega^{A}$ is in fact a complete Heyting algebra: meet and join
are intersection and union, $\top=A$ and $\bot=(\mathtt{S}\mapsto\emptyset)$,
implication is

$(\varphi\Rightarrow\psi)_{\\_}\mathtt{S}(a):=\;\;\Pi
u^{\prime}\mathtt{R}\to\mathtt{S}.\;\varphi_{\\_}\mathtt{R}(a\cdot
u)\Rightarrow\psi_{\\_}\mathtt{R}(a\cdot u)$

and negation is $\neg[\varphi]:=(\varphi\Rightarrow\bot$).

We can assemble the image of $\Omega^{(-)}$ into one category, with the
Grothendieck construction [18, 1.10].

######  Definition 11.

The _category of predicates_ of $\mathscr{P}(\mathsf{T})$, denoted
$\Omega\mathscr{P}(\mathsf{T})$, is defined as follows.

$\begin{array}[]{l@{\;\;}c@{\;\;}l}\text{Object}&\text{a pair }&\langle
A\;,\;\varphi:\Omega^{A}\rangle\\\ \text{Morphism}&\text{a pair }&f:\langle
A,\varphi\rangle\to\langle B,\psi\rangle\\\ &=&\langle f:A\to
B\;,\;\varphi\Rightarrow\psi[f]\rangle\\\ \text{Composition}&&f;g:\langle
A,\varphi\rangle\to\langle B,\psi\rangle\to\langle C,\chi\rangle\\\ &=&\langle
f;g:A\to C,\varphi\Rightarrow\psi[f]\Rightarrow\chi[g][f]\rangle\end{array}$

The projection
$\pi_{\\_}\Omega:\Omega\mathscr{P}(\mathsf{T})\to\mathscr{P}(\mathsf{T})$ is
the predicate fibration; the fiber over $A$ is $\Omega^{A}$, and the fiber
over $f:A\to B$ is $\Omega^{f}:\Omega^{B}\to\Omega^{A}$, known as a _change-
of-base functor_.

A fibration is a functor with a well-behaved notion of preimage, used in type
theory for indexing; a reference is [18, Ch. 1]. The predicate fibration is
highly structured: each change-of-base functor has adjoints which are
dependent sum and dependent product.

######  Proposition 12.

The projection
$\pi_{\\_}\Omega:\Omega\mathscr{P}(\mathsf{T})\to\mathscr{P}(\mathsf{T})$ has
indexed sums and products [18]: for each $f:A\to B$, the functor
$\Omega^{f}:\Omega^{B}\to\Omega^{A}$ has left and right adjoints
$\exists_{\\_}f\dashv\Omega^{f}\dashv\forall_{\\_}f$.

$\begin{array}[]{rlcrl}\exists_{\\_}f(\varphi)_{\\_}\mathtt{S}^{b}:=&\exists
a^{\prime}A_{\\_}\mathtt{S}.\;(f_{\\_}\mathtt{S}(a)=b)\land\varphi(a)&&\forall_{\\_}f(\varphi)_{\\_}\mathtt{S}^{b}:=&\forall(u^{\prime}\mathtt{R}\to\mathtt{S}).\forall
a^{\prime}A.\;(f_{\\_}\mathtt{R}(a)=b)\Rightarrow\varphi(a)\end{array}$

The left adjoint $\exists_{\\_}f$ is called direct image, because on
subobjects it is composition by $f$; we call the right adjoint
$\forall_{\\_}f$ secure image. While $\Omega^{f}$ is a morphism of complete
Heyting algebras, $\exists_{\\_}f$ and $\forall_{\\_}f$ are only morphisms of
join and meet semilattices, respectively.

######  Example 13.

Let $\mathsf{Th.Gph}\to\mathsf{T}$ be a $\lambda$-theory with a graph, and
$\varphi:\mathtt{V}\to\mathsf{Prop}$ be a predicate on terms. Then
$\varphi[s]:\mathtt{E}\to\mathsf{Prop}$ are rewrites with $\varphi($source$)$,
and $\exists_{\\_}{t}(\varphi[s])$ are the targets of these rewrites. Hence
there is a step-forward operation
$\mathsf{F}_{\\_}!:=[s];\exists_{\\_}t:[\mathtt{V},\mathsf{Prop}]\to[\mathtt{V},\mathsf{Prop}]$.

The secure step-forward is a more refined operation:
$\mathsf{F}_{\\_}*(\varphi):=\forall_{\\_}{t}(\varphi[s])$ determines the
terms $u$ for which $(t\leadsto u)\Rightarrow\varphi(t)$. For security
protocols, this can filter agents by past behavior.

The change-of-base adjoints satisfy the Beck–Chevalley condition: this means
that quantification commutes with substitution, and implies that
$\Omega^{(-)}:\mathscr{P}(\mathsf{T})^{\mathsf{op}}\to\mathrm{CHA}$ is a
first-order hyperdoctrine [21] and a higher-order fibration [18, section 5.3].

This concept leaves implicit additional structure: there is also an internal
hom of predicates.

######  Proposition 14.

$\Omega\mathscr{P}(\mathsf{T})$ is cartesian closed, as is $\pi_{\\_}\Omega$.
Let $\varphi:A\to\mathsf{Prop}$, $\psi:B\to\mathsf{Prop}$, and let
$\langle\pi_{\\_}1,\pi_{\\_}2,ev\rangle:A\times[A,B]\to A\times[A,B]\times B.$
Then $[\varphi,\psi]:[A,B]\to\mathsf{Prop}$ is defined
$[\varphi,\psi]:=\forall_{\\_}{\pi_{\\_}2}(\varphi[\pi_{\\_}1]\Rightarrow\psi[ev])$.
This determines maps $f:A\to B$ for which $\varphi(a)\Rightarrow\psi(f(a))$.

The cartesian closed structure of $\Omega\mathscr{P}(\mathsf{T})$ is
significant, because the category of predicates on $\mathsf{T}$ is itself a
$\lambda$-theory, the refinement of the language. We explore applications in
$\S$5.

######  Definition 15.

The predicate theory of $\mathsf{T}$, denoted $\omega\mathsf{T}$, is the
pullback of the predicate fibration along the embedding
$y:\mathsf{T}\to\mathscr{P}(\mathsf{T})$; it is a $\lambda$-theory fibered
over $\mathsf{T}$.

Note — We emphasize the idea of having “lifted” the language by an abuse of
notation: for any operation $\mathtt{f}:\mathtt{S}\to\mathtt{T}$, we may
denote
$\exists_{\\_}{y(\mathtt{f})}:[y(\mathtt{S}),\mathsf{Prop}]\to[y(\mathtt{T}),\mathsf{Prop}]$
simply by $\mathtt{f}$, and $\forall_{\\_}{y(\mathtt{f})}$ by
$\mathtt{f}_{\\_}*$.

######  Example 16.

As an example of contexts which ensure implications across substitution, we
can construct the “magic wand” of separation logic [25]. Let
$\mathsf{T}_{\\_}h$ be the theory of a commutative monoid $(H,\cup,e)$, plus
constructors for the elements of a heap. If we define
$(\varphi\mbox{--\\!$\ast$}\psi):=[\varphi,\psi][\lambda x.x\cup-]$, then
$(\varphi\mbox{--\\!$\ast$}\psi)(h_{\\_}1)$ means that
$\varphi(h_{\\_}2)\Rightarrow\psi(h_{\\_}1\cup h_{\\_}2)$.

There is a more expressive way to form hom predicates, which provides
predicate binding.

######  Proposition 17.

Let $A,B:\mathscr{P}(\mathsf{T})$, and let
$\mathsf{L}_{\\_}{A,B}:[[A,B],\mathsf{Prop}]\to[[A,\mathsf{Prop}],[B,\mathsf{Prop}]]$
be curried evaluation. There is a right adjoint which we call reification. The
predicate $\mathsf{R}_{\\_}{A,B}(F)$, denoted $\chi.F$, determines $f:[A,B]$
whose images are contained in those of $F$:

$[\chi.F]_{\\_}\mathtt{S}(f)\;=\;\Pi\chi^{\prime}[A\to\mathsf{Prop}].\;\exists_{\\_}f(y(\mathtt{S})\times\chi)\Rightarrow
F(\chi).$

The authors do not know of existing literature on this right adjoint; we do
not yet how it is connected with dependent products of
$\mathscr{P}(\mathsf{T})$. We know it is highly expressive: using reification,
separation logic can be generalized from pairs to functions of predicates. We
do not know if this has been studied.

In addition, the category of predicates has all limits and colimits, by a
result of [35]. These can be used to form modalities, inductive and
coinductive types, and more.

######  Proposition 18.

$\Omega\mathscr{P}(\mathsf{T})$ is complete and cocomplete, and
$\pi_{\\_}\Omega$ preserves limits and colimits. They are computed pointwise;
letting $\pi,\iota$ represent the cone and cocone:

$\mathrm{lim}_{\\_}i\langle
A_{\\_}i,\varphi_{\\_}i\rangle=\langle\mathrm{lim}_{\\_}i(A_{\\_}i),\mathrm{lim}_{\\_}i(\Omega^{\pi_{\\_}i}\varphi_{\\_}i)\rangle\quad\quad\mathrm{colim}_{\\_}i\langle
A_{\\_}i,\varphi_{\\_}i\rangle=\langle\mathrm{colim}_{\\_}i(A_{\\_}i),\mathrm{colim}_{\\_}i(\Sigma_{\\_}{\iota_{\\_}i}\varphi_{\\_}i)\rangle.$

To summarize the rich structure present, we allude to a term from category
theory: a cosmos is a monoidal closed category which is complete and
cocomplete [34].

######  Proposition 19.

The predicate fibration
$\pi_{\\_}\Omega:\Omega\mathscr{P}(\mathsf{T})\to\mathscr{P}(\mathsf{T})$ is a
higher-order fibration which is cosmic: cartesian closed, complete and
cocomplete.

###  3.2 The codomain fibration

Predicates $\varphi:A\to\mathsf{Prop}$ correspond to subobjects
$\mathrm{c}(\varphi)\rightarrowtail A$. More generally, any $p:P\to A$ can be
understood as a dependent type. This generalizes subsets to indexed sets:
fibers over $A$ are expanded from truth values to sets, denoted
$p_{\\_}\mathtt{S}^{a}$ or $P_{\\_}\mathtt{S}[a]$, and fibers over
$\mathscr{P}(\mathsf{T})$ are expanded from posets to categories.

Each term constructor $\mathtt{f}:\mathtt{S}\to\mathtt{T}$ defines a dependent
type $y(\mathtt{f}):y(\mathtt{S})\to y(\mathtt{T})$, still denoted
$\mathtt{f}$. Its terms are like the principal sieve
$\langle\mathtt{f}\rangle:y(\mathtt{T})\to\mathsf{Prop}$, except that the
substituted terms $u$ are recorded.

$\mathtt{f}_{\\_}\mathtt{R}[t]=\Sigma
u^{\prime}\mathtt{R}\to\mathtt{S}.\;(f(u)=t)$

######  Proposition 20.

Let $\mathrm{CCT}$ be the category of complete and cocomplete toposes and
logical functors. There is a functor
$\Delta:\mathscr{P}(\mathsf{T})^{\mathsf{op}}\to\mathrm{CCT}$ that maps $A$ to
$\mathscr{P}(\mathsf{T})/A$ and $f:A\to B$ to pullback.

We can denote pullback by substitution,
$p[f]_{\\_}\mathtt{S}^{a}:=\Delta^{f}(p)_{\\_}\mathtt{S}^{a}=p_{\\_}\mathtt{S}^{f_{\\_}\mathtt{S}(a)}=p_{\\_}\mathtt{S}^{-1}(f_{\\_}\mathtt{S}(a))$.
Dependent sum $\Sigma_{\\_}f$ and dependent product $\Pi_{\\_}f$ have the same
formulae as predicates, and they commute with substitution.

$\begin{array}[]{rlcrl}\Sigma_{\\_}f(\varphi)_{\\_}\mathtt{S}^{b}:=&\Sigma
a^{\prime}A_{\\_}\mathtt{S}.\;(f_{\\_}\mathtt{S}(a)=b)\land\varphi(a)&&\Pi_{\\_}f(\varphi)_{\\_}\mathtt{S}^{b}:=&\Pi(u^{\prime}\mathtt{R}\to\mathtt{S}).\Pi
a^{\prime}A.\;(f_{\\_}\mathtt{R}(a)=b)\Rightarrow\varphi(a)\end{array}$

The Grothendieck construction of $\Delta$ determines a category over
$\mathscr{P}(\mathsf{T})$.

######  Definition 21.

The _category of dependent types_ of $\mathscr{P}(\mathsf{T})$, denoted
$\Delta\mathscr{P}(\mathsf{T})$, is equivalent to the arrow category of
$\mathscr{P}(\mathsf{T})$. The codomain fibration is the projection
$\pi_{\\_}\Delta:\Delta\mathscr{P}(\mathsf{T})\to\mathscr{P}(\mathsf{T}).$

######  Proposition 22.

The codomain fibration $\pi_{\\_}\Delta$ is a closed comprehension category
[18, Sec. 10.5] which is cosmic, i.e. cartesian closed, complete and
cocomplete.

The two fibrations are connected by an adjunction: comprehension interprets a
predicate as a dependent type, and factorization takes a dependent type to its
image predicate. This fibered adjunction is a higher-order dependent type
theory [18, Sec. 11.6].

${{\Omega\mathscr{P}(\mathsf{T})}}$${{\Delta\mathscr{P}(\mathsf{T})}}$${{\mathscr{P}(\mathsf{T})}}$$\scriptstyle{\mathrm{c}}$$\scriptstyle{\mathrm{i}}$$\scriptstyle{\pi_{\\_}\Delta}$$\scriptstyle{\pi_{\\_}\Omega}$${\dashv}$

We denote by $\mathrm{HDT}\Sigma$ the 2-category of higher-order dependent
type theories, a full sub-2-category of adjunctions in the 2-category of
fibrations.

The reason for the notation $\mathrm{HDT}\Sigma$ is as follows. Recall that
the 2-functor

$\mathscr{P}:\lambda\mathrm{Thy}_{\\_}=^{\mathsf{op}}\to\mathrm{Topos}$

sends $\mathsf{F}:\mathsf{S}\to\mathsf{T}$ to precomposition by $\mathsf{F}$,
$\mathscr{P}(\mathsf{F}):=-\circ\mathsf{F}:[\mathsf{T}^{\mathsf{op}},\mathrm{Set}]\to[\mathsf{S}^{\mathsf{op}},\mathrm{Set}]$.
This functor preserves pullbacks, inducing morphisms of predicate and codomain
fibrations; but it is not locally cartesian closed, nor does it preserve the
subobject classifier. It is future work to consider theory translations for
which $\mathscr{P}(\mathsf{F})$ preserves $\Pi$ and $\Omega$ [19, C 3].

######  Theorem 23.

The construction which sends a topos to its internal language
$\mathscr{L}(\mathscr{E})=\langle\pi_{\\_}{\Omega\mathscr{E}},\pi_{\\_}{\Delta\mathscr{E}},\mathrm{i}_{\\_}\mathscr{E},\mathrm{c}_{\\_}\mathscr{E}\rangle$,
consisting of the predicate and codomain fibrations connected by the image-
comprehension adjunction, defines a 2-functor
$\mathscr{L}:\mathrm{Topos}\to\mathrm{HDT}\Sigma$.

##  4 Native Type Theory

We present the native type system $\mathscr{L}\mathscr{P}(\mathsf{T})$ of a
$\lambda$-theory with equality $\mathsf{T}$ ($\S$2). As
$y:\mathsf{T}\to\mathscr{P}(\mathsf{T})$ is full and faithful,
$\mathscr{L}\mathscr{P}(\mathsf{T})$ is a conservative extension of
$\mathsf{T}$.

The system is higher-order dependent type theory [18, Sec. 11.5]
“parameterized” by $\mathsf{T}$. We do not present Equality and Quotient
types. We encode Subtyping, Hom, Reification, and Inductive types, which we
use in applications.

The type system has predicates
$\mathsf{x^{\prime}\Gamma\vdash\varphi:\mathsf{Prop}}$ and types
$\mathsf{x^{\prime}\Gamma\vdash A:\mathsf{Type}}$, interpreted as
$\varphi:\mathsf{\Gamma}\to\Omega$ and $\mathsf{p:A\to\Gamma}$. A term
judgement is of the form $\mathsf{x^{\prime}\Gamma,a^{\prime}A\vdash N:B[M]}$,
interpreted as a morphism $\mathsf{\langle
M,N\rangle:(A\to\Gamma)\to(B\to\Delta)}$ in the total category of the codomain
fibration.

For details on the semantic interpretation of the type system, in particular
handling coherence when interpreting substitution as pullback, see Awodey’s
natural models [10].

We present the type system as generated from the $\lambda$-theory
$\mathsf{T}$, so a programmer can start in the ordinary language and use the
ambient logical structure as needed.

  * $\mathsf{Y}$

Representables are given in the type system as axioms.

$\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}\quad\quad\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}\quad\quad\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}$

The type $\mathsf{y}\mathtt{S}$ indexes all terms of sort $\mathtt{S}$.
Because the Yoneda embedding preserves limits and internal hom, we have
$\mathsf{y}(\mathtt{S}_{\\_}1,\mathtt{S}_{\\_}2)=(\mathsf{y}\mathtt{S}_{\\_}1,\mathsf{y}\mathtt{S}_{\\_}2)$
and
$\mathsf{y}[\mathtt{S}\to\mathtt{T}]=[\mathsf{y}\mathtt{S}\to\mathsf{y}\mathtt{T}]$.

  * $\mathsf{\Sigma}$

Dependent Pair is an indexed sum generalizing existential quantification.

$\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}\quad\quad\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}$
$\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}$
$\begin{array}[]{lcll}\mathsf{\langle M,N\rangle\;\mathsf{as}\;\langle
a,u\rangle\;\mathsf{in}\;Q}&=&\mathsf{Q[M/a,N/u]}&(\mathsf{\Sigma}_{\\_}\beta)\\\
\mathsf{P\;\mathsf{as}\;\langle a,u\rangle\;\mathsf{in}\;Q[\langle
a,u\rangle/z]}&=&\mathsf{Q[P/z]}&(\mathsf{\Sigma}_{\\_}\eta)\end{array}$

  * $\mathsf{\Pi}$

Dependent Function is an indexed product generalizing universal
quantification.

$\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}\quad\quad\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}$
$\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}\quad\quad\begin{array}[]{lcll}\mathsf{(\lambda
x^{\prime}A.t)(a)}&=&\mathsf{t(a)}&(\mathsf{\Pi}_{\\_}\beta)\\\
\mathsf{f}&=&\mathsf{\lambda
x^{\prime}A.f}&(\mathsf{\Pi}_{\\_}\eta)\end{array}$

We derive existential $\exists$ from $\mathsf{\Sigma}$ and universal $\forall$
from $\mathsf{\Pi}$ by image factorization. The rest of predicate logic
$\bot,\top,\lor,\land,\Rightarrow,\neg$ is also encoded in terms of
$\mathsf{\Sigma}$ and $\mathsf{\Pi}$.

  * $\mathsf{\\{\\}}$

Comprehension converts a predicate to the type of its satisfying terms. The
rules which convert a type to its image predicate can be derived from
$\mathsf{\Sigma}$ and Equality.

$\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}\quad\quad\quad\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}$
$\begin{minipage}{86.72267pt}
\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}
\end{minipage}\qquad\begin{minipage}{86.72267pt}
$\begin{array}[]{ll}\mathsf{\mathsf{o}(\mathsf{i}(M))=M}&(\mathsf{c}_{\\_}\beta)\\\
\mathsf{\mathsf{i}(\mathsf{o}(N))=N}&(\mathsf{c}_{\\_}\eta)\end{array}$
\end{minipage}\quad\quad\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}$

  * $\subseteq$

Subtyping of predicates is defined $(\varphi\subseteq\psi):=\mathsf{\forall
a^{\prime}A.\;\varphi(a)\Rightarrow\psi(a)}.$

  * $\to$

Hom type (def. 14) of $\mathsf{A_{\\_}1\vdash B_{\\_}1:\mathsf{Type}}$ and
$\mathsf{A_{\\_}2\vdash B_{\\_}2:\mathsf{Type}}$ is defined $\mathsf{\Pi
x^{\prime}A_{\\_}1}.\;\mathsf{B_{\\_}1[\pi]\Rightarrow B_{\\_}2[ev]}$.

  * $\mathsf{R}$

Reification (def. 17) $\mathsf{\chi.F:[A,B]\to\mathsf{Prop}}$ is defined
$\mathsf{\Pi\varphi^{\prime}[A\to\mathsf{Prop}]}.\;\mathsf{\varphi\Rightarrow
F(\varphi[-])}$.

  * $\mu$

Inductive type of
$\mathsf{F}:[\mathsf{A},\mathsf{Prop}]\to[\mathsf{A},\mathsf{Prop}]$: the
least and greatest fixed points are defined

$\begin{array}[]{rcl}\mathsf{\mu\varphi.F(\varphi)}&:=&\mathsf{\exists\varphi^{\prime}[A,\mathsf{Prop}].\;(\varphi\subseteq
F(\varphi))\Rightarrow\varphi}\\\
\mathsf{\nu\varphi.F(\varphi)}&:=&\mathsf{\forall\varphi^{\prime}[A,\mathsf{Prop}].\;(F(\varphi)\subseteq\varphi)\Rightarrow\varphi}\end{array}$

These are used to form data structures and modalities; we can generalize to
W-types [30].

These rules constitute the native type system
$\mathscr{L}\mathscr{P}(\mathsf{T})$, abridged for a first presentation. We
include rules for functoriality, so that translations of $\lambda$-theories
induce translations of native type systems.

  * $\mathsf{F}$

Translation is given by precomposing types and “whiskering” terms.

$\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}\quad\quad\quad\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}$

We add rules that
$\mathsf{F}^{\ast}:\mathscr{P}(\mathsf{T}_{\\_}2)\to\mathscr{P}(\mathsf{T}_{\\_}1)$
preserves substitution, dependent pair, and co/limits.

To further research we leave the rules for the colax preservation of
$\mathsf{\Pi}$ and $\mathsf{Prop}$, and the rules for the two covariant
functors
$\mathrm{Lan}_{\\_}\mathsf{F},\mathrm{Ran}_{\\_}\mathsf{F}:\mathscr{P}(\mathsf{T}_{\\_}1)\to\mathscr{P}(\mathsf{T}_{\\_}2)$
given by left and right Kan extension.

As a small demonstration of the type system, suppose we have a program
$\mathtt{f}:\mathtt{S}\to\mathtt{T}$, and we want to construct the predicate
which checks whether a term of sort $\mathtt{T}$ has been processed by
$\mathtt{f}$.

$\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}\quad\quad\quad\quad\box_set_eq_clear:cN{g__ebproof_box_1}\hbox{$\vbox{}$}$

We can then write protocols based on this precondition in the native type
system.

##  5 Applications

Native type systems are highly expressive and versatile. We demonstrate a few
small examples. Notation is simplified by identifying sorts and constructors
of $\mathsf{T}$ with their image in $\mathscr{P}(\mathsf{T})$.

### Behavior subsystems

Let $\mathsf{Th.Gph}\to\mathsf{T}$ be a $\lambda$-theory with internal graph
$\mathtt{G}=\langle s,t\rangle:\mathtt{E}\to\mathtt{V},\mathtt{V}$. Then
$\mathsf{y}\mathtt{G}:\mathscr{P}(\mathsf{T})$ is the (dependent) type of
rewrites over terms. The fiber over each pair is the set of rewrites between
terms.

$\mathtt{S},a^{\prime}\mathtt{V},b^{\prime}\mathtt{V}\vdash\mathtt{G}(a,b):\mathsf{Type}\quad\quad\quad\quad\mathtt{G}(a,b)=\\{\mathtt{S}\vdash
e:a\leadsto b\\}$

This object is the space of all computations in language $\mathsf{T}$. The
native type system can be used to construct predicates which specify subgraphs
of computations.

######  Example 24.

Let $\mathsf{Th.Gph}\to\mathsf{Th}.\uprho\pi$ be the structured
$\lambda$-theory of the $\uprho\pi$-calculus (ex. 5). In
$\mathscr{L}\mathscr{P}(\mathsf{Th}.\uprho\pi)$, suppose we have a name
predicate $\alpha:\mathtt{N}\to\mathsf{Prop}$, a process predicate
$\varphi:\mathtt{P}\to\mathsf{Prop}$, and a constructor of predicates
$F:[\mathtt{N}\to\mathsf{Prop}]\to[\mathtt{P}\to\mathsf{Prop}]$. Then
$\mathtt{comm}(\alpha,\varphi,\chi.F):[\mathtt{E},\mathsf{Prop}]$ determines
communications

  * •

on channels in namespace $\alpha$

  * •

sending data in codespace $\varphi$

  * •

and continuing in contexts $\lambda x.c:[\mathtt{N},\mathtt{P}]$ such that
$\chi(@p)\Rightarrow F(\chi)(c[@p/x])$.

This provides highly expressive specification and conditioning of
communication on a network. In particular, these predicates could be used to
analyze, distribute, or enforce rules for execution on a public computing
platform, such as a blockchain.

### Modalities

We can express temporal modalities to reason about past and future behavior.
Applying the “step” operators of ex. 13 to a predicate
$\varphi:\mathtt{V}\to\mathsf{Prop}$ on terms, $\mathsf{B}_{\\_}!(\varphi)$
are terms which possibly rewrite to $\varphi$, and
$\mathsf{B}_{\\_}*(\varphi)$ are terms which necessarily rewrite to $\varphi$.
By iterating, we can form each kind of modality.

$\begin{array}[]{ll@{\quad}lcll@{\quad}l}\mathsf{B}_{\\_}!^{\circ}(\varphi):=&\exists
n^{\prime}\mathbb{N}.\mathsf{B}_{\\_}!^{n}(\varphi)&\text{can become
}\varphi&&\mathsf{B}_{\\_}!^{\bullet}(\varphi):=&\forall
n^{\prime}\mathbb{N}.\mathsf{B}_{\\_}!^{n}(\varphi)&\text{always can become
}\varphi\\\ \mathsf{B}_{\\_}*^{\circ}(\varphi):=&\exists
n^{\prime}\mathbb{N}.\mathsf{B}_{\\_}*^{n}(\varphi)&\text{will become
}\varphi&&\mathsf{B}_{\\_}*^{\bullet}(\varphi):=&\forall
n^{\prime}\mathbb{N}.\mathsf{B}_{\\_}*^{n}(\varphi)&\text{always
}\varphi\end{array}$

Similarly for $\mathsf{F}$, we can condition past behavior. These modalities
can also be restricted to subsystems.

######  Example 25.

We can use modalities to express system requirements, such as the capacity to
receive and process input on certain channels, or the guarantee to only
communicate on certain channels.

$\begin{array}[]{llcll}\mathsf{live}(\alpha):=&\mathsf{B}_{\\_}*^{\bullet}(\mathtt{in}(\alpha,[\mathtt{N}\to\mathtt{P}])\;|\;\mathtt{P})&&\mathsf{safe}(\alpha):=&\mathsf{B}_{\\_}*^{\bullet}(\neg[\mathtt{in}(\neg[\alpha],[\mathtt{N}\to\mathtt{P}])\;|\;\mathtt{P}])\end{array}$

By proving $\mathtt{in}(n,\lambda
x.c):\mathtt{in}(\mathtt{N},\chi.\mathsf{safe})$, we know the program will be
secure on the channel it receives.

### Behavioral equivalence

Our rewrite graphs are deterministic, because each edge specifies all data in
the term vertices. In operational semantics, rewrites are “silent reductions”
which occur in a closed system, while transitions allow for interaction with
the environment. This can be expressed using substitution as pattern-matching,
to construct a nondeterministic labelled transition system in which to derive
behavioral equivalence.

######  Example 26.

Processes in the $\uprho\pi$-calculus interact in parallel $-|-$. The basic
actions are input and output. To construct the transition system of these
observable behaviors, we define interaction contexts.

$\mathsf{obs}:=[\lambda x.x]\lor[\lambda
x.(\mathtt{in}(\mathtt{N},\mathtt{N}\to\mathtt{P})\;|\;x)]\lor[\lambda
x.(\mathtt{out}(\mathtt{N},\mathtt{P})\;|\;x)]:[\mathtt{P}\to\mathtt{P}]\to\mathsf{Prop}$

We can then define the labelled transition system
$\mathsf{act}:\mathtt{P},[\mathtt{P}\to\mathtt{P}],\mathtt{P}\to\mathsf{Prop}$
as

$p^{\prime}\mathtt{P},\lambda
x.c^{\prime}[\mathtt{P}\to\mathtt{P}],q^{\prime}\mathtt{P}\vdash\mathsf{act}(p,\lambda
x.c,q):=\mathtt{G}(ev[p,\mathsf{obs}(\lambda x.c)],q).$

Hence the predicate which is usually written as $p\xrightarrow[]{\lambda
x.c}q$, meaning “substituting $p$ into $c$ rewrites to $q$”, we define to be
$\exists e:\mathtt{G}.\;e:c[p/x]\leadsto q$. We can now construct new
modalities relative to this observational graph, denoted with
$(-)_{\\_}\mathsf{act}$.

From this relation, many kinds of behavioral equivalence can be written
explicitly as types. For example, bisimulation is the inductive type
$\mathsf{Bisim}:=\mu\varphi.\mathsf{S}(\varphi)$ for

$\begin{array}[]{lcl}\mathsf{S}(\varphi)(p,q)&:=&\forall
y^{\prime}\mathtt{P}.\;\forall\lambda
x.c^{\prime}[\mathtt{P},\mathtt{P}].\;\mathsf{act}(p,\lambda
x.c,y)\Rightarrow\exists z^{\prime}\mathtt{P}.\;\mathsf{act}(q,\lambda
x.c,z)\land\varphi(y,z)\;\land\\\ &&\forall
z^{\prime}\mathtt{P}.\;\forall\lambda
x.c^{\prime}[\mathtt{P},\mathtt{P}].\;\mathsf{act}(q,\lambda
x.c,z)\Rightarrow\exists y^{\prime}\mathtt{P}.\;\mathsf{act}(p,\lambda
x.c,y)\land\varphi(y,z)\end{array}$

By constructing bisimilarity as a native type, we can reason up to behavioral
equivalence.

### Refined binding

Hom types provide refined binding: using predicates to condition what can be
substituted into a context. To do this, we restrict rewrite rules to require
that a term satisfies the predicate which the context binds.

######  Example 27.

In the $\uprho\pi$-calculus, an input process $\mathtt{in}(n,\lambda x.c)$
receives whatever is sent on the name $n$. We can refine input to receive only
data which satisfies a predicate.

Consider the predicate theory (def. 15) of the $\uprho\pi$-calculus. For each
namespace $\alpha$, define

$\mathtt{comm}_{\\_}\alpha:\mathtt{N},\alpha[@],[\alpha\to\mathtt{P}]\to\mathtt{E}\quad\quad\mathtt{comm}_{\\_}\alpha(n,p,\lambda
x.c):\mathtt{out}_{\\_}\alpha(n,p)|\mathtt{in}_{\\_}\alpha(n,\lambda
x.c)\leadsto c[@p/x]$

where $\alpha[@]$ is the preimage of $\alpha$ under
$@:\mathtt{P}\to\mathtt{N}$. This extends to polyadic communication.

The refinement of the $\uprho\pi$-calculus is defined to be the subtheory
$\uprho\pi_{\\_}\omega\subset\omega\mathsf{Th}.\uprho\pi$ in which the only
rewrite constructors are $\mathtt{comm}_{\\_}\alpha$ for each namespace. In
this theory,
$\mathtt{in}_{\\_}\alpha:\mathtt{N},[\alpha\to\mathtt{P}]\to\mathtt{P}$
constructs processes which only receive data on $\alpha$.

The namespace $\alpha:\mathtt{N}\to\mathsf{Prop}$ could be a predicate on
structured data, a set of trusted addresses, or the implementations of an
algorithm. Then $\mathtt{in}(n,\lambda x^{\prime}\alpha.p)$ can be understood
as a query for $\alpha$. In the refined language, we can search by both
structure and behavior.

### Reasoning about contexts

A ubiquitous question in software is “what contexts ensure this implication?”
For example, “where can this protocol be executed without security leaks?” Hom
types provide this expressive power for reasoning contextually in codebases.

By composing the hom type with modalities, we can extend contextual reasoning
over term behavior. In particular,
$\varphi\rhd\psi:=[\varphi,\mathsf{B}^{\circ}_{\\_}*(\psi)]$ are contexts for
which substituting $\varphi$ can eventually lead to some condition, desired or
otherwise.

######  Example 28.

An arrow can be used to detect security leaks: given a trusted channel
$a:\mathtt{N}$ and an untrusted $n:\mathtt{N}$, then the following program
will not preserve safety on $a$.

$\lambda p.(p\;|\;\mathtt{out}(a,\mathtt{in}(n,\lambda
x.c))):\mathsf{safe}(a)\rhd\neg[\mathsf{safe}](a)$

We can similarly detect if a program may not remain single-threaded. Let
$\mathsf{s.thr}:=\neg[\mathtt{0}]\land\neg[\neg[\mathtt{0}]\;|\;\neg[\mathtt{0}]]$.
Then

$\lambda
p.\mathtt{out}(a,(p\;|\;q)):\mathsf{s.thr}\rhd_{\\_}\mathsf{act}\neg[\mathsf{s.thr}]$

where $\rhd_{\\_}\mathsf{act}$ is the arrow for the $\mathsf{act}$ transition
system (ex. 26).

In this way, the process of finding bugs can be automated as a form of type-
checking. The query time depends only on the system complexity and the
efficiency of the type checker.

These kind of predicates in the $\uprho\pi$-calculus have been studied for
object capabilities [28], advocating for better security by determining
authority purely through object references.

######  Example 29.

A key concept in concurrency is that of a race condition, in which multiple
communications on one channel are possible simultaneously.

$\begin{array}[]{ll}\mathsf{race.out}&:=\exists
n:\mathtt{N}.\;\mathtt{out}(n,\mathtt{P})\;|\;\mathtt{out}(n,\mathtt{P})\;|\;\mathtt{in}(n,\mathtt{N}.\mathtt{P})\;|\;\mathtt{P}\end{array}$

We can use native types to design algorithms which identify and manage these
conditions. Let $\mathtt{comm}(n):=\lambda
p.(p\;|\;s(\mathtt{comm}(n,\mathtt{P},\mathtt{N}\to\mathtt{P})))$, contexts
with potential communication on $n$.

$\begin{array}[]{lclclcl}\mathtt{comm}(n)&\subseteq&[\mathtt{out}(n,\mathtt{P}),\mathsf{race.out}]&&(\mathtt{comm}(n)\;|\;\mathtt{out}(n,\mathtt{P}))&\subseteq&\mathsf{race.out}\end{array}$

This is useful especially in applications such as blockchain.

### Translating across language paradigms

The construction of native type systems is functorial, allowing us to reason
across translations. We sketch a simple example of the benefits of relating
across programming paradigms.

We give a translation $\tau:\mathsf{Th.N}\lambda\to\mathsf{Th}.\pi$ from the
name-passing $\lambda$-calculus into the $\pi$-calculus.

######  Example 30.

Name-passing $\lambda$-calculus [12] (abridged)

$\begin{array}[]{rlcrlcrl}\mathtt{V}&\text{variables}&&\mathtt{T}&\text{terms}&&\mathtt{E}&\text{rewrites
of terms}\;(+\mathsf{Th.Cat})\\\ \end{array}$
$\begin{array}[]{rlcrlcrl}\mathtt{lam}:&[\mathtt{V}\to\mathtt{T}]\to\mathtt{T}&&\mathtt{var}:&\mathtt{V}\to\mathtt{T}&&\mathtt{C}:&\mathtt{V},\mathtt{T},\mathtt{T}\to\mathtt{T}\\\
\mathtt{app}:&\mathtt{T},\mathtt{V}\to\mathtt{T}&&\mathtt{def}:&\mathtt{T},[\mathtt{V}\to\mathtt{T}]\to\mathtt{T}\\\
\end{array}$
$\begin{array}[]{rlcrl}\beta:&[\mathtt{V}\to\mathtt{T}],\mathtt{V}\to\mathtt{E}&&\beta(Q,y):&\mathtt{app}(\mathtt{lam}(Q),y)\leadsto
Q(y)\\\
\phi:&\mathtt{V},\mathtt{T},\mathtt{T}\to\mathtt{E}&&\phi(x,Q):&\mathtt{C}(x,Q,\mathtt{var}(x))\leadsto
Q\end{array}$

The name-passing $\lambda$-calculus uses references to avoid copying large
data structures. It is a restriction of the $\lambda$-calculus in that terms
may only be applied to variables, while it is an enrichment in that it
introduces an environment $\mathtt{def}$ that records binding. There is also a
carrier $\mathtt{C}$, which serves to transport the recorded binding from its
declaration to its use.

The usual $\beta$ reduction splits into two reductions. The first, denoted
$\beta$, replaces variables in a term with other variables. The second,
denoted $\phi$ (for “fetch”), replaces a variable in head position with the
term to which it is bound in the environment.

######  Example 31.

Polyadic asynchronous $\pi$-calculus [31] (abridged)

$\begin{array}[]{rlcrlcrl}\mathtt{N}&\text{names}&&\mathtt{P}&\text{processes}&&\mathtt{E}&\text{rewrites
between processes}\;(+\mathsf{Th.Cat})\end{array}$
$\begin{array}[]{rlcrlc}\mathtt{0}:&1\to\mathtt{P}&&\mathtt{in}_{\\_}k:&\mathtt{N},[\mathtt{N}^{k}\to\mathtt{P}]\to\mathtt{P}\\\
-|-:&\mathtt{P},\mathtt{P}\to\mathtt{P}&&\mathtt{out}_{\\_}k:&\mathtt{N},\mathtt{N}^{k}\to\mathtt{P}\\\
!:&\mathtt{P}\to\mathtt{P}&&\nu:&[\mathtt{N}\to\mathtt{P}]\to\mathtt{P}&\mbox{syntactic
sugar: }\nu x.p\mbox{ means }\nu(\lambda x.p)\end{array}$
$\begin{array}[]{rlcrl}\mathtt{comm}_{\\_}k:&\mathtt{N},\mathtt{N}^{k},[\mathtt{N}^{k}\to\mathtt{P}]\to\mathtt{E}&&\mathtt{comm}_{\\_}k(n,\vec{a_{\\_}i},\lambda\vec{y_{\\_}i}.Q):&\mathtt{out}_{\\_}k(n;\vec{a_{\\_}i})|\mathtt{in}_{\\_}k(n,\lambda\vec{y_{\\_}i}.Q)\leadsto
Q[a_{\\_}i/y_{\\_}i]\\\
\mathtt{par}_{\\_}l:&\mathtt{E},\mathtt{P}\to\mathtt{E}&&\mathtt{par}_{\\_}l(\langle
p,e\rangle,q):&p|q\leadsto t(e)|q\\\
\nu_{\\_}\mathtt{e}:&[\mathtt{N}\to\mathtt{E}]\to\mathtt{E}&&\nu_{\\_}\mathtt{e}x.\rho:&\nu
x.s(\rho)\leadsto\nu x.t(\rho)\end{array}$

The $\pi$-calculus [29] models concurrent processes which compute via
communication, or the exchange of “names”. It is like the $\uprho\pi$-calculus
of this paper, without reflection and with two added constructors. The
replication operator $!$ makes infinitely many copies of a process. The $\nu$
operator introduces a new scope in which a fresh name has been made available
to the contained process. Scopes can expand via scope extrusion to absorb
other processes running in parallel with the scope.

######  Proposition 32.

There is a translation
$\llbracket-\rrbracket:\mathsf{Th}.\mathsf{N}\lambda\to\mathsf{Th}.\pi$ as
follows.

On sorts, $\llbracket\mathtt{V}\rrbracket=\mathtt{N}$,
$\llbracket\mathtt{T}\rrbracket=[\mathtt{N}\to\mathtt{P}]$, and
$\llbracket\mathtt{Hom}_{\\_}\mathtt{V}\rrbracket=\mathtt{Hom}_{\\_}\mathtt{P}$.

$\begin{array}[]{ll}\llbracket\mathtt{var}\rrbracket:\mathtt{N}\to[\mathtt{N}\to\mathtt{P}]\\\
\llbracket\mathtt{var}(x)\rrbracket=\lambda u.\mathtt{out}_{\\_}1(x,u)\\\ \\\
\llbracket\mathtt{lam}\rrbracket:[\mathtt{N}\to[\mathtt{N}\to\mathtt{P}]]\to[\mathtt{N}\to\mathtt{P}]\\\
\llbracket\mathtt{lam}(\lambda x.Q)\rrbracket=\lambda
u.\mathtt{in}_{\\_}2(u,\lambda x.\llbracket Q\rrbracket)\\\ \\\
\llbracket\mathtt{app}\rrbracket:[\mathtt{N}\to\mathtt{P}],\mathtt{N}\to[\mathtt{N}\to\mathtt{P}]\\\
\llbracket\mathtt{app}(Q,x)\rrbracket=\lambda u.\nu v.(\llbracket
Q\rrbracket(v)|\mathtt{out}_{\\_}2(v;x,u))\\\ \\\
\llbracket\mathtt{def}\rrbracket:[\mathtt{N}\to\mathtt{P}],[\mathtt{N}\to[\mathtt{N}\to\mathtt{P}]]\to[\mathtt{N}\to\mathtt{P}]\\\
\llbracket\mathtt{def}(Q,\lambda x.R)\rrbracket=\lambda u.\nu x.(\llbracket
R\rrbracket(u)|!\mathtt{in}_{\\_}1(x,\llbracket Q\rrbracket))\\\ \\\
\llbracket\mathtt{C}\rrbracket:\mathtt{N},[\mathtt{N}\to\mathtt{P}],[\mathtt{N}\to\mathtt{P}]\to[\mathtt{N}\to\mathtt{P}]\\\
\llbracket\mathtt{C}(x,Q,R)\rrbracket=\lambda u.(\llbracket
R\rrbracket(u)|\mathtt{in}_{\\_}1(x,\llbracket Q\rrbracket))\end{array}$

The translation preserves equations and rewrites. This induces a functor
$\mathscr{P}(\mathsf{Th}.\pi)\to\mathscr{P}(\mathsf{Th.N}\lambda)$, which in
turn induces a translation of the native type systems.

A $\pi$-calculus predicate $\varphi:\mathtt{P}\to\mathsf{Prop}$ contains
processes which may involve interaction between agents in a network that is
highly nondeterministic. By the translation, ir is mapped to a
$\lambda$-calculus predicate by precomposition; this has the effect of
restricting $\varphi$ to its “functional” processes.

Because $\lambda$-terms have no side-effects and execute deterministically,
restricting to functional terms can allow for significant optimization in
network computing; e.g. agents trying to reach consensus about side effects. A
compiler could recognize that a $\pi$-term can be implemented functionally and
run the consensus protocol on not the details of the execution but only the
result.

These few small examples are only a modest selection of the applications of
native type theory. Native types are practical because they are basic: they
are made by logic from languages we already use. We encourage the reader to
explore what native types can do for you.

##  6 Conclusion

Native type theory is a method to generate expressive type systems for a broad
class of languages. We believe that integrating native type systems in
software can help to provide a shared framework of higher-order reasoning in
everyday computing. Most of the tools necessary for implementation already
exist.

## References

  * [1]
  * [2] _Flow: A Static Type Checker for Javascript_.  Available at https://flow.org/.
  * [3] _Google Closure Compiler_.  Available at https://developers.google.com/closure/compiler.
  * [4] _Hoogle_.  Available at https://hoogle.haskell.org/.
  * [5] _K Framework_.  Available at http://www.kframework.org/.
  * [6] _KJS: A Complete Formal Semantics of JavaScript_.  Available at https://github.com/kframework/javascript-semantics.
  * [7] _Microsoft TypeScript_.  Available at https://www.typescriptlang.org/.
  * [8] _RChain_.  Available at https://www.rchain.coop/.
  * [9] Steve Awodey (2010): _Category Theory_ , 2nd edition.  Oxford University Press, Inc., USA.
  * [10] Steve Awodey (2016): _Natural models of homotopy type theory_.  Mathematical Structures in Computer Science 28(2), pp. 241–286, 10.1017/s0960129516000268.
  * [11] H. P. Barendregt (1984): _The Lambda Calculus: Its Syntax and Semantics_.  Elsevier.
  * [12] Gérard Boudol (1997): _The $\uppi$-calculus in direct style_.  In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL, ACM Press, 10.1145/263699.263726.
  * [13] John Cartmell (1986): _Generalised algebraic theories and contextual categories_.  Annals of Pure and Applied Logic 32, pp. 209–243, 10.1016/0168-0072(86)90053-9.  Available at https://www.sciencedirect.com/science/article/pii/0168007286900539.
  * [14] Thierry Coquand & Gérard Huet (1988): _The calculus of constructions_.  Information and Computation 76(2-3), pp. 95–120, 10.1016/0890-5401(88)90005-3.
  * [15] Roy L. Crole (1994): _Categories for Types_.  Cambridge University Press, 10.1017/CBO9781139172707.
  * [16] Robert Harper (2016): _Practical Foundations for Programming Languages_ , 2 edition.  Cambridge University Press, 10.1017/CBO9781316576892.
  * [17] André Hirschowitz, Tom Hirschowitz & Ambroise Lafont (2020): _Modules over monads and operational semantics_.  arXiv:2012.06530.
  * [18] B. Jacobs (1998): _Categorical Logic and Type Theory_.  Elsevier, Amsterdam, 10.1016/s0049-237x(98)x8028-6.
  * [19] Peter T. Johnstone (2002): _Sketches of an Elephant: A Topos Theory Compendium: 2 Volume Set_.  Oxford University Press UK.
  * [20] J. Lambek & P. J. Scott (1986): _Introduction to Higher Order Categorical Logic_.  Cambridge University Press, USA.
  * [21] F. William Lawvere (1969): _Adjointness in Foundations_.  dialectica 23(3-4), pp. 281–296, 10.1111/j.1746-8361.1969.tb01194.x.
  * [22] Saunders MacLane (1971): _Categories for the Working Mathematician_.  Springer New York, 10.1007/978-1-4612-9839-7.
  * [23] Saunders MacLane & Ieke Moerdijk (1994): _Sheaves in Geometry and Logic_.  Springer New York, 10.1007/978-1-4612-0927-0.
  * [24] Per Martin-Löf (1998): _An intuitionistic theory of types_.  In: Twenty Five Years of Constructive Type Theory, Oxford University Press, 10.1093/oso/9780198501275.003.0010.
  * [25] Paul-André Melliès & Noam Zeilberger (2015): _Functors are Type Refinement Systems_.  ACM SIGPLAN Notices 50(1), pp. 3–16, 10.1145/2775051.2676970.
  * [26] L. G. Meredith & Matthias Radestock (2005): _Namespace Logic: A Logic for a Reflective Higher-Order Calculus_.  In: Trustworthy Global Computing, Springer Berlin Heidelberg, pp. 353–369, 10.1007/1158085019.
  * [27] L.G. Meredith & Matthias Radestock (2005): _A Reflective Higher-order Calculus_.  Electronic Notes in Theoretical Computer Science 141(5), pp. 49–67, 10.1016/j.entcs.2005.05.016.
  * [28] Lucius G Meredith, Mike Stay & Sophia Drossopoulou (2013): _Policy as Types_.  arXiv:1307.7766.
  * [29] Robin Milner (1993): _The Polyadic $\uppi$-Calculus: a Tutorial_.  In: Logic and Algebra of Specification, Springer Berlin Heidelberg, pp. 203–246, 10.1007/978-3-642-58041-36.
  * [30] Ieke Moerdijk & Erik Palmgren (2000): _Wellfounded trees in categories_.  Annals of Pure and Applied Logic 104(1-3), pp. 189–218, 10.1016/s0168-0072(00)00012-9.
  * [31] Davide Sangiorgi (2000): _Communicating and Mobile Systems: the $\uppi$-calculus,_.  Science of Computer Programming 38(1-3), pp. 151–153, 10.1016/s0167-6423(00)00008-3.
  * [32] Dana S. Scott (1980): _Relating Theories of the Lambda Calculus_.  Available at https://www.andrew.cmu.edu/user/awodey/dump/Scott/ScottRelating.pdf.
  * [33] Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau & Théo Winterhalter (2019): _Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq_.  Proc. ACM Program. Lang. 4(POPL), 10.1145/3371076.
  * [34] Ross Street (1974): _Elementary cosmoi I_.  In Gregory M. Kelly, editor: Category Seminar, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 134–180, 10.1016/0022-4049(72)90019-9.
  * [35] Andrzej Tarlecki, Rod M. Burstall & Joseph A. Goguen (1991): _Some fundamental algebraic tools for the semantics of computation: Part 3. indexed categories_.  Theoretical Computer Science 91(2), pp. 239 – 264, 10.1016/0304-3975(91)90085-G.  Available at http://www.sciencedirect.com/science/article/pii/030439759190085G.
  * [36] D. Turi & G. Plotkin: _Towards a mathematical operational semantics_.  In: Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, IEEE Comput. Soc, 10.1109/lics.1997.614955.


# Bench-marking and Improving Arabic Automatic Image Captioning Through The
Use of Multi-task Learning Paradigm

Muhy Eddin Za’ter
University of Colorado Boulder
Boulder, Colorado
<EMAIL_ADDRESS>
Bashar Talafha
University of British Columbia
Vancouver
<EMAIL_ADDRESS>

###### Abstract

The continuous increase in the use of social media and the visual content on
the internet have accelerated the research in computer vision field in general
and the image captioning task in specific. The process of generating a caption
that best describes an image is a useful task for various applications such as
it can be used in image indexing and as a hearing aid for the visually
impaired. In recent years, the image captioning task has witnessed remarkable
advances regarding both datasets and architectures, and as a result, the
captioning quality has reached an astounding performance. However, the
majority of these advances especially in datasets are targeted for English,
which left other languages such as Arabic lagging behind. Although Arabic
language, being spoken by more than 450 million people and being the most
growing language on the internet, lacks the fundamental pillars it needs to
advance its image captioning research, such as benchmarks or unified datasets.
This work is an attempt to expedite the synergy in this task by providing
unified datasets and benchmarks, while also exploring methods and techniques
that could enhance the performance of Arabic image captioning. The use of
multi-task learning is explored, alongside exploring various word
representations and different features. The results showed that the use of
multi-task learning and pre-trained word embeddings noticeably enhanced the
quality of image captioning, however the presented results show that Arabic
captioning still lags behind when compared to the English language. The used
dataset and code are available at this link.

_K_ eywords Image Captioning $\cdot$ Arabic Language $\cdot$ Multi-task
Learning $\cdot$ Benchmark

##  1 Introduction

With the enormous surge of social media usage and the continued rapid increase
in the visual data generated by users from all around the world, the task of
image caption generation is gaining more and more attention and attracting a
considerable amount of research efforts from Natural Language Processing (NLP)
community and computer vision community [1]. Image captioning; known to be the
generation of meaningful captions for images, is a challenging task for
machine learning-based models, as they are required to combine both visual and
linguistic understanding that includes steps of reasoning to generate high
quality captions given an image[2]. However, despite the challenging nature of
the image captioning task, recent research endeavors were capable of achieving
considerable advances and achievements on this task. Inspired by the recent
advances in computer vision and machine translation, researchers have been
employing a variety of techniques and algorithms to enhance models performance
on image captioning. In addition to that, multiple datasets were developed and
collected for image captioning, which helped in accelerating and advancing the
research efforts in this field [3, 4, 5, 6, 7].

However, the overwhelming majority of the available datasets, algorithms, and
research efforts were directed toward English, which leaves other languages
lagging in this task. Arabic language for instance, is one of the majorly used
languages on the web, used by more than 450 million people, and also among
internet users, Arabic is the language with the fastest growth rate in the
last few years [8]. Despite these facts, the image captions generation was
untouched by the Arabic vision and NLP communities until recently with only a
few shy attempts to create datasets or to apply the advancement in other
languages on the Arabic language [9].

The Arabic language is known to be rich morphologically, with various distinct
dialects that significantly differ from the standard Arabic. These facts
impose new challenges for the Arabic NLP, that range from collecting datasets
or developing algorithms and models. These challenges are strongly reflected
in the task of image captioning, as the attempts so far to create Arabic image
captioning datasets are only at best humanly revised translations from the
English versions of the datasets such as Flicker30[10]. Also, except for one,
these datasets are not available for public, which leads to the absence of
reliable benchmarks and hence largely hinges any advancement in this task.

Multi-task learning is not a new idea in computer vision nor NLP, and it has
proved its effectiveness in tackling some models’ shortcomings and enhancing
their performance, also it has been known as a method to overcome the shortage
of labeled data for a specific task [11, 12]. Also, it has been utilized
earlier for better generation of image captions[13, 14]. Therefore, this work
attempts to utilize the paradigm of multi-task learning to overcome the
scarcity of image captioning data for Arabic, through using models with
superior performance on other tasks for different languages as a form of
inductive transfer in an attempt to enhance the results of Arabic Image
captioning. Also, the datasets developed by translating English captions will
be available for public to establish a benchmark for Arabic image captioning
to expedite synergy in this task. For the benchmark, this work preliminary
results for Arabic image captioning on the well-known translated datasets.

The rest of the document is divided as following. Section 2 lists the related
work that tackles Arabic image captioning or uses multi-task learning for
image captioning. Section 3 explains the used approach of multi-task learning
paradigm and the used datasets in this work. Section 4 illustrates the
experimental design in this work, while section 5 presents the results of
these experiments. Finally, section 6 concludes the work.

##  2 Related Work

There are few attempts for advancing research in Arabic image captioning
through creation of datasets and new algorithms, which will be listed in this
section. While also presenting work related to utilizing multi-task learning
in image captioning.

The work in the paper [15] in 2017 was the first work to use deep learning for
captioning in Arabic language. The approach consists of using deep belief
network and root words, in which tree based relations are used to generate
captions in the right order. This work was further followed by [16], in which
the author replaces the deep belief networks with recurrent neural networks.
However, the work proposed in this document uses the multi-task paradigm to
overcome the shortage of data in the Arabic language.

Furthermore, encoder-decoder paradigm [17, 18, 19] was used for Arabic image
captioning, in which it also leveraged pre-trained image models such as
VGGNet. This work uses the multi-task learning paradigm which leverages models
trained on multiple tasks such as object recognition and detection in addition
to other computer vision tasks. While, the work in [19] publishes the
collected data for public use, this work uses different methods for collecting
the Arabic captions, as instead of translation using Google API, this work
proposes the usage of 3 best evaluated English-to-Arabic open source
translation models in order to gain multiple captions per on image.

Work presented in [20] suggests a new hybrid approach to tackle the
challenging nature of the Arabic language. The hybrid pipeline consists of an
object based caption generator, followed by both object detector and attention
based caption generator. On the other hand, this work proposes an encoder-
decoder architecture, that uses a shared encoder between multiple tasks as an
attempt to overcome the shortage of high quality labeled data in Arabic
language.

Multi-task learning paradigm was used for image captioning in [14, 13, 5] for
the English language. Also, the work presented in this document differs in the
language, the tasks, the proposed architecture from the aforementioned papers
and the variety of features that are explored. As the main language in this
work is Arabic. Also the architecture proposed in this work is encoder-
decoder based architecture with a shared encoder and multiple decoders; one
for each task; and the different tasks are trained on a language different
than Arabic to tackle the deficiency of data in the Arabic language.

In summary, the existing literature on Arabic image captioning is novel and
only few attempts addressed it, with either applying translation on top of
English image captioning systems, or applying famous algorithms on translated
datasets or by utilizing some Arabic linguistic features. However, the work
lacks a unified dataset that is open for public where each work creates its
own dataset, and hence there is an absence of benchmarks for this task.

The contributions are summarized as follows:

  * •

An attempt to enhance the performance of Arabic image captioning task by using
multi-task learning in order to overcome the scarcity of high quality humanly
annotated Arabic dataset for image captioning.

  * •

Exploring new different visual and textual features for Arabic image
captioning for both multi-task learning and single task learning.

  * •

Provide a publicly available translated dataset for Arabic image captioning to
compare the different performances of algorithms on this task.

  * •

Provide a benchmark for Arabic image captioning in order to accelerate the
research in the task.

The code and datasets used are available at this link.

##  3 Method

This section describes the MTLparadigm, features explored, the architectures
and the datasets used to train the image captioning model.

###  3.1 Multi-task Learning Paradigm

The Multi-task Learning (MTL) paradigm can be used for multiple purposes in
order to enhance the models’ performance on specific tasks. It has various
positive effects such as implicit data augmentation, focusing attention on a
specific task and can play a regularization role [21].

The concept of MTL consists of hidden layers that are shared between all the
trained tasks, and multiple task-specific output layers for each of the tasks.
Figure 1 illustrates the MTL paradigm.

Figure 1: Multi-task Learning Paradigm [21]

The training methodology of MTL consists of training with each batch each task
separately, in which at each batch, the training updates the weights of the
task specific layers and the shared layers, while preserving the weights of
the other tasks, and with each different batch, the task that is currently
being trained changes.

The purpose of using MTL in this work is to overcome the scarcity of high
quality data for image captioning in the Arabic Language, therefore multiple
language agnostic tasks will be used to enhance both the visual and textual
perception of the overall model.

The tasks used will be image captioning, object recognition [22] and action
classification [23]. The object recognition task is selected in order to
assist the model in recognizing the dominant object in an image which in turn
will enhance the image captioning model performance in determining the
dominant object in an image. Also, the action classification task will improve
the image captioning model in recognizing the action in the image which is
expected to enhance the image captioning capability of the model.

###  3.2 Features

Different features will be examined for both textual and visual features.

####  3.2.1 Textual Features

Word embeddings are an integral part of most Natural Language Processing
tasks, as they act as text encoders in order to provide contextual
representation for different words, which usually results in significant
enhancements on the performance of the models on different tasks. The
following word representations will be used in this work.

  * •

AraVec [24] is a publicly available pre-trained word embeddings for the Arabic
language using Word2Vec technique [25]. It consists of more than 3.3 Million
tokens from different domains such as tweets, Wikipedia and World Wide Web
pages.

  * •

ELMO Based Embeddings [9] Elmo embeddings were first to provide different
embeddings for the same word depending on the context of the sentence, in
order to tackle the issues in Word2Vec models.

  * •

Bert-Based Embeddings [26] The Bert-based model uses 12 layers of transformer
encoders, in which each layer provides a different representation for the
word/sentence. They are trained on huge amount of data, and provide contextual
and semantic representations for the words. The pre-trained model in [27] will
be used in this work.

####  3.2.2 Image Features

The field of computer vision has witnessed significant advances in both the
datasets and algorithms, which in turn yielded significant advances in the
features that are used as image encoders. In this work, the most used image
features will be used for the purpose of evaluating their performance on the
task of Arabic image captioning. The following visual features will be used.

  * •

ResNet [28] Residual Networks were first introduced for image recognition and
they significantly enhanced the performance of the computer vision models on
image recognition task. They have exceptional learning capabilities and
therefore it is very common to be used as image encoders and features for
different tasks that involve image processing.

  * •

VGGNet [29] was first proposed in 2014 as an attempt to investigate the effect
of Convolutional Neural Network (CNN) depth effect on the performance of image
recognition. It has been widely used as image encoders (features) for
different image processing tasks as it has proven its representation
capabilities.

Both of these networks are trained on ImageNet dataset [22].

###  3.3 Architectures

As aforementioned, the MTL paradigm consists of shared layers between all
tasks and a task specific layer for each task.

####  3.3.1 Shared Layers

The shared layers that will form the encoder of the MTL paradigm will consist
of Convolutional Neural Networks (CNN) layer in order to learn image features
based on the actions and objects to be passed for the different decoders.

####  3.3.2 Task-Specific Layers

The task specific layers of the object recognition and action classification
tasks will consist of Fully Connected Neural Networks and a Softmax prediction
output layer.

Whereas, Long-Short-Term-Memory (LSTM) based decoder will be used as a task
specific layer for image captioning due to LSTM capabilities of receiving and
generating variable output sequences.

####  3.3.3 Action and Object classifiers architecture

For a more detailed description of the classifiers; each of the object and
action classifiers are implemented with a similar architecture. The features
will be extracted from either ResNet or VGGNet, that will be fed into CNN
Layers, in addition to a Fully Connected Neural Network (FCNN) and finally a
FCNN layer with Softmax activation function as an output layer. Figure 2
illustrates the action and object classifiers, whereas table 1 presents the
hyper-parameters of the networks.

Figure 2: Action and object classifiers architecture Table 1: Object and Action classifier hyper-parameters Hyper-Paramter | Value
---|---
Number of CNN layers | 6
Filter size | 3X3
Stride | 1
Number of nodes | 64
FCNN Number of layers | 2
FCNN number of nodes | 64
FCNN activation function | Relu
Dropout | 0.2

####  3.3.4 Image captioning architecture

The implemented architecture for image captioning is very similar to the
architecture in show, attend and tell [4]. The Encoder-decoder paradigm is
utilized, whereas the encoder consists of CNN layers that were fed the image
features extracted from ResNet or VGGNet. The decoder on the other hand is
implemented using LSTM as they can generate the captions sequentially at every
time step. Also Bahdanu [30] attention was implemented in the decoder which
has been proved in multiple domains and tasks that it significantly enhances
the performance. Figure 3 illustrates the architecture of the image caption-
er, whereas table 2 shows the hyper-parameters used to implement the image
captioning architecture.

Figure 3: Image captioning architecture Table 2: Image captioning architecture hyper-parameters Hyper-Paramter | Value
---|---
Number of CNN layers | 6
Filter size | 3X3
Stride | 1
Number of nodes | 64
LSTM Number of layers | 2
LSTM Number of nodes | 512
Dropout | 0.2
Attention number of nodes | 256

###  3.4 Image Captioning Datasets

The following datasets will be used in the experiments. All the datasets will
be translated using 3 open source models and services. These models are Google
Translation API, Facebook Machine Translation and University of Helsinki Open
translation services.

  * •

Flickr8K [31]This dataset consists of 8000 images while each of these images
has 5 different captions.

  * •

Flickr30K[10] As an extension of the previous dataset, this dataset includes
around 32000 images while again each of these images has five different
captions. For both of Flickr dataset, the division provided by the authors for
training, validation and testing will be followed.

  * •

MSCOCO [7]This dataset has around 120000 for training and validation. While
each of these images also has five different captions.

The datasets will be combined in both training and testing. However, for
speeding the training, 70% of the training only was used and the same for
training. The division is available on the Github repository provided earlier
in the document.

###  3.5 Other Datasets

For training the aforementioned action classifiers, Stanford 40 Action [32]
dataset will be used for action classification. The Stanford 40 dataset
consists of 9532 different images with 40 classes, in which it has 180-300
images per class.

On the other hand, the object classifier is trained on Cifar-100 dataset [33]
which consists of 100 different objects with different levels and depths.

###  3.6 Architecture training

Figure 4 is a summary of the implemented architecture including the three
aforementioned tasks and the variation of features described above.

Figure 4: Multi-task learning paradigm for image captioning

Unlike most MTL training designs, which include switching between the tasks
after each batch, this work trains the action classifier, then the object
classifier, and uses the resulting encoder for image captioning. this training
procedure was followed because this work only focuses on enhancing the image
captioning performance.

The training related parameters used were Adam [34] as an optimizer, 0.001 as
learning rate, batch size of 32 and 80 epochs were trained.

##  4 Experimental Design

This section presents the evaluation metrics and the different experiments
conducted to study the effect of each feature and technique on the overall
performance.

###  4.1 Evaluation metrics

The following metrics will be used to assess the performance of the different
models:

  * •

BLEU-N [35] This is a common metric for evaluating translation models due to
the fact that it correlates with human judgment. While using BLEU, the recall
and precision are calculated by best match length and n-gram precision.

  * •

METEOR [36] This metric was also first proposed for the evaluation of
translation. It was proposed to tackle the issues of the BLEU score. This
metric uses the balanced mean of the unigram precision and recall and the
penalty function for incorrect word order.

###  4.2 Baseline model

For the purpose of evaluating the effect of each component on the overall
performance of image captioning in the Arabic language; at first a baseline
model which consists of ResNet as feature extractor for images, a simple
tokenizer as word representation, and a CNN encoder solely trained on image
captioning without other tasks.

###  4.3 Effect of Different Features

Both the effect of visual and textual features will be evaluated. Different
variations of the textual and visual features will be evaluated.

####  4.3.1 Text Features

As they contributed to increased performance enhancement on each task they
were used in, text-based features namely word embeddings or representations
will be used as text encoders. Aravec, BERT-based embeddings and ELMO-based
embeddings.

####  4.3.2 Image Features

The popular ResNet and VGGNet are used as image features in this work. They
are compared in order to study the effect of using different image features on
image captioning.

###  4.4 Effect of Multi-task Learning

The effect of the addition of each task on image captioning will be evaluated.
At first, the shared encoder will be trained on action classifier then image
captioning to evaluate the effect of adding the action classifier task. The
same pipeline will be repeated for object detection task. Finally, to assess
the effect of both tasks; the CNN shared encoder will be trained on action
classification, then object classification and eventually image captioning.

###  4.5 Comparison with other work and languages

To evaluate the overall status of the Arabic Image captioning, it is compared
against the results on the same datasets in the English language. However, as
mentioned earlier in the document, Arabic image captioning results on a
unified dataset are not available.

##  5 Experimental Design and Results

Presenting the experimental results of each of the experiments described
above. Also, the features and parameters of the baseline model are used when
studying the effect of one feature.

Table 3 presents the results of the baseline model described in the above
section.

Table 3: Baseline model Performance Feature | B-2 | B-3 | B-4 | METEOR
---|---|---|---|---
Baseline model | 34.13 | 23.5 | 14.31 | 13.13

Table 4 illustrates the results of using different set of work
representations.

Table 4: Word embeddings effects on the performance Feature | B-2 | B-3 | B-4 | METEOR
---|---|---|---|---
Tokenizer | 34.21 | 23.5 | 14.31 | 13.13
AraVec | 35.22 | 24.92 | 14.87 | 13.79
BERT Based | 34.46 | 24.15 | 14.45 | 13.36
ELMO | 34.33 | 23.98 | 14.35 | 13.21

It is evident that the use of word embeddings has a positive effect on the
performance. However, Aravec based embeddings achieved the results as they are
trained on the largest amount of data between the three presented techniques.
Also, the used ELMO and BERT embeddings were trained on the dialectic version
of the Arabic language, which might have negatively affected the results.

Similarly, table 5 shows the results for using different image extraction
features. Tokenizer as word embeddings were used in the following table.

Table 5: Image features effects on the performance Feature | B-2 | B-3 | B-4 | METEOR
---|---|---|---|---
ResNet | 34.21 | 23.5 | 14.31 | 13.13
VGGNet | 34.22 | 23.4 | 14.26 | 13.12

There was not any evident difference between the use of ResNet or VGGNet on
the results.

Finally, the effect of multi-task learning is presented in table 6. The word
embeddings used in this experiment are Aravec as they provided the best
results. ResNet is used as the image feature extractor.

Table 6: The effect of different tasks on the performance Task | B-2 | B-3 | B-4 | METEOR
---|---|---|---|---
Object Recognition | 35.29 | 25.23 | 14.91 | 14
Action Classification | 35.59 | 25.83 | 15.02 | 14.21
Both Tasks | 36.38 | 25.93 | 15.09 | 14.23
Single-task Learning | 34.13 | 23.5 | 14.31 | 13.13

Multi-task learning achieved better results than single task learning.
However, the action classification task achieved better results than object
classifier, which can be attributed to the fact that actions are more relevant
to image captioning, and the fact ResNet is already heavily trained on object
classification task.

Finally, table 7 shows the difference between the results in the work; show,
attend and tell [4] on flickr8k test-set against the best performing model in
this work against the same test-set.

Table 7: Comparison against the state of the art English language Feature | B-2 | B-3 | B-4 | METEOR
---|---|---|---|---
Show, attend and tell | 45.7 | 31.4 | 21.3 | 20.3
This work | 36.38 | 25.93 | 15.09 | 14.23

##  6 Conclusion

The literature and experiments conducted in this work clearly show that the
Arabic image captioning task is lacking behind when compared to English. Also,
the absence of benchmarks and dataset slows down the research. Also, it can be
concluded that MTL can be utilized to overcome shortage of data for a specific
task and its potential is worth further exploration in this task. Also, the
use of pre-trained word embeddings clearly enhanced the performance of image
captioning which further proves their usefulness and the fact that NLP
advances can contribute to the advances of image captioning.

## Acknowledgments

The authors would like to thank Mawdoo3.com company for granting permission to
use their servers for conducting the experiments.

## References

  * [1] Xinlei Chen and C Lawrence Zitnick.  Learning a recurrent visual representation for image caption generation.  arXiv preprint arXiv:1411.5654, 2014.
  * [2] Ahmed Elhagry and Karima Kadaoui.  A thorough review on recent deep learning methodologies for image captioning.  arXiv preprint arXiv:2107.13114, 2021.
  * [3] Oriol Vinyals, Alexander Toshev, Samy Bengio, and Dumitru Erhan.  Show and tell: A neural image caption generator.  In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 3156–3164, 2015.
  * [4] Kelvin Xu, Jimmy Ba, Ryan Kiros, Kyunghyun Cho, Aaron Courville, Ruslan Salakhudinov, Rich Zemel, and Yoshua Bengio.  Show, attend and tell: Neural image caption generation with visual attention.  In International conference on machine learning, pages 2048–2057. PMLR, 2015.
  * [5] Cheng Wang, Haojin Yang, and Christoph Meinel.  Image captioning with deep bidirectional lstms and multi-task learning.  ACM Transactions on Multimedia Computing, Communications, and Applications (TOMM), 14(2s):1–20, 2018.
  * [6] Peter Anderson, Xiaodong He, Chris Buehler, Damien Teney, Mark Johnson, Stephen Gould, and Lei Zhang.  Bottom-up and top-down attention for image captioning and visual question answering.  In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 6077–6086, 2018.
  * [7] Xinlei Chen, Hao Fang, Tsung-Yi Lin, Ramakrishna Vedantam, Saurabh Gupta, Piotr Dollár, and C Lawrence Zitnick.  Microsoft coco captions: Data collection and evaluation server.  arXiv preprint arXiv:1504.00325, 2015.
  * [8] Naaima Boudad, Rdouan Faizi, Rachid Oulad Haj Thami, and Raddouane Chiheb.  Sentiment analysis in arabic: A review of the literature.  Ain Shams Engineering Journal, 9(4):2479–2490, 2018.
  * [9] Mahmoud Al-Ayyoub, Aya Nuseir, Kholoud Alsmearat, Yaser Jararweh, and Brij Gupta.  Deep learning for arabic nlp: A survey.  Journal of computational science, 26:522–531, 2018.
  * [10] Bryan A Plummer, Liwei Wang, Chris M Cervantes, Juan C Caicedo, Julia Hockenmaier, and Svetlana Lazebnik.  Flickr30k entities: Collecting region-to-phrase correspondences for richer image-to-sentence models.  In Proceedings of the IEEE international conference on computer vision, pages 2641–2649, 2015.
  * [11] Yu Zhang and Qiang Yang.  An overview of multi-task learning.  National Science Review, 5(1):30–43, 2018.
  * [12] Joseph Worsham and Jugal Kalita.  Multi-task learning for natural language processing in the 2020s: where are we going?  Pattern Recognition Letters, 136:120–126, 2020.
  * [13] Wei Zhao, Benyou Wang, Jianbo Ye, Min Yang, Zhou Zhao, Ruotian Luo, and Yu Qiao.  A multi-task learning approach for image captioning.  In IJCAI, pages 1205–1211, 2018.
  * [14] Anna Fariha.  Automatic image captioning using multitask learning.  In Proceedings of the 29th Conference on Neural Information Processing Systems, 2016.
  * [15] Vasu Jindal.  A deep learning approach for arabic caption generation using roots-words.  In Thirty-First AAAI Conference on Artificial Intelligence, 2017\.
  * [16] Vasu Jindal.  Generating image captions in arabic using root-word based recurrent neural networks and deep neural networks.  In Proceedings of the AAAI Conference on Artificial Intelligence, volume 32, 2018.
  * [17] Rasha Mualla and Jafar Alkheir.  Development of an arabic image description system.  International Journal of Computer Science Trends and Technology (IJCST)–6 (3), pages 205–213, 2018.
  * [18] Huda A Al-Muzaini, Tasniem N Al-Yahya, and Hafida Benhidour.  Automatic arabic image captioning using rnn-lst m-based language model and cnn.  International Journal of Advanced Computer Science and Applications, 9(6), 2018.
  * [19] Obeida ElJundi, Mohamad Dhaybi, Kotaiba Mokadam, Hazem M Hajj, and Daniel C Asmar.  Resources and end-to-end neural network models for arabic image captioning.  In VISIGRAPP (5: VISAPP), pages 233–241, 2020.
  * [20] Imad Afyouni, Imtinan Azhar, and Ashraf Elnagar.  Aracap: A hybrid deep learning architecture for arabic image captioning.  Procedia Computer Science, 189:382–389, 2021.
  * [21] MS Windows NT kernel description.  https://ruder.io/multi-task/.  Accessed: 2021-11-17.
  * [22] Jia Deng, Wei Dong, Richard Socher, Li-Jia Li, Kai Li, and Li Fei-Fei.  Imagenet: A large-scale hierarchical image database.  In 2009 IEEE conference on computer vision and pattern recognition, pages 248–255. Ieee, 2009.
  * [23] Gary Ge, Kiwon Yun, Dimitris Samaras, and Gregory J Zelinsky.  Action classification in still images using human eye movements.  In Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition Workshops, pages 16–23, 2015.
  * [24] Abu Bakr Soliman, Kareem Eissa, and Samhaa R El-Beltagy.  Aravec: A set of arabic word embedding models for use in arabic nlp.  Procedia Computer Science, 117:256–265, 2017.
  * [25] Tomas Mikolov, Kai Chen, Greg Corrado, and Jeffrey Dean.  Efficient estimation of word representations in vector space.  arXiv preprint arXiv:1301.3781, 2013.
  * [26] Emily Alsentzer, John R Murphy, Willie Boag, Wei-Hung Weng, Di Jin, Tristan Naumann, and Matthew McDermott.  Publicly available clinical bert embeddings.  arXiv preprint arXiv:1904.03323, 2019.
  * [27] Bashar Talafha, Mohammad Ali, Muhy Eddin Za’ter, Haitham Seelawi, Ibraheem Tuffaha, Mostafa Samir, Wael Farhan, and Hussein T Al-Natsheh.  Multi-dialect arabic bert for country-level dialect identification.  arXiv preprint arXiv:2007.05612, 2020.
  * [28] Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun.  Deep residual learning for image recognition.  In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 770–778, 2016.
  * [29] Karen Simonyan and Andrew Zisserman.  Very deep convolutional networks for large-scale image recognition.  arXiv preprint arXiv:1409.1556, 2014.
  * [30] Dzmitry Bahdanau, Jan Chorowski, Dmitriy Serdyuk, Philemon Brakel, and Yoshua Bengio.  End-to-end attention-based large vocabulary speech recognition.  In 2016 IEEE international conference on acoustics, speech and signal processing (ICASSP), pages 4945–4949. IEEE, 2016.
  * [31] Micah Hodosh, Peter Young, and Julia Hockenmaier.  Flickr8k dataset.
  * [32] Bangpeng Yao, Xiaoye Jiang, Aditya Khosla, Andy Lai Lin, Leonidas Guibas, and Li Fei-Fei.  Human action recognition by learning bases of action attributes and parts.  In 2011 International conference on computer vision, pages 1331–1338. IEEE, 2011.
  * [33] Bing Xu, Naiyan Wang, Tianqi Chen, and Mu Li.  Empirical evaluation of rectified activations in convolutional network.  arXiv preprint arXiv:1505.00853, 2015.
  * [34] Diederik P Kingma and Jimmy Ba.  Adam: A method for stochastic optimization.  arXiv preprint arXiv:1412.6980, 2014.
  * [35] Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu.  Bleu: a method for automatic evaluation of machine translation.  In Proceedings of the 40th annual meeting of the Association for Computational Linguistics, pages 311–318, 2002.
  * [36] Satanjeev Banerjee and Alon Lavie.  Meteor: An automatic metric for mt evaluation with improved correlation with human judgments.  In Proceedings of the acl workshop on intrinsic and extrinsic evaluation measures for machine translation and/or summarization, pages 65–72, 2005.