1: \documentclass[11pt,a4paper]{article}
2:
3: \usepackage{euler,beton}
4: \usepackage{amsmath,amsthm,amssymb}
5: \usepackage{xspace}
6:
7:
8: \newcommand{\Nat}{\mathbb{N}} %% natural numbers
9: \newcommand{\monus}{\dot-}
10: \def\vek#1{\overrightarrow{#1\,\,}}
11:
12: \newcommand{\var}[1]{\alpha_{#1}} %% levelled variables
13: \newcommand{\typ}[1]{\tau_{#1}} %% levelled types
14: \newcommand{\typp}{\tau'_0} %% flat types
15: \newcommand{\fv}[1]{\mathsf{FV}({#1})} %% free variables
16: \newcommand{\abs}[2]{\lambda {#1}\, .\, {#2}} %% lambda abstraction
17: \newcommand{\pair}[2]{\langle {#1},{#2}\rangle} %% pairs
18: \newcommand{\pl}[1]{{#1}\mathsf{L}} %% left projection
19: \newcommand{\pr}[1]{{#1}\mathsf{R}} %% right projection
20: \newcommand{\conv}{\mathrel{\mapsto}} %% conversion
21: \newcommand{\rd}{\mathrel{\leadsto}} %% reduction
22: \newcommand{\all}[2]{\forall {#1} . {#2}} %% universal type
23: \newcommand{\subst}[3]{{#1}[{#2}:={#3}]} %% substitution
24: \newcommand{\ass}[2]{{#1}\mathbin{:}{#2}} %% type asssertion
25: \newcommand{\judge}[3]{{#1}\mathrel{\vdash}\ass{#2}{#3}} %% typing judgement
26:
27: %% typing rules:
28: \newcommand{\ax}{\ensuremath{(\text{var})}\xspace}
29: \newcommand{\impi}{\ensuremath{(\to\! I)}\xspace}
30: \newcommand{\impe}{\ensuremath{(\to\! E)}\xspace}
31: \newcommand{\prodi}{\ensuremath{(\times I)}\xspace}
32: \newcommand{\prodel}{\ensuremath{(\times E^1)}\xspace}
33: \newcommand{\proder}{\ensuremath{(\times E^2)}\xspace}
34: \newcommand{\alli}{\ensuremath{(\forall I)}\xspace}
35: \newcommand{\alled}{\ensuremath{(\forall E^1)}\xspace}
36: \newcommand{\alles}{\ensuremath{(\forall E^2)}\xspace}
37:
38: \newcommand{\nat}{\mathsf{Nat}} %% type of natural
39: %% numbers
40: \newcommand{\natz}{\nat_0}
41: \newcommand{\nati}{\nat_1}
42: \newcommand{\typn}[1]{{#1}^{\ast}} %% instantiated Nat
43: \newcommand{\typnn}[1]{{#1}^{\ast\ast}} %% the same twice
44: \newcommand{\typi}[2]{{#1}^{({#2})}} %% iterated type
45: \newcommand{\num}[1]{\underline{#1}} %% Church numerals
46:
47: \newcommand{\suc}{\mathop{\mathsf{suc}}} %% successor
48: \newcommand{\add}{\mathop{\mathsf{add}}} %% addition
49: \newcommand{\mul}{\mathop{\mathsf{mult}}} %% multiplication
50: \newcommand{\pred}{\mathop{\mathsf{pred}}} %% predecessor
51: \newcommand{\cd}{\mathop\downarrow\nolimits} %% typecast down
52: \newcommand{\cu}{\mathop\uparrow\nolimits} %% typecast up
53: \newcommand{\sub}{\mathop{\mathsf{sub}}}
54: \newcommand{\subt}{\mathop{\widetilde{\mathsf{sub}}}\nolimits}
55:
56: \newcommand{\rk}[1]{\mathrm{rk}({#1})} %% rank of types
57: \newcommand{\ajudge}[5]{{#1}\mathrel{\vdash^{#2}_{#3}}\ass{#4}{#5}} %% annotated judgement
58:
59: \newcommand\betaeq{\mathrel{{=}_\beta}}
60: \newcommand\betaetaeq{\mathrel{{=}_{\beta\eta}}}
61:
62: \newtheorem{theorem}{Theorem}
63: \newtheorem{lemma}[theorem]{Lemma}
64: \newtheorem{proposition}[theorem]{Proposition}
65: \newtheorem{corollary}[theorem]{Corollary}
66: \newtheorem*{definition}{Definition}
67:
68: \begin{document}
69:
70: \title{An Elementary Fragment of Second-Order Lambda Calculus}
71: \author{Klaus Aehlig\thanks{Supported by the DFG Graduiertenkolleg
72: ``Logik in der Informatik''}\\ Mathematisches Institut\\ Universit\"at
73: M\"unchen \and Jan Johannsen\thanks{Partially supported by DFG grant
74: Jo 291/2-2}\\ Institut f\"ur Informatik\\
75: Universit\"at M\"unchen}
76: \date{~}
77:
78: \maketitle
79:
80: \allowdisplaybreaks
81:
82: \begin{abstract}
83: A fragment of second-order lambda calculus (System $F$) is defined
84: that characterizes the elementary recursive functions. Type
85: quantification is restricted to be non-interleaved and stratified,
86: i.e., the types are assigned levels, and a quantified variable can
87: only be instantiated by a type of smaller level, with a slightly
88: liberalized treatment of the level zero.
89: \end{abstract}
90:
91: \begin{section}{Introduction and Related Work}
92:
93: Machine-independent characterizations of computational complexity
94: classes are at the core of the research area called \emph{Implicit
95: Computational Complexity} which has received a lot of attention
96: recently. The goal is to give natural descriptions of these classes
97: by \emph{conceptual} means, mostly derived from mathematical logic. In
98: particular it is desirable to go without any explicit mention of
99: bounds or ad hoc initial functions.
100:
101: The second-order, or polymorphic lambda calculus (System $F$)
102: \cite{gir71,rey74}
103: provides a particularly natural framework for this purpose, as all
104: data-types, such as natural numbers, binary words or trees, can be
105: encoded therein without the use of constructors or initial functions.
106: Unfortunately, full system $F$ has a computational strength far beyond
107: anything reasonable in this context: all functions provably total in
108: second-order arithmetic can be defined.
109:
110: Recently there have been approaches to define fragments of system $F$
111: with a weaker
112: computational strength. Altenkirch and Coquand~\cite{altcoq01}
113: proposed a fragment characterizing the functions provably recursive in
114: Peano Arithmetic by restricting type abstraction to first-order types
115: in a single variable. Earlier, Leivant~\cite{leiv91} has used
116: stratification of type abstraction to obtain a fragment characterizing
117: the fourth level $\mathfrak E_4$ of the Grzegorczyk
118: hierarchy~\cite{grz53}.
119:
120: Here we give a characterization of the third level $\mathfrak E_3$ of
121: the Grzegorczyk hierarchy, that is, the Kalm\'ar elementary recursive
122: functions. In order to achieve this, we use a stratification of type
123: abstractions into only two levels. This alone would give a system in
124: which all definable functions are elementary recursive. However, the
125: class would presumably not be exhausted, as, for example, subtraction
126: seems to be undefinable.
127:
128: Therefore we use a primitive product type former
129: and allow a quantified variable of the lowest level to be
130: instantiated by a finite product of itself. Note that product types
131: are definable in system $F$, however using an additional type
132: quantifier and thus disturbing our stratification.
133:
134: Different restrictions of system $F$ based on linear logic, and
135: characterizing also the elementary recursive functions, as well as
136: polynomial time, were introduced by Girard~\cite{gir98} and further
137: elaborated by several authors~\cite{asprov02,danjoi02}.
138: \end{section}
139:
140: \begin{section}{Definitions}
141:
142: The elementary recursive functions are a natural subclass of the
143: primitive recursive functions that was first defined by Kalm\'ar
144: \cite{kalmar}.
145: A function $f(x,\vec{y})$ is a bounded sum (a bounded product), if it
146: is defined from $g(x,\vec{y})$ by
147: \[ f(x,\vec{y}) =\sum_{i=0}^{x-1} g(i,\vec{y}) \qquad \Bigl(\text{
148: resp. } \quad f(x,\vec{y}) =\prod_{i=0}^{x-1} g(i,\vec{y})
149: \;\;\Bigr) \; . \] The elementary recursive functions are the least
150: class of number-theoretic functions that contains the constant $0$,
151: all projections, successor, addition, modified subtraction $x\monus y
152: := \max(x-y,0)$, multiplication and is closed under composition and
153: bounded sums and products.
154:
155: It is well-known that the elementary recursive functions coincide with
156: the third level $\mathfrak E_3$ of the Grzegorczyk hierarchy
157: \cite{grz53}, and that they coincide as well with the functions
158: computable in time or space bounded by an elementary recursive
159: function (see e.g.~\cite{clotehb}).
160:
161: The functions $\abs{n}{2_k(n)}$ for $k \in \Nat$ are inductively
162: defined as follows: $2_0(n) = n$ and $2_{k+1}(n) = 2^{2_k(n)}$\@.
163: For every fixed $k$, this function is elementary recursive, but the binary
164: function $\abs{kn}{2_k(n)}$ is not:
165: $\abs k {2_k(1)}$ eventually majorizes every elementary recursive
166: function.
167:
168: \paragraph{The system.}
169: We now give a formal definition of our system, by means of a type
170: assignment calculus. So terms are only the terms of the untyped lambda
171: calculus with pairs, i.e., given by the grammar
172: %
173: $$r,s ::= x \mid rs \mid \abs{x}{r} \mid \pair{r}{s} \mid \pl{r}
174: \mid \pr{r}\; , $$
175: where $x$ ranges over an infinite set of variables.
176: %
177: We define types of
178: level $n$ for a natural number $n$\@. However, we will use only the
179: types of level at most $2$\@. Our type variables also come in different
180: levels; let $\var n$ range over variables of level $n$.
181: \begin{definition}
182: The types $\typ n$ of level $n$ and the flat types $\typp$ of
183: level $0$ are inductively given by the following grammar:
184: %
185: \begin{align*}
186: \typ{n} & := \var{n} \mid \typ{n} \to \typ{n} \mid \typ{n} \times \typ{n} \mid \all{\var{k}}{\typ{k}} \\
187: \typp &:= \var{0} \mid \typp \times \typp
188: \end{align*}
189: %
190: where $k<n$ and $\fv{\typ{k}} \subseteq \{ \var k \}$.
191: \end{definition}
192: Note that this notion of the level of a type differs from the notion
193: commonly used in the literature, so it should more correctly be called
194: \emph{modified level}. However, since the usual notion is not used in
195: the present work, for sake of brevity we just use the term
196: \emph{level} for the modified notion.
197:
198: Also note that with respect to our notion of the level of a type, there
199: are no closed types of level $0$.
200:
201: \paragraph{Contexts and Judgments.}
202: A context $\Gamma$ is a set of pairs $x:\tau$ of variables and types,
203: where the variables occurring in a context have to be distinct.
204: A typing judgment is of the form $\judge{\Gamma}{r}{\tau}$ and
205: expresses that $r$ has type $\tau$ in the context $\Gamma$\@.
206: The typing rules are:
207: \begin{align*}
208: \ax\;&\dfrac{}{\judge{\Gamma}{x}{\tau}} & &\text{if }x:\tau\text{ occurs in }
209: \Gamma
210: \\[2ex]
211: \impi\;&\dfrac{\judge{\Gamma,x:\sigma}{r}{\rho}}{\judge{\Gamma}{\abs
212: x r}{\sigma\to\rho}}
213: &
214: &\impe\;\dfrac{\judge{\Gamma}{r}{\sigma \to \rho} \qquad
215: \judge{\Gamma}{s}{\sigma}}{\judge{\Gamma}{rs}{\rho}}
216: \\[2ex]
217: \prodi\;&\dfrac{\judge{\Gamma}{r}{\rho} \qquad \judge\Gamma s \sigma}{\judge\Gamma{\pair{r}{s}}{\rho\times\sigma}}
218: \\[2ex]
219: \prodel\;&\dfrac{\judge\Gamma r {\sigma\times\rho}}{\judge\Gamma{\pl r}\sigma}
220: &
221: &\proder\;\dfrac{\judge\Gamma r {\sigma\times\rho}}{\judge\Gamma{\pr r}\rho}
222: \\[2ex]
223: \alli\;&\dfrac{\judge{\Gamma}{r}{\typ k}}{\judge{\Gamma}{r}{\all{\var k}{\typ k}}}
224: & &\text{if } \var{k} \notin \fv{\Gamma}
225: \\[2ex]
226: \alled\;&\dfrac{\judge{\Gamma}{r}{\all{\var k}{\typ k}}}{\judge{\Gamma}{r}
227: {\subst{\typ k}{\var k}{\sigma_\ell}}} &
228: &\text{if } \ell\leq k \text{ and } \fv{\sigma_\ell} = \emptyset
229: \\[2ex]
230: \alles\;&\dfrac{\judge\Gamma r {\all{\var 0}{\typ 0}}} {\judge\Gamma
231: r {\subst{\typ 0}{\var 0}{\sigma'_0}}}
232: & &\text{where } \sigma'_0 \text{ is flat type.}
233: \end{align*}
234: %
235: We will tacitly use the obvious fact that $\judge\Gamma{r}\tau$ holds
236: only if all the free variables of $r$ are assigned a type in
237: $\Gamma$.
238: The rules are formulated in such a way that weakening is
239: admissible. By a simple induction on the derivation one verifies:
240: \begin{proposition}[Weakening]
241: If $\Gamma \subseteq \Gamma'$ and $\judge{\Gamma}{r}{\tau}$, then
242: $\judge{\Gamma'}{r}{\tau}$.
243: \end{proposition}
244:
245: \paragraph{Reductions.}
246: Our system is equipped with the usual reductions of lambda calculus
247: with pairs. Let $\rd$ be the reflexive and transitive closure of the
248: reduction given by the compatible closure of the conversions below,
249: i.e., by allowing application of these conversions to arbitrary
250: subterms.
251: \begin{align*}
252: (\abs{x}{r})s &\conv \subst{r}{x}{s} \\
253: \pl{\pair{r}{s}} &\conv r \\
254: \pr{\pair{r}{s}} &\conv s \; .
255: \end{align*}
256: %
257: We denote the induced congruence relation by $\betaeq$, i.e.,
258: $\betaeq$ is the symmetric and transitive closure of $\rd$. For
259: technical reasons, in some proofs we will also need the notion of
260: $\beta\eta$-equality, denoted by $\betaetaeq$. It is defined like
261: $\betaeq$, but based on the conversions above together with
262: $\eta$-conversion
263: \[ \abs x {tx}\conv t\]
264: with the proviso that $x$ is not free in $t$.
265:
266: It is easily verified that our reductions preserve typing.
267: \begin{proposition}[Subject Reduction]
268: If $\judge\Gamma r\tau$ and $r\rd r'$, then $\judge\Gamma {r'}\tau$.
269: \end{proposition}
270:
271:
272: \paragraph{Statement of the main result.}
273: For every type $\tau$, we define the type $$\typn{\tau} := (\tau \to
274: \tau)\to(\tau\to\tau)\,.$$
275: For a natural number $n$, the Church
276: numeral $\num n$ is $\abs{fx}{f^nx}$, it can have type $\typn{\tau}$
277: for every $\tau$\@. The types of natural numbers are $\natz :=
278: \all{\var 0}{\typn{\var 0}}$ and $\nati := \all{\var 1}{\typn{\var
279: 1}}$\@. It can be shown that the only closed normal inhabitants of
280: the types $\nat_i$ are the Church numerals, and the identity
281: combinator $\mathsf{id} := \abs{x}{x}$, which is equivalent to the
282: numeral $\num 1$ under $\eta$-conversion.
283:
284: A function $f\colon\Nat^k \to \Nat$ is \emph{representable}, if there
285: is a term $t_f$ such that \mbox{$\judge{}{t_f}{\nati^k \to \natz}$}
286: and for all $\vec{n} \in \Nat^k$, it holds that $t_f \vec{\num n}
287: =_\beta \num{f(\vec n)}$\@. We shall prove below, as Corollary \ref{char},
288: that the representable functions are exactly the elementary recursive
289: functions.
290:
291: \paragraph{Notation.}
292: As usual, lists of notations for terms, numbers etc.\ that only differ
293: in successive indices are denoted by leaving out the indices and
294: putting an arrow over the notation. It is usually obvious where to add
295: the missing indices, otherwise we add dots wherever an index is left
296: out. We use one dot if the index runs with the innermost arrow, two
297: dots if the index runs with the next innermost arrow etc., so that
298: e.g.\ the expression
299: \[ \vek{ t_\cdot \vek{n_{\cdot\cdot,\cdot}} } \]
300: stands for a sequence of the form
301: \[ t_1 n_{1,1} \ldots n_{1,k_1} \; , \; \ldots \; , \; t_r
302: n_{r,1} \ldots n_{r,k_r} \; . \]
303: \end{section}
304:
305: \begin{section}{Completeness}
306:
307: In this section we show one direction of our claim, namely we show
308: that every elementary recursive function can be represented by a term.
309: To start, it is easy to check that the usual basic arithmetic
310: functions can have the following types
311: $$\begin{array}{lclcl}
312: \suc &:=& \abs{nsz}{s(nsz)} &:& \typn{\tau}\to\typn{\tau} \\
313: \add &:=& \abs{mnsz}{ms(nsz)} &:& \typn{\tau}\to\typn{\tau}\to\typn{\tau} \\
314: \mul &:=& \abs{mns}{m(ns)} &:& \typn{\tau}\to\typn{\tau}\to\typn{\tau} \\
315: \end{array}$$
316: {for every $\tau$\@. We use these to program a downward
317: typecast, that is a function }
318: $$
319: \cd\, :=\,\abs{n}{n\suc\num 0} \,\,\colon \typnn{\tau} \to \typn{\tau}
320: $$
321: with the property $\cd \num n\betaeq \num n$\@. Note that $\cd$
322: also has the type $\typn{\natz}\to\natz$, since $\suc$ can be typed as
323: $\natz\to\natz$ by instantiating the argument $\ass{n}{\natz}$ as
324: $\ass n{\typn{\var0}}$. Note moreover that $\add$ and $\mul$, by a similar
325: argument, can also have type $\natz\to\natz\to\natz$.
326:
327: The predecessor can be implemented of type $\natz\to\natz$ as follows:
328: in the context where we have variables $\ass{s}{\var0\to\var0}$ and
329: $\ass{z}{\var0}$, as abstract successor and zero, we get the term
330: $P := \abs{p}{\pair{s(\pl{p})}{\pl{p}}}$ of type
331: $(\var0\times\var0)\to (\var0\times\var0)$, such that the $n$-fold
332: iteration of $P$ applied to $\pair zz$ reduces to $\pair{s^n
333: z}{s^{n\monus 1}z}$, for every $n\geq 0$.
334: Thus the argument $\ass{n}{\natz}$ is
335: instantiated as $\ass{n}{\typn{(\var0\times\var0)}}$ by the rule
336: \alles, and we get
337: \[
338: \judge{\ass{n}{\natz}}{\abs{sz}{\pr{n P \pair{z}{z}}}}{\typn{\var0}}
339: \]
340: and an application of \alli and \impi yields that the predecessor
341: $\pred := \abs{nsz}{\pr{n P \pair{z}{z}}}$ is typeable as
342: $\ass{\pred}{\natz\to\natz}$.
343:
344: We obtain subtraction $\sub := \abs{mn}{n\pred m}$ by iterating the
345: predecessor, of type $\ass{\sub}{\natz \to \typn\natz \to \natz}$.
346: Obviously, for $m,n\in \Nat$ we have $\sub \,\num m \,\num n
347: \betaetaeq \num{m \monus n}$.
348:
349: Testing for zero can also be easily programmed as $\chi_0 :=
350: \abs{nxy}{n(\abs{z}{y})x}$, which has type $\ass{\chi_0}{\natz \to
351: \var0\to\var0\to\var0}$, and the operational semantics \textsl{if
352: $n=0$ then $x$ else $y$}, i.e., with the properties $\chi_0 \, \num
353: 0 \, x \, y \betaeq x$ and $\chi_0 \, \num{n+1} \, x \, y \betaeq y$.
354: To obtain the typing, we instantiate the input $\ass{n}{\natz}$ as
355: $\ass{n}{\typn{\var0}}$ by \alles.
356:
357: Next we define a function $T_0$ such that for natural numbers $n$ and
358: $m$, we have $T_0 \,\num 0\,\num m \betaetaeq \num m$, and $T_0 \,\num{n+1}
359: \,\num m \betaetaeq \num{m+1}$, as
360: \[ T_0 := \abs{nxszs'z'}{\mathop{\chi_0}n(s(xsz)s'z')(xszs'z')} \]
361: The term $T_0$ can have the type $\natz \to \typn{\natz} \to \typn{\natz}$,
362: which is verified as follows: in the context $\ass{x}{\typn{\natz}}$,
363: $\ass{s}{\natz\to\natz}$, $\ass{z}{\natz}$ we obtain the terms $xsz$ and
364: $s(xsz)$ of type $\natz$\@. These are instantiated with the rule \alles
365: as being of type $\typn{\var0}$, and with $\ass{s'}{\var0\to\var0}$ and
366: $\ass{z'}{\var0}$ we get $\ass{s(xsz)s'z'}{\var0}$ and $xszs'z':\var0$\@.
367: Therefore we obtain
368: \[ \judge{\Gamma}{\abs{s'z'}{\mathop{\chi_0} n (s(xsz)s'z')
369: (xszs'z')}}{\typn{\var0}} \; , \] where $\Gamma$ is the context
370: $\ass{n}{\natz}, \ass{x}{\typn{\natz}}, \ass{s}{\natz\to\natz},
371: \ass{z}{\natz}$, and an application of \alli followed by several \impi
372: gives the claimed typing of $T_0$. It is easily verified by
373: straightforward calculations that $T_0$ has the claimed operational
374: behaviour.
375:
376: We use $T_0$ to implement an upward typecast that works with
377: the aid of a large parameter of suitable type, i.e., a term $\ass{\cu}
378: {\typnn{\natz} \to \natz \to \typn{\natz}}$ with the property that
379: $\cu \num m \, \num n \betaetaeq \num n$ as long as $m\geq n$\@.
380: This can be implemented as
381: \[ \cu := \abs{mn}{m\bigl(\abs{x}{T_0 (\sub n x) x}\bigr)\num0} \; , \]
382: i.e., the function $\abs{x}{T_0 (\sub n x) x}$, which operationally
383: behaves as
384: \[
385: \textsl{if $x < n$ then $x+1$ else $x$,}
386: \]
387: is iterated $m$ times, starting at $0$, to
388: the effect that in the first $n$ iterations, the value is increased by
389: $1$, and thereafter the value is $n$, and thus remains the same.
390:
391:
392: Now by use of the typecast, a more useful type-homogeneous
393: subtraction, but again with the aid of a large parameter, can be
394: defined as
395: \[ \subt := \abs{mnk}{\cu m (\sub (\cd n) k)} \; : \;
396: \typnn{\natz} \to \typn{\natz} \to \typn{\natz} \to \typn{\natz} \; ,
397: \]
398: with the property that $\subt \num m \, \num{n} \, \num{k} \betaetaeq
399: \num{n\monus k}$ as long as $m \geq n \monus k$.
400:
401: \begin{definition}
402: For a type $\tau$, let $\typi{\tau}{0} := \tau$, and
403: $\typi{\tau}{k+1} := \typn{(\typi{\tau}{k})}$.
404: \end{definition}
405: To iterate the above construction, assume we have a subtraction
406: \[ \ass{\subt_k }{ \typi{\natz}{k+1} \to \typi{\natz}{k} \to \typi{\natz}{k}
407: \to \typi{\natz}{k}} \; , \]
408: and note that $T_0$ can have type $\typi{\natz}{k} \to
409: \typi{\natz}{k+1} \to \typi{\natz}{k+1}$ for every $k$, since $\chi_0$
410: can have type $\typi\natz{k+1}\to\typi\natz k\to\typi\natz k\to\typi\natz k$ (in
411: fact, $\chi_0$ can have any type of the form
412: $\typn\tau\to\tau\to\tau\to\tau$).
413: Thus we can program an upward typecast
414: \[ \cu_k := \abs{mn}{m \bigl(\abs{x}{T_0 (\subt_k (\cd m) n (\cd x)) x}
415: \bigr)\num0} \]
416: of type ${\cu_k}\colon{\typi{\natz}{k+2} \to \typi{\natz}{k} \to
417: \typi{\natz}{k+1}}$, which again can be used to define a subtraction
418: \[ \subt_{k+1} := \abs{m{n_1}{n_2}}{\cu_k m \bigl( \subt_k (\cd m) (\cd
419: n_1) (\cd n_2) \bigr)} \]
420: of type $\typi{\natz}{k+2} \to \typi{\natz}{k+1} \to \typi{\natz}{k+1}
421: \to \typi{\natz}{k+1}$\@.
422: Thus inductively we get subtractions $\subt_k$ and upward typecasts
423: $\cu_k$ for every $k$\@.
424: We also define iterated upward typecasts
425: $\ass{\cu^\ell_k}{ \typi{\natz}{k+\ell+1} \to \typi{\natz}{k} \to
426: \typi{\natz}{k+\ell}}$ by
427: \[ \cu^0_k := \abs{mn}{n} \qquad \text{and} \qquad \cu^{\ell+1}_k :=
428: \abs{mn}{\cu_{k+\ell} m ( \cu^\ell_k (\cd m) n)} \; . \]
429: From now on we will omit the index $k$ in $\cu_k$, $\cu^\ell_k$ and
430: $\subt_k$ when it can be inferred from the context.
431: We are ready to state our main lemma:
432: \begin{lemma}
433: For every elementary recursive function $f\colon\Nat^n \to \Nat$ and
434: $k\in \Nat$, there are a closed term $t$ and $\ell,r\in \Nat$ and a list
435: $\vec{\eta}$ of types, where each $\eta$ is of the form $\eta ::=
436: \typi{\natz}{k} \mid \typn{\eta} \mid \typn{(\eta \times \eta)}$,
437: such that
438: \[ \judge{}{t}{\vec{\eta} \to \vek{\typi{\natz}{k+\ell}} \to
439: \typi{\natz}{k}} \] and for all $\vec{n} \in \Nat^n$, $t\,
440: \num{\vec{L}} \, \num{\vec{n}} \; \betaetaeq \; \num{f(\vec{n})}$ as
441: long as $L \geq 2_r(\sum \vec{n})$.
442: \end{lemma}
443: Note that we plug in the same numeral $\num L$ for all the arguments
444: of the types $\vec\eta$\@.
445: Also note that only simple types over $\natz$ are used as these types
446: $\vec\eta$, and this is the only property used in the
447: application and proof.
448: A statement similar to this lemma was offered by
449: Simmons~\cite{simmons} as a characterization of the Kalm\'ar
450: elementary recursive functions.
451:
452: Before we prove the main lemma, we shall first use it to derive the
453: main theorem of this section, the representability of all elementary
454: recursive functions:
455: \begin{theorem} \label{elemdef}
456: For every elementary recursive function $f\colon\Nat^n \to \Nat$ there is
457: a closed term $\ass{T}{\nati^n \to \natz}$ such that $T\, \num{\vec{n}}
458: \betaetaeq \num{f(\vec n)}$ for all $\vec n \in \Nat^n$.
459: \end{theorem}
460: \begin{proof}
461: From the lemma for $f$ and $k=1$, we obtain a term $t$ and
462: $\ell,r,\vec{\eta}$ with the properties stated there.
463: As we can always move to bigger values of $r$, we may without loss of
464: generality assume $r$ to be at least $2$ and even.
465:
466: Let $s := r/2$. For each type $\eta_i$, instantiate each input
467: $\ass{n}{\nati}$ as $\ass{n}{\typi{\eta_i}{s}}$, which is possible
468: by \alled since $\typi{\eta_i}{s}$ is a closed type of level $1$\@.
469: Now use $\ass{\add}{\typi{\eta_i}{s} \to \typi{\eta_i}{s} \to
470: \typi{\eta_i}{s}}$ to compute $S := \sum \vec n$ of type
471: $\typi{\eta_i}{s}$\@. Next form the term $N :=
472: (\ldots((S\num2)\num2)\ldots\num2)$, with $r$ occurrences of the
473: numeral $\num2$, of type $\eta_i$.
474:
475: Instantiate the inputs $\vec n$ again by \alled at the closed, level $1$
476: type $\typi{\natz}{\ell}$,
477: and form $T := \abs{\vec n}{\cd (t \, \vec{N} \, \vec{n})}$\@.
478: As for every input $\vec{n}$, $N$ evaluates to a numeral $\num L$ with
479: $L \geq 2_r(\sum \vec n)$, the term $T$ has the required
480: properties, by the lemma.
481: \end{proof}
482: \begin{corollary}
483: For every elementary recursive function $f\colon\Nat^n \to \Nat$ there is
484: a closed term $\ass{T}{\nati^n \to \natz}$ such that $T\, \num{\vec{n}}
485: \rd \num{f(\vec n)}$ for all $\vec n \in \Nat^n$.
486: \end{corollary}
487: \begin{proof}
488: Take $\abs{\vec nsz}T\vec nsz$ for the term $T$ obtained from the
489: theorem. For every $\vec n$ consider the $\beta$-normal of
490: $(\abs{\vec nsz}T\vec nsz)\num{\vec n}$, which is a closed,
491: $\beta$-normal term of type $\Nat$, starting with two abstractions,
492: hence a numeral. So it has to be $\num{f(\vec n)}$, for otherwise
493: two distinct numeral would be $\beta\eta$-equal, which by the well
494: known confluence of lambda calculus with pairs is not the case.
495: \end{proof}
496:
497: \begin{proof}[Proof of the Lemma]
498: We have produced terms representing the base functions successor,
499: addition, subtraction and multiplication above. For $S$, $+$ and
500: $\times$, we can set $\ell=r=0$ and $\vec{\eta}$ empty for any
501: $k$\@.
502:
503: Concerning subtraction $\monus$, for $k=0$ we use the term $\abs{nk}{\sub
504: (\cd n) k}$ and set $r=0$, $\ell=1$ and $\vec{\eta}$ empty, and
505: for $k\geq 1$ we use $\subt_k$, and we set $\ell=r=0$ and
506: $\vec{\eta}$ contains the single type $\typi{\natz}{k+1}$.
507:
508: In the following, note that by the properties of $\cd$, whenever we
509: have a term $t$ of type $\typi{\natz}{k+\ell}$, we can obtain a term
510: $\cd^{\ell} t$ with the same value of type $\typi{\natz}k$.
511:
512: For closure under composition, let $f(\vec n) = g(\vek{h_\cdot(\vec n)})$
513: and $k$ be given. By the induction hypothesis for $g$ and $k$, we
514: have a term $t_g$, numbers $\ell_g$ and $r_g$ and a list
515: $\vek{\eta}$ of types such that the claim of the lemma holds for these.
516:
517: Also, the induction hypothesis for each $h_i$ and $k+\ell_g$ yields
518: terms $t_i$ and $\ell_i,r_i \in \Nat$ and types
519: $\vek{\eta_{\cdot,i}}$, such that the claim holds for these.
520:
521: Let $\ell := \ell_g + \max_i{\ell_i}$\@. Since the functions $h_i$
522: are elementary recursive, $\sum h_i(\vec n)$ is also elementary,
523: and therefore there is an $s\in\Nat$ such that $\sum_i
524: {h_i(\vec n)} \leq
525: 2_s(\sum \vec n)$\@. For variables $\vec{v}$ and
526: $\vek{w_{\cdot,i}}$, which we
527: give the types $\vec\eta$ and $\vek{\eta_{\cdot,i}}$, respectively,
528: we set
529: \[ t := \abs{\vec v \;\vec{\vec{w}}
530: \;\vec n\,}{\, t_g \; \vec v
531: \; \vek{(t_\cdot \:\vek{w_{\cdot,\cdot\cdot}}
532: \: \vek{(\cd^{\ell-\ell_g-\ell_{\cdot\cdot}}\, n_\cdot)})}} \]
533: such that $t$ has type $\vec\eta \to \vec{\vec\eta} \to
534: \vek{\typi{\natz}{k+\ell}} \to \typi{\natz}{k}$\@. By the induction
535: hypothesis, for $r := \max(r_g + s,\vec{r})$ we have $t \,
536: \vec{\num L} \, \vec{\vec{\num L}} \, \vec{\num n} \betaetaeq
537: \num{f(\vec n)}$ as long as $L\geq 2_r(\sum \vec n)$.
538:
539: For closure under bounded sums, let $f(\vec n,m) = \sum_{i=0}^{m-1}
540: g(\vec n,i)$ and $k$ be given. By the induction hypothesis for $g$
541: and $k+1$, we have a term $t_g$, numbers $\ell$ and $r$ and a list
542: $\vec{\eta}$ of types such that the claim of the lemma holds.
543: Define
544: \[ \tilde{\chi}_0 := \abs{nxysz}{\chi_0\, n\, (xsz)\,(ysz)} \]
545: of type $(\typi{\natz}{k+\ell+1})^3 \to \typi{\natz}{k+\ell+1}$,
546: with the same operational semantics as $\chi_0$, i.e., for $i,j\in
547: \Nat$ we have $\tilde{\chi}_0 \, \num0 \, \num i \,\num j \betaetaeq
548: \num i$ and $\tilde{\chi}_0 \, \num{n+1} \, \num i \,\num j \betaetaeq
549: \num j$\@. For variables $\ass{v}{\typi{\natz}{k+\ell+2}}$, $\vec w$
550: of the types $\vec\eta$ and $\vec n,m$ of type
551: $\typi{\natz}{k+\ell+1}$, we have
552: \[
553: T := \abs{x y}{\tilde{\chi}_0 \,
554: (\subt v\, m\, y)x (\add x (\cu^\ell \, v \, (t_g \,\vec w
555: \,\vec n \,y)))} \; ,
556: \]
557: of type
558: $\typi{\natz}{k+\ell+1}\to\typi{\natz}{k+\ell+1}\to\typi{\natz}{k+\ell+1}$.
559:
560: As long as a sufficiently large numeral $\num L$ is substituted for
561: the variables $v$ and $\vec w$, $T$ operationally behaves as
562: \begin{quote}
563: \textsl{if $y< m$ then $x + g(\vec n, y)$ else $x$}.
564: \end{quote}
565: More precisely, $L$ has to be large enough so that all values of
566: $g(\vec n,i)$ are computed correctly, that is, $L \geq 2_r(\sum\vec n
567: + m)$, and we need $L \geq g(\vec n,i)$ for the typecast $\cu^\ell$ to
568: work properly. Next, we define
569: \[ P := \abs{p}{\pair{T (\pl{p}) \,(\pr{p})}{\suc (\pr{p})}} \]
570: of type $(\typi{\natz}{k+\ell+1} \times \typi{\natz}{k+\ell+1}) \to
571: (\typi{\natz}{k+\ell+1} \times \typi{\natz}{k+\ell+1})$\@. When this
572: term, having the operational semantics
573: \[ \pair{s}{i} \mapsto \begin{cases} \pair{s+g(\vec n,i)}{i+1}
574: &\text{if } i<m \\ \pair{s}{i+1} &\text{otherwise,} \end{cases} \]
575: is iterated starting from the pair $\pair{0}{0}$, by use of a
576: sufficiently large numeral of type $\typn{(\typi{\natz}{k+\ell+1}
577: \times \typi{\natz}{k+\ell+1})} $, the values $g(\vec n,i)$ for
578: $i=0,\ldots,m-1$ are summed up in the left component. Thus to
579: represent $f$, we define the term
580: \[
581: t := \abs{u\, v \, \vec w \, \vec n \, m}
582: { \cd^{\ell+1} \bigl(\pl{
583: u \, P \, \pair{\num0}{\num0}
584: }\bigr)}
585: \]
586: of type
587: \[
588: \typn{(\typi{\natz}{k+\ell+1} \times \typi{\natz}{k+\ell+1})} \to
589: \typi{\natz}{k+\ell+2} \to \vec\eta \to \vek{\typi{\nat}{k+\ell+1}} \to
590: \typi{\natz}{k}
591: \]
592: By the induction hypothesis and the construction, we get the property
593: that $t \, \num L \, \num L \, \vec{\num L} \, \vec{\num n} \, \num m
594: \; \betaetaeq \num{f(\vec n , m )}$ as long as $L$ is sufficiently large.
595: To be more precise, $L$ needs to satisfy the requirements above for $T$ to be
596: computed correctly, and $L \geq m$ in order to complete the summation\@.
597: Therefore, let $s$ be such that for every $m$ and $i\leq m$ we have
598: $g(\vec n,i) \leq 2_s(\sum\vec n+m)$, which exists since $g$ is
599: elementary recursive, and let $r' := \max(r,s)$\@. Then all
600: conditions on $L$ are satisfied if $L \geq 2_{r'}(\sum \vec n + m)$.
601:
602: Closure under bounded products is shown in the same way, only with
603: $\add$ in the definition of $T$ replaced by $\mul$, and the iteration
604: of $P$ is started at $\pair{1}{0}$.
605: \end{proof}
606: \end{section}
607:
608: \begin{section}{Soundness}
609:
610: In this section we show the other direction of our claim, that is, we
611: show that every term of type $\nati\to\natz$ denotes a function on
612: Church numerals computable in elementary space. The main idea is to
613: use the elementary bound for traditional cut-elimination in
614: propositional logic. In this section we will deal only with types of
615: level at most $1$, so let $\tau$, $\rho$, $\sigma$ range over those
616: types within this section. Note that every instantiation of $\nati$ is
617: a type of level $1$\@.
618: Types of level $0$ and $1$ are almost simple types
619: (corresponding to propositional logic) with the exception of
620: quantification of $\var0$\@. These quantifiers however, can only be
621: instantiated with flat types of the form $\var0\times\ldots\times\var0$\@.
622: Hence we can get a notion of cut-rank that is invariant under
623: generalization and instantiation of level $0$, if we ignore pairs.
624: Fortunately we can do so, as the reduction of a pair-redex reduces the
625: size of the term and hence does not do any harm. So we define the rank
626: $\rk{\tau}$ of a type $\tau$ inductively as follows:
627: \begin{align*}
628: \rk{\alpha} &:= 0 \\
629: \rk{\rho\times\sigma} &:= \max(\rk{\rho},\rk{\sigma}) \\
630: \rk{\rho\to\sigma} &:= \max(\rk{\rho}+1,\rk{\sigma}) \\
631: \rk{\all{\alpha}{\rho}} &:= \rk{\rho}
632: \end{align*}
633: We inductively define a relation $\ajudge{\Gamma}{m}{k}{r}{\tau}$
634: saying that $\judge{\Gamma}{r}{\tau}$ can be derived by a typing
635: derivation of height $m$ and cut-rank $k$:
636: \begin{align*}
637: &\ax\:\frac{}{\ajudge{\Gamma}{m}{k}{x}{\tau}} & &\text{if }x:\tau\text{ occurs in } \Gamma \text{ and } m,k \geq 0
638: \\[2ex]
639: &\impi\:\dfrac{\ajudge{\Gamma,x:\sigma}{m}{k}{r}{\rho}}{\ajudge{\Gamma}{m+1}{k}{\abs x r}{\sigma\to\rho}}
640: \\[2ex]
641: &\impe\:\dfrac{\ajudge{\Gamma}{m}{k}{r}{\sigma \to \rho} \qquad
642: \ajudge{\Gamma}{m'}{k}{s}{\sigma}}{\ajudge{\Gamma}{m''}{k}{rs}{\rho}}
643: & &\text{if } \rk{\sigma}<k
644: \\[2ex]
645: &\prodi\:\dfrac{\ajudge{\Gamma}mk{r}{\rho} \qquad \ajudge\Gamma{m'}ks\sigma}{\ajudge\Gamma{m''}k{\pair{r}{s}}{\rho\times\sigma}}
646: \\[2ex]
647: &\prodel\:\dfrac{\ajudge\Gamma mkr{\sigma\times\rho}}{\ajudge\Gamma{m+1}k{\pl r}\sigma} & &\text{and analogous for \proder}
648: \\[2ex]
649: &\alli\:\dfrac{\ajudge{\Gamma}mkr\tau}{\ajudge{\Gamma}{m+1}kr{\all{\alpha}{\tau}}}
650: & &\text{if } \alpha \notin \fv{\Gamma}
651: \\[2ex]
652: &\alles\:\dfrac{\ajudge\Gamma mkr{\all{\alpha}{\tau}}}
653: {\ajudge\Gamma{m+1}kr{\subst{\tau}{\alpha}{\sigma'}}}
654: & &\text{where } \sigma' \text{ is a flat type.}
655: \end{align*}
656: where $m'' := \max(m,m')+1$\@. As the rules are precisely those of
657: our typing judgment for types of level at most $1$, we have the
658: following property for typing derivations of level at most $1$: if
659: $\judge\Gamma r\tau$ then there are $m$, $k$ such that $\ajudge\Gamma
660: mkr\tau$\@. On the other hand, the following property obviously
661: holds and motivates our interest in this notion:
662: \[ \ajudge\Gamma mkr\tau \quad \text{implies} \quad |r| \leq 2^m \]
663: The rules are formulated in such a way that weakening is admissible.
664: \begin{proposition}[Weakening]
665: If $\ajudge\Gamma mkr\tau$, $\Gamma'\supset\Gamma$, $m'\geq m$, $k'\geq
666: k$ then $\ajudge{\Gamma'}{m'}{k'}r\tau$.
667: \end{proposition}
668: %
669: The next proposition, which can be shown by a trivial induction on
670: $\typp$ or $\tau$, respectively, explains formally why we can allow
671: instantiations with flat types of level $0$ without any harm: the rank
672: is not altered!
673: %
674: \begin{proposition}\label{prop-rank-subst} For a flat type $\typp$ of
675: level $0$ we have $\rk{\typp}=0$ and
676: $\rk{\subst\tau{\var0}{\typp}}=\rk\tau$.
677: \end{proposition}
678: %
679: Knowing that the rank of a type is not altered by substituting in a
680: flat type, the cut-rank, being a rank, is not altered as
681: well, hence an induction on $\ajudge\Gamma mkt\tau$ shows:
682: \begin{proposition}\label{prop-deriv-subst}
683: If $\ajudge\Gamma mkt\tau$ and $\typp$ is a flat type of level $0$ then
684: $\ajudge{\subst\Gamma{\var0}{\typp}}mkt{\subst\tau{\var0}{\typp}}$
685: \end{proposition}
686: %
687: Using this proposition a simple induction on $m$ shows that a
688: derivation $\ajudge\Gamma mkt\tau$ can be transformed in such a way
689: that the rule $\alli$ is never followed by $\alles$\@.
690: %
691: So from now on we tacitly assume all derivations to be free from
692: those $\alli$-$\alles$-redexes, as for example in the
693: proof of the next proposition, which then is a simple analysis of the
694: last rule of the derivation.
695: %
696: \begin{proposition}
697: If $\ajudge\Gamma mk{\pl{\pair rs}}\rho$ then $\ajudge\Gamma mkr\rho$ and
698: if $\ajudge\Gamma mk{\pr{\pair rs}}\sigma$ then $\ajudge\Gamma
699: mks\sigma$.
700: \end{proposition}
701: %
702: As usual, induction on the first derivation shows that cuts can be
703: performed at the cost of summing up heights.
704: %
705: \begin{lemma}\label{lem-cut}
706: If $\ajudge{\Gamma,\ass x\rho}mks\sigma$ and
707: $\ajudge\Gamma{m'}kr\rho$ then $\ajudge\Gamma{m+m'}k{\subst sxr}\sigma$.
708: \end{lemma}
709: %
710: In order to be able to reduce the cut rank, we first show an
711: ``inversion''-lemma, that is, we show that under certain conditions
712: terms of arrow-type can be brought into abstraction form.
713: \begin{lemma}[Inversion]
714: If $\rk\Gamma\leq k$ and $\ajudge\Gamma mkt{\rho\to\sigma}$ where
715: $\rk\rho\geq k$, then there are $t'$ and $x$ with $t\betaeq\abs x{t'}$
716: such that $\ajudge{\Gamma,\ass x\rho}mk{t'}\sigma$.
717: \end{lemma}
718: \begin{proof}
719: Induction on $m$ and case distinction according to $t$.
720:
721: The case $t=x\vec s$ is impossible, since $x$ would have to occur in
722: $\Gamma$ and hence $\rk\Gamma>k$\@. The case $t=\pair rs\vec t$ is
723: also impossible since $\vec t$ has to be empty, as we assume $t$ to be
724: free of pair-redexes, and therefore $t$ would have to have a pair type.
725:
726: So the only remaining case is that $t$ is of the form $t=(\abs yr)\vec
727: t$\@. The claim is trivial if $\vec t$ is empty. So without loss of
728: generality we might assume $t$ to be $t=(\abs y r)s\vec s$, with
729: $y$ not free in $s,\vec s$\@. The abstraction $\abs yr$ must
730: have been introduced from a derivation
731: $\ajudge{\Gamma,\ass y\tau}mkr{\tilde\tau}$ with $\rk\tau<k$ for otherwise
732: the cut would not have been allowed. Hence, for some $m'$ with
733: $m'+2\leq m$ we get
734: \[
735: \ajudge{\Gamma,\ass y\tau}{m'}k{r\vec
736: s}{\rho\to\sigma} \text{~and~} \ajudge\Gamma{m'+1}ks\tau
737: \]
738: Hence by the
739: induction hypothesis we get a new variable $x$ and a term $t'$ such
740: that $r\vec s\betaeq\abs x{t'}$ and
741: $\ajudge{\Gamma,\ass y\tau,\ass x\rho}{m'}k{t'}\sigma$\@. From that we
742: conclude $\ajudge{\Gamma,\ass x\rho}{m'+2}k{(\abs y{t'})s}\sigma$ and
743: note $\abs x{(\abs y{t'})}s\betaeq\abs x{\subst{t'}ys}=\subst{(\abs
744: x{t'})}ys \betaeq\subst{(r\vec s)}ys=\subst rys\vec s\betaeq(\abs
745: yr)s\vec s=t$, hence the claim.
746: \end{proof}
747:
748: \begin{lemma}[Cut-rank reduction]
749: If $\ajudge\Gamma m{k+1}t\rho$, $\rk\Gamma\leq k$, and $\rk\rho\leq
750: k+1$ then $\ajudge\Gamma{2^m}k{t'}\rho$ for some $t'\betaeq t$.
751: \end{lemma}
752: \begin{proof}
753: Induction on $m$\@. The only interesting cases are $\impi$ and
754: $\impe$\@. Concerning $\impi$ we are in the situation that
755: $\ajudge\Gamma{m+1}{k+1}{\abs xr}{\sigma\to\tau}$ was concluded from
756: $\ajudge{\Gamma,\ass x\sigma}m{k+1}r\tau$\@. With $\rho=\sigma\to\tau$ we
757: have $\rk\Gamma\leq k$, $\rk\sigma<\rk\rho\leq k+1$ and
758: $\rk\tau\leq\rk\rho\leq k+1$\@. Hence an application of the induction
759: hypothesis yields $\ajudge{\Gamma,\ass x\sigma}{2^m}k{r'}\tau$ from
760: which we conclude $\ajudge{\Gamma}{2^m+1}k{\abs x{r'}}{\sigma\to\tau}$
761: which, by weakening, suffices, since $2^m+1\leq2^{m+1}$.
762:
763: Concerning the case $\impe$ we are in the situation that
764: $\ajudge\Gamma{m+1}{k+1}{ts}\rho$ was concluded from $\ajudge\Gamma
765: m{k+1}t{\sigma\to\rho}$ and $\ajudge\Gamma m{k+1}s\sigma$\@. The only
766: case that is not immediate by the induction hypothesis is if
767: $\rk\sigma=k$\@. Then the induction hypothesis gives us
768: $\ajudge\Gamma{2^m}k{t'}{\sigma\to\rho}$ for some $t'\betaeq t$\@. By
769: our assumption $\rk\Gamma\leq k$, hence by inversion we get
770: $\ajudge{\Gamma,\ass x\sigma}{2^m}k{t''}\rho$ for some new $x$ and $t''$
771: such that $\abs x{t''}\betaeq t'\betaeq t$\@. Also by the induction
772: hypothesis we get $\ajudge\Gamma{2^m}ks\sigma$\@. By Lemma~\ref{lem-cut}
773: we get $\ajudge\Gamma{2^m+2^m}k{\subst{t''}xs}\rho$ which yields the
774: claim since $\subst{t''}xs\betaeq(\abs x{t''})s\betaeq ts$.
775: \end{proof}
776:
777: \begin{corollary}\label{cor-cut-elim}
778: If $\ajudge{}m{k+1}t{\typn{\var{}}}$ then
779: $\ajudge{}{2_k(m)}1{t'}{\typn{\var{}}}$ for some $t'\betaeq t$\@.
780: \end{corollary}
781:
782: \begin{proposition}\label{prop-lamfree}
783: If $t$ normal and $\judge\Gamma t{\typp}$ for some $\Gamma$ with
784: $\rk\Gamma\leq1$ then $t$ is $\lambda$-free.
785: \end{proposition}
786: \begin{proof}
787: Inspection of the typing rules yields that the only rule introducing a
788: $\lambda$ is $\impi$, which creates an arrow-type. In order for the
789: whole term to be of arrow-free type, the rule $\impe$ has to be used,
790: either creating a redex or requiring a variable of rank at least $2$.
791: \end{proof}
792:
793: \begin{definition}
794: A term $t$ is \emph{quasinormal}, if every redex in $t$ is of the form
795: $\pl{\pair rs}$ or $\pr{\pair rs}$ with $\lambda$-free $r$ and $s$
796: \end{definition}
797: We remark the trivial property that the normal form of a quasinormal
798: term $t$ can be computed in space bound by the length of $t$\@. We also
799: note that Proposition~\ref{prop-lamfree} also holds for quasinormal
800: terms, since the only types discarded by a redex are those of terms
801: which are $\lambda$-free by definition. Moreover, a simple induction
802: on $t$ shows:
803: \begin{proposition}
804: If $t$ is quasinormal and $s$ is $\lambda$-free and quasinormal then
805: $\subst txs$ is quasinormal.
806: \end{proposition}
807: %
808: From that proposition, Proposition~\ref{prop-lamfree} and
809: Lemma~\ref{lem-cut} we immediately get:
810: %
811: \begin{corollary}\label{cor-qn-cut}
812: If $\ajudge{\Gamma,\ass x\sigma'}m1r\rho$ and
813: $\ajudge\Gamma{m'}1s{\sigma'}$ and $r$ and $s$ are quasinormal then
814: $\ajudge\Gamma{m+m'}1{\subst rxs}\rho$ and $\subst rxs$ is
815: quasinormal.
816: \end{corollary}
817: %
818: This corollary allows us to show our last ingredient for the soundness
819: theorem: we can transform a term with cut-rank $1$ into a quasinormal
820: one at exponential cost.
821: %
822: \begin{lemma}\label{lem-qn-cut-elim}
823: If $\ajudge\Gamma m1t\tau$ then $\ajudge\Gamma{2^m}1{t'}\tau$
824: for some quasinormal $t'$ with $t'\betaeq t$.
825: \end{lemma}
826: \begin{proof}
827: Induction on $m$\@. If $t$ is not quasinormal, it has a subterm of the
828: form $(\abs xr)s$\@. Then, for some $\Delta$, $\sigma$, $\rho$ and $k$ we have
829: $\ajudge{\Delta,\ass x\sigma}k1r\rho$, and $\ajudge\Delta{k+1}1s\sigma$
830: from which $\ajudge\Delta{k+2}1{(\abs xr)s}\rho$ was concluded. Since
831: the cut was allowed, we have $\rk\sigma<1$\@. Hence, by the induction
832: hypotheses we get a quasinormal
833: $s'\betaeq s$ such that $\ajudge\Delta{2^{k+1}}1{s'}\sigma$\@. Also by
834: induction hypothesis we get a quasinormal $r'\betaeq r$ such that
835: $\ajudge{\Delta,\ass x\sigma}{2^k}1{r'}\rho$\@. By
836: Corollary~\ref{cor-qn-cut} we get
837: $\ajudge\Delta{2^{k}+2^{k+1}}1{\subst{r'}x{s'}}\rho$ and
838: ${\subst{r'}x{s'}}$ is quasinormal, hence the claim.
839: \end{proof}
840: %
841: We are now ready to show that every representable function is
842: elementary recursive. To keep the notation simple, we only state and
843: prove this for unary functions, but the generalization to higher
844: arities is straightforward.
845: \begin{theorem}
846: If $\judge{}t{\nati\to\natz}$ then $t$ denotes an elementary function
847: on Church numerals.
848: \end{theorem}
849: \begin{proof}
850: We have $\judge{\ass x\nati}{tx}\natz$\@. Since all our terms are also
851: typeable in usual system $F$, hence strongly normalizing, and since
852: subject reduction holds, we can find (in maybe long time, which
853: however is independent of the input) a normal term $t'\betaeq tx$ and
854: $\judge{x:\nati}{t'}\natz$\@.
855: %
856: Since $t'$ is normal, inspection of the typing rules yields that every
857: occurrence of $x$ must be within some context, that is, of the form
858: %
859: $$
860: \alled\quad
861: \frac{\judge{\ass x\nati}x\nati}{\judge{\ass x\nati}x{\typn\xi}}
862: $$
863: %
864: for some level $1$ type $\xi$, without (free) variable $\var1$\@. Let
865: $c$ be the maximum of the ranks of all the $\xi$'s occurring in that
866: derivation and $k$ the number of occurrences of such $\xi$'s (note that
867: $c$ and $k$ are still independent of the input).
868:
869: Now, let a natural number $n$ be given. Replacing all $\ass x{\typn\xi}$
870: by derivations of $\ass{\num n}{\typn\xi}$ yields a term $t''\betaeq
871: t\num n$ and a derivation
872: $\ajudge{}{k\cdot(n+2)+2|t'|}c{t''}\natz$\@. The bound on the height of
873: the derivation is obtained as follows:
874: there are $k$ derivations of height $n+2$ yielding $\ass n{\typn\xi}$
875: and these are plugged into the derivation of $\ass{t'}\natz$\@. In the
876: latter derivation there is at most one inference for each symbol in
877: $t'$ followed possible by a single quantifier inference.
878:
879: Using Corollary~\ref{cor-cut-elim} we obtain a term $\tilde t\betaeq
880: t''\betaeq t\num n$ such that\linebreak
881: $\ajudge{}{2_{c+1}(k(n+2)+2|t'|)}1{\tilde t}\natz$\@. Hence
882: Lemma~\ref{lem-qn-cut-elim} and the remark on computing the normal
883: form of a quasinormal term provides means to calculate the normal form
884: of $t\num n$ in elementary space. (Note that all the intermediate terms
885: are also of elementary bounded size.)
886: \end{proof}
887:
888: Together with Theorem \ref{elemdef} we obtain the claimed characterization.
889: \begin{corollary} \label{char}
890: The representable functions are precisely the elementary recursive
891: functions.
892: \end{corollary}
893:
894: Note that our characterization does not mean that the normalization
895: procedure for terms typeable in our system is elementary recursive.
896: The following easy counterexample shows that this is indeed not the
897: case: the terms $(\ldots ((\num 2 \,\num 2)\num 2) \ldots \num 2 )$ with $n$
898: occurrences of $\num 2$ are of size $O(n)$, but their normal forms are
899: the numerals $\num{2_n(1)}$ of size $\Omega(2_n(1))$\@. Thus the
900: normalization function has super-elementary growth.
901: \end{section}
902:
903:
904: \begin{thebibliography}{10}
905:
906: \bibitem{altcoq01}
907: T.~Altenkirch and T.~Coquand.
908: \newblock A finitary subsystem of the polymorphic lambda-calculus.
909: \newblock In S.~Abramsky, editor, {\em Typed Lambda Calculi and Applications},
910: volume 2044 of {\em LNCS}, pages 22--28. Springer, 2001.
911:
912: \bibitem{asprov02}
913: A.~Asperti and L.~Roversi.
914: \newblock Intuitionistic light affine logic.
915: \newblock {\em ACM Transactions on Computational Logic}, 3(1):137--175, 2002.
916:
917: \bibitem{clotehb}
918: P.~Clote.
919: \newblock Computation models and function algebras.
920: \newblock In E.~R. Griffor, editor, {\em Handbook of Computability Theory},
921: pages 589--681. Elsevier, 1999.
922:
923: \bibitem{danjoi02}
924: V.~Danos and J.-B. Joinet.
925: \newblock Linear logic and elementary time.
926: \newblock {\em Information and Computation}, 183(1):123--137, 2003.
927:
928: \bibitem{gir71}
929: J.-Y. Girard.
930: \newblock Une extension de l'interpr\'etation de {G\"o}del \`a l'analyse, et
931: son application \`a l'\'elimination des coupures dans l'analyse et la
932: th\'eorie des types.
933: \newblock In J.~Fenstad, editor, {\em Proceedings of the 2nd Scandinavian Logic
934: Symposium}, pages 63--92. North-Holland, 1971.
935:
936: \bibitem{gir98}
937: J.-Y. Girard.
938: \newblock Light linear logic.
939: \newblock {\em Information and Computation}, 143(2):175--204, 1998.
940:
941: \bibitem{grz53}
942: A.~Grzegorczyk.
943: \newblock Some classes of recursive fuctions.
944: \newblock {\em Rozprawy Matematyczne}, 4, 1953.
945:
946: \bibitem{kalmar}
947: L.~Kalm\'ar.
948: \newblock Egyszer{\H{u}} p\'elda eld{\"o}nthetetlen aritmetikai probl\'em\'ara.
949: \newblock {\em Matematikai \'es Fizikai Lapok}, 50:1--23, 1943.
950:
951: \bibitem{leiv91}
952: D.~Leivant.
953: \newblock Finitely stratified polymorphism.
954: \newblock {\em Information and Computation}, 93:93--113, 1991.
955:
956: \bibitem{rey74}
957: J.~Reynolds.
958: \newblock Towards a theory of type structure.
959: \newblock In {\em Proceedings, Colloque sur la programmation}, pages 408--425.
960: Springer LNCS 19, 1974.
961:
962: \bibitem{simmons}
963: H.~Simmons.
964: \newblock Tiering as a recursion technique.
965: \newblock \emph{Bulletin of Symbolic Logic}, to appear.
966:
967: \end{thebibliography}
968: \end{document}
969: