The Semantics and Complexity of Successor-free Nondeterministic G¨odel’s T

The Semantics and Complexity of Successor-free Nondeterministic G¨odel’s T

Bedeho Mesghina Wolde Mender

May 4, 2009

Acknowledgements

I would like to extend my gratitude to my thesis advisor Professor Lars Kris- tiansen for introducing me to his work and for our uncountably many talks which I enjoyed so much. Thank you for having the wisdom to know that any- thing worthwhile takes time, especially mathematics. Thank you to Professor Dag Normann for his brave efforts in explaining domain theory to me, and his never ending patience with my many inquiries. Thank you to Professor Herman Ruge Jervell for agreeing to be my secondary adviser, and always making me feel so welcome at the logic meetings. Thank you to my love Camilla for all her encouragement and support, and for our lovely vacation where I discovered the model in this thesis. But most importantly, I owe everything I have and am to my family, especially my mother and father, of whom I am so immeasurably proud.

I dedicate this to you Hibret and Mesghina.

Contents

1 Introduction 3

1.1 Introduction . . . 3

1.2 Overview . . . 4

2 Successor free G¨odel’s T 5 2.1 The Calculus . . . 5

3 Denotational semantics of T^v 8 3.1 The domainD^σ_b . . . 8

3.2 InterpretingT^v_b inD_b+1^σ . . . 10

3.3 MappingD_b^σ toN_b^σ . . . 16

3.4 InterpretingT^v_b inN_b+1^σ . . . 18

4 Successor free computation in T⁻ 24 4.1 InterpretingT⁻_b inN^σ_b+1 . . . 24

4.2 Computation withval^A_b+1 . . . 27

5 Computing nval^A_b in T⁻ 34 5.1 Relating|σ|b and||σ||b . . . 34

5.2 Computing||σ||b, ξb, βb, µb, θ^σ_b, λ^σ_b, ρ^σ_b, δ_b^σ,Υ^σ_b, M erge^σ_b . . . 36

5.3 ModellingAb . . . 42

5.4 Computingnval^A_b+1 . . . 44

6 Complexity classesF_i⁻ and F_i^v 48

Chapter 1

Introduction

1.1 Introduction

L. Kristiansen, P. Voda, N. Jones and M. Barra have in several papers studied the computational power of fragments of various successor-free computational models, such as G¨odel’s T in [1, 2], an imperative language in [1], PCF in [4] and function algebras in [3, 5]. In these papers they have demonstrated surprising computational power such models, and successfully captured well known complexity classes defined by explicit time and space bounds on Turing machines. In particular, L. Kristiansen and P. Voda showed in [1] that certain neat successor-free fragments of G¨odel’s T, perfectly match the well known alternating space-time hierarchy¹

SPACE2^LIN₀ ⊆TIME2^LIN₁ ⊆SPACE2^LIN₂ ⊆TIME2^LIN₃ ⊆SPACE2^LIN₄ ⊆...

The three classes at the bottom of the hierarchy are called respectivelyLINSPACE,

EXPandEXPSPACEin the literature. A natural direction of continued research is to study the nondeterminstic counterpart to this model, and that is the sub- ject of this thesis. We develop a model for a successor-free nondeterministic flavour of G¨odel’s T, which is built with particular consideration made to keep it as convenient to compute as possible, while still being adequate². We desire this convenience since we will use deterministic programs to compute the inter- pretation of nondeterministic programs, and from this establish a relationship between deterministic and nondeterminstic complexity classes. This was the motivating goal for this thesis.

1Let^LINdenotec|x|for somec, and let 2^x₀ =xand 2^x_i+1= 2^2xi.SPACE(f) andTIME(f) denote the set of problems decidable by a Turing machine working inO(f) space and time respectively.

2A model is adequate when the interpretation of any closed termM of base type contains exactly those elements corresponding to canonical termsM reduces to.

1.2 Overview

In chapter 2 we define a deterministic and a nondeterministic successor-free flavour of G¨odel’s T, called T⁻ and T^v respectively. We establish that T^v is strongly normalizing, and define some concepts required later.

In chapter 3 we provide a denotational semantic for T^v and demonstrate its adequacy. This proof also gives a reduction strategy which preserves the interpretation of a running program³ in a desirable way. The model itself is based on interpreting terms in domains with total functionals over power sets, and the domains are also equipped with an order relation and a binary operator.

This operator is the key to understanding the calculus, since it precisely models the nondeterminstic term. We also embed the model of T^v into the natural numbers by way of a computable isomorphism, and this embedded model is later computed in chapter 5.

In chapter 4 we quickly present L. Kristiansens model for T⁻ embedded in natural numbers from [1]. We dramatically extend the computing machinery he develops, by demonstrating terms for input-bounded repetition and higher-level arithmetic. These are used in chapter 5 to compute the interpretation of terms.

In chapter 5 we finally compute the functions defining the model in chapter 2. We decide certain type requirements for doing this by relating the sizes of the deterministic and nondeterministic domains.

In chapter 6 we define complexity classes for T⁻ and T^v, and use the main result from chapter 5 to relate them by computing the interpretation of nonde- terministic programs with deterministic programs.

3We later define a progam to be any closed term of typeι→ι, so a running program is understood to be such a term when given a closed term of typeιas input.

Chapter 2

Successor free G¨ odel’s T

2.1 The Calculus

Definition 2.1. We define the type space as the least setT satisfying (i)ι∈ T (ii)σ×τ∈ T whenσ, τ ∈ T (iii)σ→τ ∈ T whenσ, τ ∈ T. For convenience let the shorthandsσ1×...×σn andσ1, ..., σn−1→σn denote typesσ1×(...(σn−1× σn))andσ1→(σ2→...(σn−1→σn))respectively.

For each type σ∈ T we have an infinite countable supply of symbols V^σ = {x^σ₀, x^σ₁, x^σ₂, ...} called the variables of type σ, and the set of all variables of all types is V=S

σ∈T V^σ. Likewise we haveH^σ ={[]^σ₀,[]^σ₁,[]^σ₂, ...} called the holes of typeσ, and the set of all holes of all types is H=S

σ∈T H^σ. We also have an infinite countable supply of symbolsK={k0, k1, k2, ...} called numerals.

We inductively define C⁻ as the set of all deterministic successor-free con- texts. All contexts C ∈ C⁻ are said to be of some type σ ∈ T, and we may clarify the type ofC by writingC^σ or C:σ.

(NUM). ki is a context of typeι for allki∈ K (HOLE).[]^σ_i is a context of typeσ for all[]^σ_i ∈ H (VAR). x^σ_i is a context of typeσfor all x^σ_i ∈ V

(APP). (C₁^σ→τC₂^σ)is a context of typeτ for all contextsC₁^σ→τ,C₂^σ

(ABS).λx^σ_i.C^τ is a context of typeσ→τ for any x^σ_i ∈ V and all contexts C^τ (PAIR).hC₁^σ,C₂^τi is a context of typeσ×τ for all contextsC₁^σ,C^τ₂

(L-PRJ). f st.C^σ×τ is a term of typeσ for all contextsC^σ×τ (R-PRJ).snd.C^σ×τ is a term of typeτ for all contextsC^σ×τ

(REC).Rσ(C^ι₁,C₂^ι,σ→σ,C₃^σ)is a context of typeσfor all contextsC₁^ι,C₂^ι,σ→σ,C₃^σ We define C^v as the set of nondeterministic successor-free contexts by nat- urally extending the induction schema above with

(NDT).(C₁^σ|C₂^σ)is a context of typeσ for all contextsC₁^σ,C^σ₂

We say that a context is simple when it has at most one hole in it. Let C be a simple context, then for any simple contextC∗ which has the same type as any hole inC, letC[C_∗] denote replacingC_∗ with any hole in C.¹

We define the set of deterministic successor-free terms, denoted T⁻, as all contextsC ∈C⁻ which have no hole. We defineT^v the same way. LetC^σ∈C^v be a simpleT^vcontext, and letsbe aT^v-term of appropriate type, observe then that C[s] is also a T^v-term. Given T^v-termsM :σ andt:τ, if there exists a contextC:σsuch that M =C[t] then we say thatt is a subterm ofM.

For any b ≥ 0 let T⁻_b denote the set of T⁻-terms such that all numerals occurring in them are no greater thenkb, and we define T^v_b the same way.

When we simply refer to something as a term, then it may be either a T⁻ orT^v term. For convenience we allow some syntactic sugar; for a term of the form(M) we may write M, for a term of the form((((M)N1)...)Nk)we may writeM(N1, ..., Nk), for a term of the form N(N(...(M)...))whereN occurs k times we may write(N^k(M)), for a term of the formλx1.(λx2.(...λxk.M))we may write(λx1x2...xk.M), and in most situations concerning variables we will drop the subscript and sometimes also type.

A variable is said to be bound in a term M if each occurrence of it in M is within the scope of an abstraction for it, otherwise we say that each occurrence outside of the scope of an abstraction is free inM. A term is said to be closed when all variables are bound, otherwise it is said to be open.

For terms M and N : τ and variable x: τ, we say that N is substitutable forxinM if substituting all freexinM withN does not result in binding free variables inN. LetM_N^x denote such a substitution whenever N is substitutable forxin M.

We define the one step reduction relation →¹ forT⁻ (α). C[λx.M]→¹C[λy.M_y^x] wheny is not free inM (β). C[(λx.M)N]→¹C[M_N^x]

(LPRJ). C[f st.hM, Ni]→¹C[M] (RPRJ).C[snd.hM, Ni]→¹C[N]

(0-REC).C[Rσ(k0, M, N)]→¹C[N]

(REC).C[Rσ(kn+1, M, N)]→¹C[M(kn, Rσ(kn, M, N))]

for any simple context and suitably typed M,N. We define the one step reduction relation¤¹ forT^v by naturally extending the list above with

(γ). C[(M|N)]¤¹C[M]andC[(M|N)]¤¹C[N]

1Notice that using [C∗] respects the inductive structure ofC. By this we mean that for example given the simple C = C1C2 we have C[C∗] = C1[C∗]C2[C∗]. This allows us to do convenient induction on the structure ofC[C∗].

We make the distinction between theT⁻ andT^v reduction relation by using the symbols→¹ and¤¹respectivley. Let the relations→andBbe the symmet- ric,transitive closures of→¹and¤¹. A term is said to be on normal form when no non-α-reduction can be applied to it, and it is said to be on γ-normal form when no non-α-γ-reduction is available.

Definition 2.2. We definelv(σ)as the level ofσby (i)lv(ι) = 0(i)lv(σ×τ) = max{lv(σ), lv(τ)} (iii) lv(σ → τ) = max{lv(σ) + 1, lv(τ)}. Let Rσ1, ..., Rσn

be an exact list of all recursors occurring in a term M, we define the re- cursor rank of M as Rk(M) = max{0, lv(σ1), ..., lv(σn)}. We also define T r(M) as the term rank of M by (i) T r(kn) = 0 (ii) T r(x^σ) = lv(σ) (iii) T r(λx^σ.P^τ) = max{lv(σ → τ), T r(P)} (iv) T r(P Q) = max{T r(P), T r(Q)}

(v) T r(P|Q) = max{T r(P), T r(Q)} (vi) T r(hP, Qi) = max{T r(P), T r(Q)}

(vii) T r(f st.P) =T r(P) (viii) T r(snd.P) =T r(P) (viiii) T r(Rσ(P, Q, R)) = max{T r(P), T r(Q), T r(R)}

Lemma 2.3. For any termM :σwe have (i) T r(M)≥lv(σ)

(ii) T r(M)≥T r(R)for any subtermR of M

(iii) T r(M) =lv(τ) =T r(R)for some subterm R:τ ofM Proof. All are proven by simple induction on structure ofM.

Definition 2.4. We say that an infinite reduction of a term normalizes if it ends with an infinite use of onlyα-reductions, and a term is said to be strongly normalizable if all infinite reductions normalize.

Theorem 2.5. AllT^v-terms are strongly normalizable

Proof. In [7] Berger U. demonstrates that natural extensions of G¨odels T are strongly normalizing by using W.W. Tait’s method of strong computability for simply typed lambda calculus from [8]. However we cannot directly apply his result to our calculus because of a superficial discrepancy. In T^v we do not considerR_σ, f st., snd.and|_σ as independent constants and terms on their own, as is customary and done in [7]. To overcome this we simply construct a new calculus TC where for all typesσandτ we have constants

Rσ:ι,(σ→σ), σ→σ,|σ:σ, σ→σ, f stσ×τ:σ×τ→σ, sndσ×τ:σ×τ→τ and the same reduction rules as before. It is obvious that T^v ⊂TC, and any reduction of a T^v-term is also a reduction of the same term in TC. Therefor since the reduction sequence is normalizing by strong normalization of TC, then T^v is also strongly normalizing.

Chapter 3

Denotational semantics of T ^v

3.1 The domain D

Definition 3.1. For any type σ and b >0 we define D_b^σ as the domain over typeσin base b and a binary relationv^σ_b overD_b^σ

(i) D_b^ι =P({0, ..., b−1})anddv^ι_be⇔d⊆efor alld, e∈D_b^σ1

(ii) D_b^σ×τ =D^σ_b ×D^τ_b anddv^σ×τ_b e⇔f st(d)v^σ_b f st(e)∧ snd(d)v^τ_b snd(e) for alld∈D^σ_b,e∈D^τ_b²

(iii) D_b^σ→τ is the set of all functions f :D^σ_b →D^τ_b and f v^σ→τ_b g ⇔f(d)v^τ_b g(d)for all d∈D_b^σ

These domains are simple in structure and rich in elements not corresponding to any term, e.g. D_b^ι contains the empty set. The domains also contain non- monotonic functions which also do not correspond to any term, given certain natural conditions on open terms. As mentioned in the introduction, the reason no refinements have been made is because we want the domains to be of easily computable size, namely||σ||b as seen later.

We experience that our terms behave monotonically with respect to v^σ_b, so one would expect that an accurate interpretation would be monotonic as well. Also, when [[N : σ→τ]]_A is given input which is monotonic,e.g the in- terpretation of a term, we expect monotonic output. The complication is that monotonicity is usually defined for functions over domains which are them self’s restricted to only monotonic elements. We overcome this by introducing a suit- able extension of the notion of monotonicity.

1P(S) denotes the set of all subsets ofS

2fst and snd refers to functions taking the first and second component of a 2-tuple respec- tively, not to be confused withf st.andsnd.which are part of the term language.

Definition 3.2. We define a unary relation for all domains, called deep mono- tonicity

(i) g∈D_b^ι is deeply monotonic

(ii) g∈D^σ×τ_b is deeply monotonic when f st(g) andsnd(g) are deeply mono- tonic

(iii) g∈D_b^σ→τ is deeply monotonic when

- g(e)is deeply monotonic for all deeply monotonic e∈D_b^σ - dv^σ_b e⇒g(d)v^τ_b g(e)for all deeply monotonic d, e∈D^σ_b

Proposition 3.3. Let M :σ be aT^v_b-term, and Ab+1 be an assignment map- ping all free variables inM to deeply monotonic elements, then[[M]]_Ais deeply monotonic.

Proof. We omit a detailed proof since this proposition si no more then an ob- servation. We prove this by induction on the structure ofM. In each induction case we rely on the fact that the functions defining [[·]]_A, such as∨^σ_b and Ψ^σ_b+1, preserve deep monotonicity.

Proposition 3.4. hD^σ_b,v^σ_biis a partial order.

Proof. We prove this by induction on the structure ofσ.

Definition 3.5. For any type σ and b > 0 we define the binary operator ∨^σ_b overD^σ_b as the merge operator for type σin baseb

(i) d∨^ι_be=d∪efor alld, e∈D_b^ι

(ii) d∨^σ×τ_b e= (f st(d)∨^σ_b f st(e), snd(e)∨^τ_b snd(e))for alld, e∈D_b^σ×τ (iii) f ∨^σ→τ_b g = h for all f, g ∈ D^σ→τ_b , where h(x) = f(x)∨^τ g(x) for all

x∈D_b^σ

Lemma 3.6. For anyd, e, f ∈D^σ_b (i) d∨^σ_b e∈D^σ_b

(ii) d∨^σ_b e=e∨^σ_b d

(iii) (d∨^σ_b e)∨^σ_b f =d∨^σ_b (e∨^σ_b f) (iv) dv^σ_b e∨^σ_b d

(v) d∨^σ_b d=d

(vi) d=e⇔ev^σ_b danddv^σ_b e

(vii) ev^σ_b dandf v^σ_b d⇒(e∨^σ_b f)v^σ_b d

Proof. All are easily proved by a standard induction on the structure σ, and some may also be derived from the others.

For convenience we define a shorthand for merging the elements of any finite setS⊆D_b^σ. LetW_σ,b

d∈Sddenote the merging of alld∈Sin some arbitrary order.

This is well-defined, since merging is both commutative and associative by(ii) and (iii) in Lemma 3.6 respectively. Throughout the text we may use slight variations off this shorthand, but it will always be clear that we are merging over some finite subset of our domains.

3.2 Interpreting T

in D

Definition 3.7. For anyσ andb >0 we define ψ_b^σ:Nb×D^ι,σ→σ_b ×D^σ_b →D^σ_b andΨ^σ_b :D_b^ι\{∅} ×D^ι,σ→σ_b ×D^σ_b →D^σ_b by

(i) ψ^σ_b(0, f, g) =g

(ii) ψ^σ_b(i+ 1, f, g) =f({i}, ψ_b^σ(i, f, g)) (iii) Ψ^σ_b(S, f, g) =W_σ,b

n∈Sψ_b^σ(n, f, g)

Lemma 3.8. For anyS1, S2∈D_b^ι,f ∈D_b^ι,σ→σ and g∈D^σ_b Ψ^σ_b(S1∪S2, f, g) = Ψ^σ_b(S1, f, g)∨^σ_b Ψ^σ_b(S1, f, g) Proof.

Ψ^σ_b(S1∪S2, f, g) =

σ,b_

n∈S1∪S2

ψ_b^σ(n, f, g) Ψ^σ_b def.

= Ã _σ,b

_

n∈S1

ψ_b^σ(n, f, g)

!

∨^σ_b à _σ,b

_

n∈S2

ψ_b^σ(n, f, g)

!

= Ψ^σ_b(S1, f, g)∨^σ_b Ψ^σ_b(S2, f, g) Ψ^σ_b def.

Definition 3.9. We define a domain assignment A in base b as a total map from V into S

σD^σ_b such that A(x^σ) ∈ D_b^σ, occasionally we may write Ab to clarify the base, or only refer to it as an assignment if the context allows this.

LetAbe a domain assignment in baseb+ 1, then we define[[·]]_Aas the domain interpretation ofT^v-terms under assignmentA

[[kn]]_A={n}

[[x]]_A=A(x)

[[M N]]_A= [[M]]_A[[N]]_A

[[λx^σ.M^τ]]_A=f where f(u) = [[M]]_Ax u

3 for allu∈D_b+1^σ [[M^σ|N^σ]]_A= [[M]]_A∨^σ_b [[N]]_A

[[hM, Ni]]_A= ([[M]]_A,[[N]]_A) [[f st.M^σ×τ]]_A=f st([[M]]_A) [[snd.M^σ×τ]]_A=snd([[M]]_A)

[[Rσ(N, F, G)]]_A= Ψ^σ_b+1([[N]]_A,[[F]]_A,[[G]]_A)

Lemma 3.10. For any T^v_b-termM :σ and assignmentAb+1

(i) [[M]]_A∈D^σ_b+1

(ii) [[M]]_U= [[M]]_Afor any assignmentUb+1 if M is closed (iii) [[M]]_Ax

[[R]]A

= [[M_R^x]]_A for anyT^v_b-termR:τ and variablex:τ such thatR is substitutable forxinM.

Proof. All are easily proved by a standard induction on structure of M. We will for closed terms often omit the domain assignment and write [[M]]

instead of [[M]]_A, this is possible since (ii) in the lemma above shows that assignments are irrelevant for closed terms.

Lemma 3.11. For any context C : σ and terms s^τ, t^τ such that C[s],C[t] are T^v_b -terms and assignmentAb+1

(i) [[s]]_Av^τ_b+1[[t]]_A⇒[[C[s]]]_Av^σ_b+1[[C[t]]]_A (ii) [[s]]_A= [[t]]_A⇒[[C[s]]]_A= [[C[t]]]_A

Proof. (i)is easily proved by induction on the structure ofC,(ii) follows imme- diately.

Lemma 3.12. For any T^v_b-termM :σwhere M¤¹N and assignment Ab+1, then[[N]]_Av^σ_b+1[[M]]_Awhen theγ-reduction was used, otherwise[[N]]_A= [[M]]_A. Proof. Lets:τ be the subterm ofM to which the reduction is directly applied, resulting in some termt:τ, so there exists a contextC :σsuch that M =C[s]

and N = C[t]. We now consider each reduction rule and demonstrate that [[s]]_Av^τ_b+1[[t]]_Aif theγ-reduction was used, otherwise [[s]]_A= [[t]]_A.

3A^x_uis standard notation for the map sendingxtou, and otherwise behaving likeA. It is used throughout this thesis.

(α). By definition of [[·]]_A we have [[λy^ρ.M_y^x]]_A=gwhereg(u) = [[M_y^x]]_A^y_u, and [[λx^ρ.M]]_A=f where f(u) = [[M]]_Ax

u. So for allu∈D^ρ_b+1 g(u) = [[M_y^x]]_A^y_u = [[M]]_A^y,x

u,Ay u(y)

(iii)Lemma 3.10

= [[M]]_A^y,x

u,u A^yu(y) =u

= [[M]]_Ax

u yis not free inM

=f(u)

Thereforf =g, that is [[λx^ρ.M]]_A= [[λy^ρ.M_y^x]]_A. (β).

[[(λx.R)S]]_A= [[λx.R]]_A[[S]]_A= [[R]]_Ax [[S]]A

= [[R^x_S]]_A The last equality holds by(iii)in Lemma 3.10

(γ). By definition of [[·]]_A we have

[[R|S]]_A= [[R]]_A∨^σ_b+1[[S]]_A and

[[R]]_Av^σ_b+1[[R]]_A∨^σ_b+1[[S]]_A by(iii)in Lemma 3.6, hence

[[R]]_Av^σ_b+1[[R|S]]_A The argument is symmetric inS.

(PRJ).

[[f st.hR, Si]]_A=f st([[hR, Si]]_A) =f st([[R]]_A,[[S]]_A) = [[R]]_A snd.hR, Siis analogous.

(0-REC).

[[Rσ(k0, F, G)]]_A= Ψ^σ_b+1([[k0]]_A,[[F]]_A,[[G]]_A) [[·]]_Adef.

=

σ,b+1_

n∈[[k0]]_A

ψ^σ_b+1(n,[[F]]_A,[[G]]_A) Ψ^σ_b+1def.

=ψ_b+1^σ (0,[[F]]_A,[[G]]_A) [[k0]]_A={0}def.

= [[G]]_A ψ_b+1^σ def.

(REC).

[[Rσ(kn+1, F, G)]]_A

= Ψ^σ_b+1([[kn+1]]_A,[[F]]_A,[[G]]_A) [[·]]_Adef.

=

σ,b+1_

m∈[[kn+1]]_A

ψ^σ_b+1(m,[[F]]_A,[[G]]_A) Ψ^σ_b+1def.

=ψ^σ_b+1(n+ 1,[[F]]_A,[[G]]_A) [[kn+1]]_A={n+ 1}

= [[F]]_A({n}, ψ^σ_b+1(n,[[F]]_A,[[G]]_A)) ψ_b+1^σ def.

= [[F]]_A



[[kn]]_A,

σ,b+1_

m∈[[kn]]_A

ψ^σ_b+1(m,[[F]]_A,[[G]]_A)





= [[F]]_A¡

[[kn]]_A,Ψ^σ_b+1([[kn]]_A,[[F]]_A,[[G]]_A)¢

Ψ^σ_b+1def.

= [[F]]_A([[kn]]_A,[[Rσ(kn, F, G)]]_A) [[·]]_Adef.

= [[F kn]]_A[[Rσ(kn, F, G)]]_A [[·]]_Adef.

= [[F(kn, Rσ(kn, F, G))]]_A [[·]]_Adef.

We see from the relations above, if aγ-reduction was applied then [[s]]_A= [[t]]_A, so by(ii) in Lemma 3.11 [[M]]_A= [[N]]_Aas desired. Otherwise [[s]]_Av^τ_b+1[[t]]_A, so by(i)in Lemma 3.11 [[N]]_Av^σ_b [[M]]_A.

Corollary 3.13. For any T^v_b-termM :σand assignment A_b+1 whereM ¤N [[N]]_Av^σ_b [[M]]_A

Proof. There is a sequence of T^v_b-terms R1 : σ, ..., Rk : σ where M = R1

and N = Rk and Ri ¤¹ Ri+1 for all i < k. By Lemma 3.12 we know that [[Ri]]_Av^σ_b+1[[Ri+1]]_A, and combined with transitivity ofv^σ_b+1 from Proposition 3.4 we get that [[Ri]]_A v^σ_b+1 [[Rj]]_A for all i, j ≤k. Hence [[R1]]_A v^σ_b+1 [[Rk]]_A, that is [[N]]_Av^σ_b+1[[M]]_A.

Lemma 3.14. Let M be a closed term on normal form of typeσ (i) σ=ι thenM is a numeral

(ii) σ=τ→ρ thenM is a lambda abstraction (iii) σ=τ×ρ thenM is a pair

Proof. We do a simultaneous induction proof on the structure ofM for all three claims, and keep in mind that any subterm ofM must also be on normal form.

In each claim we will argue that M cannot have certain forms, and some of these forms occur in all claims, therefor we argue these outside the claims to avoid repetition.

Since M is closed it cannot be a variable, and since it is on normal form it

can obviously not be on form (A|B). It cannot be on form R(N, F, G) since N : ι by the induction hypothesis must be a numeral, and this allows us to apply the recursor reduction onM, contradicting it being on normal form. It cannot be on form (A^τ→ρB^τ),f st.A^τ×ρ orsnd.A^τ×ρ, since either one would by the induction hypothesis onAallow us to apply a reduction,β- and projection respectively, onM directly. Observe now that the only remaining possible forms are the numeral, lambda abstraction and pairing.

M :ι: Since M is of type ι it cannot be on form λx.A or hA, Bi, so the only remaining form is numeral, soM is a numeral term.

M :τ →ρ: SinceM is of typeτ →ρit cannot be a numeral or on formhA, Bi, so the only remaining form is lambda abstraction, soM is a lambda ab- straction term.

M :τ×ρ: Since M is of type τ×ρ it cannot be a numeral or a lambda ab- straction , so the only remaining form is pairing, soM is a pairing term.

Lemma 3.15. A choice term is a closed T^v term where the γ-reduction is available, but no other non-α-reduction.⁴ Let M : σ be a closed choice term not of the form λx.Q and hP, Qi, then there exists a context C : σ such that M =C[p|q] and

[[C[p|q]]] = [[C[p]]]∨^σ_b+1[[C[q]]]

Proof. We demonstrate this by induction on the structure of M.

Case M =kn, x. Neither of these cases are possible sinceM is a choice term.

Case M = P^τ→σQ^τ. P is a closed term since M is closed. P must be a choice term, otherwise it would have to be on normal form, which by(ii) in Lemma 3.14 puts it on form λx.u, contradicting that M is a choice term. P cannot be on formhu, visince it is of the arrow type, and not on formλx.usince this as mentioned contradicts thatM is choice term. This allows the induction hypothesis to be applied on P, giving us a context C1:σ→τ such thatP=C1[p|q].

LetC=C1Qand observe thatM =C[p|q] and

[[C[p|q]]] = [[C1[p|q]Q]] C[] def.

= [[C1[p|q]]][[Q]] [[·]] def.

=©

[[C1[p]]]∨^τ→σ_b+1 [[C1[q]]]ª

[[Q]] IH.

= [[C1[p]]]([[Q]])∨^σ_b+1[[C1[q]]]([[Q]]) ∨^τ_b+1^→σ.def

= [[C1[p]Q]]∨^σ_b+1[[C1[q]Q]] [[·]] def.

= [[C[p]]]∨^σ_b+1[[C[q]]] C

4Not to be confused with a term onγ-normal form, which does not guarantee having a nondeterministic reduction available. So a choice term is onγ-normal form, but the converse does not hold.

Case M =λx.P,hP, Qi. These cases are not possible by assumption.

Case M =f st.P^σ×τ, snd.P^τ×σ. We only consider the first case. P is clearly a choice term, and cannot be on formλx.usince it is of the product type, and not of formhu, visince this as contradicts thatM is choice term. This allows the induction hypothesis to be applied toP, giving us a contextC1

such thatP =C1[p|q]. LetC=f st.C1 and observe thatM =C[p|q] and [[C[p|q]]] = [[f st.C1[p|q]]] C[] def.

=f st([[C1[p|q]]]) [[·]] def.

=f st([[C1[p]]]∨^σ×τ_b+1 [[C1[q]]]) IH.

=f st([[C₁[p]]])∨^σ_b+1f st([[C₁[q]]]) ∨^σ×τ_b+1 def.

= [[f st.C1[p]]]∨^σ_b+1[[f st.C1[q]]] [[·]] def.

= [[C[p]]]∨^σ_b+1[[C[q]]] Cdef.

Case M = (P|Q). LetC = [] and observe thatM = C[P|Q] and the desired result.

Case M =Rσ(N^ι, F^ι,σ→σ, G^σ). Terms N, F, Gmust all be closed. The term N must be a choice term, otherwise it would be on normal form and therefore by(ii) in Lemma 3.14 also on numeral form, contradicting that M is a choice term. N cannot be on formhu, viorλx.usince it is of the ι type. This allows the induction hypothesis to be applied to N, giving us a contextC1 such thatN =C1[p|q]. Let C=Rσ(C1, F, G) and observe thatM =C[p|q] and

[[C^σ,ρ[p|q]]] = [[Rσ(C1[p|q], F, G)]] C[] def.

= Ψ^σ_b+1([[C1[p|q]]],[[F]],[[G]]) [[·]] def.

= Ψ^σ_b+1([[C1[p]]]∨^ι_b+1[[C1[q]]],[[F]],[[G]]) IH.

= Ψ^σ_b+1([[C1[p]]]∪[[C1[q]]],[[F]],[[G]]) ∨^ι_b+1def.

= Ψ^σ_b+1([[C1[p]]],[[F]],[[G]])∨^σ_b+1Ψ^σ_b+1([[C1[q]]],[[F]],[[G]]) Lemma 3.8

= [[Rσ(C1[p], F, G)]]∨^σ_b+1[[Rσ(C1[q], F, G)]] [[·]] def.

= [[C[p]]]∨^σ_b+1[[C[q]]] Cdef.

This induction reveals that if a term has a nondeterministic choice as its only remaining non-α-reduction, then we will always find such a choice outside the scope of a recursor, meaningF orGfor anyRσ(N, F, G). We may however, find it completely outside a recursor, or alternatively inN. For example we may haveR([A|B], F, G) or evenR(...R([A|B], F0, G0)..., F1, G0), and so on. This is a fundamental ingredient in the adequacy proof, and it actually provides us with a guarantee of how we can suitably reduce a term to preserve its interpretation.

Corollary 3.16. For any closed T^v_b-term M : ι not on normal form with n ∈ [[M]], there exists a term N : ι such that M ¤¹N by way of a non α- reduction andn∈[[N]]

Proof. If M is not a choice term, then it must have a deterministic reduction available, and applying any such reduction preserves the interpretation and thus n∈[[N]]. Assume now that M is a choice term, and observe that it cannot be on formλx.P orhP, Qisince it it of typeι.

By Lemma 3.15M =C[p|q] where

[[C[p|q]]] = [[C[p]]]∨^ι_b+1[[C[q]]]

alternatively

[[M]] = [[C[p]]]∪[[C[q]]]

which demonstrates the existence of an available nondeterministic reduction, moreover we must have n ∈ [[C[p]]] or n ∈ [[C[q]]]. So picking the appropriate reduction will provide the desired result.

Theorem 3.17. For any closed T^v_b-termM :ι n∈[[M]]⇔M ¤kn

Proof. First observe that

M ¤kn⇒[[kn]]v^ι_b+1[[M]] corollary 3.13

⇒ {n} v^ι_b+1[[M]] [[·]]_Adef.

⇒ {n} ⊆ [[M]] v^ι_b+1def.

⇒n∈[[M]]

For the converse implication letn∈[[M]]. By Lemma 3.16 we can do a reduction M¤¹M1¤¹M2¤¹... consisting of only nonα-reductions such that

[[M]] = [[M1]] = [[M2]] =...

This reduction sequence must normalize since it otherwise would constitute a counterexample to Theorem 2.5. So there is a termMiin the sequence on normal form. Mi must also be closed and of typeιsince reductions preserves this, and soMi=kmfor somemby Lemma 3.14. Since andn∈[[Mi]] = [[km]] ={m}, so Mi=kn and thusM¤kn as desired.

3.3 Mapping D

to N

In this section we show how to map D_b^σ into it’s isomorphic counterpart and subset of the natural numbersN_b^σ, by way of a bijectionπ^σ_b.

Definition 3.18. For any type σ and b > 0 we define kσk_b as the nondeter- ministic cardinality of σ by (i) kιk_b = 2^b (ii) kσ×τk_b = kσk_b× kτk_b (iii) kσ→τk_b=kτk^kσk_b ^b. For any typeσandb >0 we defineN_b^σ ={0, ...,kσk_b−1}

This following lemma is necessary for following functions onN_b^σto be well- defined

Lemma 3.19. For any number a∈ N_b^σ where

(i) σ=ι there are unique numbersd0, ..., db−1∈ {0,1} such that a=d0+d12 +...+db−12^b−1

(ii) σ=ρ×τ there are unique numbersd0∈ N_b^τ,d1∈ N_b^ρ such that a=d0+d1||τ||_b

(iii) σ=ρ→τ there are unique numbers d0, ..., d` ∈ N<sub>b</sub><sup>τ</sup> where `=||ρ||b−1 such that

a=d0+d1||τ||_b+...+d`||τ||<sub>b</sub><sup>`</sup>

Proof. (i)is proven the same way as(iii), and both(ii) and(iii) are analogous to Lemma 4.2.

Lemma 3.20. For all b >0 we define

- ξb:N_b^ι →D_b^ι byξb(d0+...+db−12^b−1) ={i|di= 1}

- βb :N_b^ι× Nb→ {0,1} by βb(d0+...+db−12^b−1, i) =di

- µb:D^ι_b→ N_b^ι by µb(S) =X

i∈S

2ⁱ

Then (i) ξb is a bijection (ii) µb is the inverse of ξb (iii)µb is a bijection (iv) β(n, m) = 1⇔ {m} ⊆ξb(n)for any n∈ N_b^ι andm∈ Nb.

Proof. For surjectivity ofξ_b fixS∈D^ι_b and let di=

(

1 i∈ S

0 else for alli < b then

ξb(d0+...+db−12^b−1) ={i|di= 1}=S Injectivity ofξb follows from(ii) , so or anya∈ N_b^ι

µb(ξb(a)) =µb(ξb(d^∗₀+...+d^∗_b−12^b−1))

=µb({i|d^∗_i = 1})

= X

i∈{i|d^∗_i=1}

2ⁱ

=d^∗₀+...+d^∗_b−12^b−1

=a