Functional Programming in
Sublinear Space
Ulrich Schöpp
Institute of Advanced Studies
University of Bologna(on leave from University of Munich)

Joint work with Ugo Dal Lago
Workshop on Geometry of Interaction, Traced Monoidal Categories
and Implicit Complexity, Kyoto, August 2009

Programming with Sublinear Space
Computation with data that does not ﬁt in memory• Input can be requested in small chunks from the environment.
• Output is provided piece-by-piece.

Writing sublinear space programs can be quite complicated• Cannot store intermediate values.
• Recompute small parts of values only when they are needed.

Language/Compiler Support

Can we ﬁnd a Programming Language that• hides on-demand recomputation behind useful abstractions;• delegates some tedious programming tasks to a compiler;• allows for an easy combination of a sublinear space algorithms

with the rest of the program?

Language/Compiler Support
Existing work for LOGSPACE explores possible abstractions …
• restricted primitive recursion [Møeller-Neergaard 2004]• subsystem of Bounded Linear Logic [Sch. 2007]• (LOGSPACE predicates: [Kristiansen 2005], [Bonfante 2006])…but is still far away from making programming easier.
Perhaps it is too ambitious for now to aim for a programming
language that completely hides on-demand recomputation?
A more modest goal:
Design a functional programming language that provides support
for working with sublinear space, without trying to hide all
implementation details behind abstractions.

A Functional Language for Sublinear Space

1. Computation with external data
How should we represent data that does not ﬁt into memory in afunctional programming language?

2. Deriving the functional language IntML
3. LOGSPACE programming in IntML

Sublinear Space Complexity
Modify the machine model to account for computation withexternal data:
Turing Machines =⇒ Oﬄine Turing Machines
Oﬄine Turing Machines

read-only input tapework tapewrite-only output tape

Input and output tape belong to environment.
Only the space on the work tape(s) counts.

Oﬄine Turing Machines

Composition is implemented without storing intermediate result.

Oﬄine Turing Machines
Oﬄine Turing Machines can be seen as a convenient abbreviation
for normal Turing Machines that
• obtains its input not in one piece but that may request it

character-by-character from the environment;• gives its output as a stream of characters.

Formally, we may describe this as a computable function of type

Request for output character
Output character

Request for input character
Answer for input request

Space Complexity in Functional Programs

What relates to Oﬄine Turing Machines in the same way thatfunctional programming languages relate to Turing Machines?

Int Construction
Understand the transition from Turing Machines to Oﬄine Turing
Machines in terms of the Int construction[Joyal, Street & Verity 1996].
1. Apply the Int construction directly to a functional language.

2. Derive a functional language from the semantic structure.
3. Identify programs with sublinear space usage.

Traced Monoidal Category• Category B(e.g. sets and partial functions)• Monoidal structure (+, 0)(e.g. disjoint union)ACf

f : A + B −→ C + D
BD• Trace(e.g. while loop)A

f : A + B −→ C + B
T r(f ) : A −→ CCfBCategory Int(B)• Objects are pairs of B-objects

X = (X − , X + )• Morphism f : X → Y is a B-map
Y−
f : X + + Y − −→ X − + Y +

Y+
f
X−

X+

• Composition
Z−

Z+
g
Y−

X+
Y+

f

X−

Structure in Int(B)B embeds into Int(B)• A map from A −→ B in B corresponds to a map(0, A) −→ (0, B) in Int(B).
0

B
f

A

0

This gives a full and faithful embedding.
• We shall use [A] = (1, A), where 1 is a singleton.
1
A

B
f

1

Structure in Int(B)Int(B) has a monoidal structure ⊗(A ⊗ B)− = A− + B −(A ⊗ B) = A + B++

I = (0, 0)+Int(B) is compact closed(X − , X + )∗ = (X + , X − )Unit η : I → X ∗ ⊗ X and counit ε : X ⊗ X ∗ → I:
X−
X+

η

X+

X+

X−

X−

B is monoidal closed X ⊸ Y = X ∗ ⊗ Y

X−
ε

X+

Structure in Int(B)Int(B) has B-object indexed tensors
O
A

O

A

X

−
+

X

= A × X−
= A × X+

(given suitable structure in B, e.g. products)
ExampleB sets with partial functions, (+, 0) coproduct, A ﬁnite
OX ∼· · ⊗ X}= X
| ⊗ ·{zA|A| times

Indexed Tensor
Consider the Int-construction on categories B with
• ﬁnite products (×, 1);• distributive ﬁnite coproducts (+, 0);• uniform trace with respect to (+, 0).

Deﬁne B[Σ] by freely adjoining to B an indeterminate element of Σ.
One obtains indexed categories:
B[−] : Bop → Cat
Int(B[−]) : Bop → Cat
The indexed tensor is a strong monoidal functor
O: Int(B[Σ × A]) → Int(B[Σ]).
AIndexed Tensor
O
A: Int(B[Σ × A]) → Int(B[Σ])• For any f : Σ → A a strong monoidal natural transformation:

πf :

O
A

X −→ hΣ, f i∗ X

in Int(B[Σ])• Natural isomorphisms that are compatible with πf .

OX∼= ρ∗ X
O
 O

O
X∼
(Σ × inl)∗ X ⊗(Σ × inr)∗ X
=
A+B
A
B
O O
O
∗
X∼
α X
=
1

A×B

A

B

Indexed Tensor

The projections
πf :

O
A

X −→ hΣ, f i∗ X

in Int(B[Σ])internalise to a certain extent:N

A [B] R[f ]⊗id/ [A] ⊗RRR
RRR
RR
πf RRRRR
R(

N


π

[B]

A [B]

in Int(B[Σ])Int Construction and Space Complexity
The functions that represent Oﬄine Turing Machines(State × Σ) + N −→ (State × N) + Σ
appear in Int(Pfn) as morphisms of typeO
(N ⊸ Σ) −→ (N ⊸ Σ),Statewhere we write just N for (0, N) and Σ for (0, Σ).

Int Construction and Space Complexity
The functions that represent Oﬄine Turing Machines(State × Σ) + N −→ (State × N) + Σ
appear in Int(Pfn) as morphisms of typeO
(N ⊸ Σ) −→ (N ⊸ Σ),Statewhere we write just N for (0, N) and Σ for (0, Σ).
The structure of Int(Pfn) is useful for working with OTMs.
• Composition:

O O
S

S

Nf O

S
→
(N ⊸ Σ) −−−0Sg(N ⊸ Σ) −→ (N ⊸ Σ)

• Input lookup is just (linear) function application.
• …

A Functional Language for Sublinear Space

1. Computation with external data
2. Deriving the functional language IntML
1. Start with a standard functional programming language.
2. Apply the Int construction to a term model B of this language.
3. Derive a functional language from the structure of Int(B). It
can be seen as a deﬁnitional extension of the initial language.
4. Identify programs with sublinear space usage.

3. LOGSPACE programming in IntML

A Simple First Order Language
Finite Types
A, B ::= α | A + B | 1 | A × B
Ordering on all types
minA | succA (f ) | eqA (f, f )Explicit trace (with respect to +)trace(c.f )(g)(suﬃcient for now, could use tail recursion)Standard call-by-value evaluation, constants unfolded on demand
Chosen for simplicity and to make analysis easy.
Richer languages are possible.

Examples
Example: Additionx : α, y : α ` add(x, y) : α
With syntactic sugar for tail recursion:
add(x, y) =if y = min then x else add(succ x, pred y)With explicit trace:
add(x, y) =(trace p. case p ofinl(z) -> inr(z)| inr(z) -> let z be <x, y> in
if y = min then inl(x) else inr(<succ x, pred y>)) <x,y>The Functional Language IntML
IntML extends the simple ﬁrst order language with syntax for Int(B),where B is the term model of the simple ﬁrst order language.
IntML has two classes of terms and types:• Working Class (for B)

A, B ::= α | A + B | 1 | A × B
Terms from the simple ﬁrst order language + unbox• Upper Class (for Int(B))

X, Y ::= [A] | X ⊗ Y | A · X ⊸ Y
All computation is being done by working class terms. Upper classterms correspond to morphisms in Int(B), which are implemented
by working class terms.

IntML Type System — Working Class
Usual typing rules, e.g.
Σ`f: AΣ ` g: BΣ ` hf, gi : A × B…
There is one additional rule for using upper class results in theworking class:Σ | ` t : [A]Σ ` unbox t : A

IntML Type System — Upper Class
The upper class type system identiﬁes a useful part of Int(B).
Types
X, Y ::= [A] | X ⊗ Y | A · X ⊸ Y
NIn the syntax we write A · X for A X.
Typing SequentsΣ | x1 : A1 · X1 , . . . , xn : An · Xn ` t : Y
denotes morphismO
A1

X1 ⊗ · · · ⊗OAnXn −→ Yin Int(B[Σ]).

N
The restrictions on the appearance of A are motivated byDual Light Aﬃne Logic [Baillot & Terui 2003].

Upper Class Typing Rules(Var)(LocWeak)(Congr)Σ | Γ, x : A · X ` s : Y
Σ | Γ, x : (B × A) · X ` s : Y

Σ | Γ, x : A · X ` s : X
A∼= B, e.g. 1 × A ∼=AΣ | Γ, x : B · X ` s : X

(⊸-I)

(⊸-E)

Σ | Γ, x : A · X ` x : X

Σ | Γ, x : A · X ` s : Y
Σ | Γ ` λx. s : A · X ⊸ Y

Σ | Γ ` s: A · X ⊸ Y
Σ | Δ ` t: X
Σ | Γ, A · Δ ` s t : Y(straightforward rules for ⊗)Upper Class Typing Rules(Contr)(Case)

Σ | Γ ` s: X
Σ | Δ, x : A · X, y : B · X ` t : Y
Σ | Δ, (A + B) · Γ ` copy s as x, y in t : YΣ`f: A+B
Σ, c : A | Γ ` s : X
Σ, d : B | Γ ` t : X
Σ | Γ ` case f of inl(c) ⇒ s | inr(d) ⇒ t : X([ ]-I)([ ]-E)Σ`f: AΣ | Γ ` [f ] : [A]Σ | Γ ` s : [A]Σ, c : A | Δ ` t : [B]Σ | Γ, A · Δ ` let s be [c] in t : [B]Upper Class Typing — Examples
λx. let x be [c] in [hc, ci]: α · [α] ⊸ [α × α]
λf. λx. let x be [c] in f [c] [c]: α · ([α] ⊸ [α] ⊸ [β]) ⊸ [α] ⊸ [β]λy. copy y as y1 , y2 inhlet y1 be [c] in [π1 c], let y2 be [c] in [π2 c]i: (γ + δ) · [α × β] ⊸ [α] ⊗ [β]Terms do not contain type annotations.
Conjecture: Inference of most general types is possible.
(have an implementation for the type system without rule (Cong);
uniﬁcation up to congruence is decidable).

Hacking
Have we captured all the structure of Int(B)?

Hacking
Have we captured all the structure of Int(B)?
No! Int(B) has a lot more structure!
Can we ever capture all the useful structure?

Hacking
Have we captured all the structure of Int(B)?
No! Int(B) has a lot more structure!
Can we ever capture all the useful structure?
Let the programmer deﬁne the structure he needs himself!
(Hack)

Σ, x : X − ` a : X +Σ | Γ ` hack x.a : X[A]− = 1[A]+ = A(X ⊗ Y )− = X − + Y −(X ⊗ Y )+ = X + + Y +(A · X ⊸ Y )− = A × X + + Y − (A · X ⊸ Y )+ = A × X − + Y +Complexity results remain true in presence of (Hack).

Hacking
Example: loop
loop : α · (β · [α] ⊸ [α + α]) ⊸ [α] ⊸ [α](loop f [y] if f x0 is [inl(y)]loop f x0 =[z]
if f x0 is [inr(z)]loop = hack x. case x of
| inl(y) -> let y be <store, stepq> incase stepq of| inl(argq) -> let argq be <argstore, unit> ininl(<store, inl(<argstore, store>)>)| inr(contOrStop) -> case contOrStop of| inl(cont) -> inl(<cont, inr(<>)>)| inr(stop) -> inr(inr(stop))| inr(z) -> case z of
| inl(basea) -> let basea be <junk, basea> ininl(<basea, inr(<>)>)| inr(initialq) -> inr(inl(<<>, <>>))

Hacking
Example: loop
loop : α · (β · [α] ⊸ [α + α]) ⊸ [α] ⊸ [α](loop f [y] if f x0 is [inl(y)]loop f x0 =[z]
if f x0 is [inr(z)]1αα × (α + α)
α×β×1

α
1
α×1
α×β×α

A Functional Language for Sublinear Space

1. Computation with external data
2. Deriving the functional language IntML
3. LOGSPACE programming in IntML
IntML is sound and complete for LOGSPACE.

LOGSPACE Soundness
Size bounds on working class terms follow easily from the types.
• Types bound the maximal size of closed values.
• We can read oﬀ directly from a well-typed term how big its

reducts under closed reductions can get, e.g.
kck = |A|

if c is variable of type A

khf, gik = kf k + kgk + 1
ksuccA (f )k = 12|A| + kf k...
Type variables as parameters inﬂuence the space usage linearly
Let x : A ` f : B, where A and B may contain the type variable α.
Then there exist m and n such that for any closed type C and any
closed value v of type A[C/α]f [C/α][v/x] −→∗ g

implies|g| ≤ m · |C| + n.

LOGSPACE Soundness
An upper class termt : A·(B·[α] ⊸ [3]) ⊸ (C·[P (α)] ⊸ [3])represents a LOGSPACE function on binary words.
If we consider α as a natural number then t induces a function
ϕα : {0, 1}≤α −→ {0, 1}≤P (α) .
as follows:• A word w ∈ {0, 1}≤α can be represented as a function in
hwi : B·[α] ⊸ [3] by a big case distinction.
• Then ϕα (w) is the word that (t hwi) represents.
The working-class term for t gives a LOGSPACE algorithm for thefunctionw 7−→ ϕ|w| (w) : {0, 1}∗ −→ {0, 1}∗ .

LOGSPACE Soundness
The compilation of t is a working-class term t0 of type
A×(B×1 + 3) + (C×P (α) + 1)−→
A×(B×α + 1) + (C×1 + 3).
It can be understood as an Oﬄine Turing Machine.
Given an input word w, let N = 2| × 2 ×{z· · · × 2} .
dlog(|w|)e

Evaluation of s[N /α] v needs space linear in |N | = dlog(|w|)e.
⇒ Can evaluate the output of the Oﬄine Turing Machine
represented by t0 in logarithmic space.

LOGSPACE CompletenessState of a LOGSPACE Turing Machine can be represented as aworking class value of type S(α).
Step function
input : [α] ⊸ [3] ` step : [S(α)] ⊸ [S(α) + S(α)]
step = λx. let x be [s] in
let input [inputpos(s)] be [i] in[…working class term for transition function …]
Turing Machine
M : A·(B·[α] ⊸ [3]) ⊸ (C·[P (α)] ⊸ [3])M = λinput. λoutchar. loop step init

A Functional Language for Sublinear Space
1. Computation with external data
2. Deriving the functional language IntML
3. LOGSPACE programming in IntML
Encoding of Turing Machines is a sanity check at best.
Can the language express LOGSPACE algorithms in a natural way?
• How hard is it to actually write programs?
• Do the types get in the way?
• Can we combine the special sublinear space programming

patterns with the standard ones in a useful way?

Case Studies

Assess the suitability of IntML for LOGSPACE programming byimplementing typical algorithms:• LOGSPACE evaluation of the function algebra BCε−• Graph algorithms: deciding acyclicity in undirected graphs

Function algebra BCε− [Møller-Neergaard 2004]
Restricted form of primitive recursion on binary words that captures
the functions in LOGSPACE.
• Example basic functions:

succ0 (: y) = y0
succ1 (: y) = y1(tcase(: y, t, f ) =f

if y ends with 1otherwise• Closed under composition• Closed course-of-value recursion on notation:f = rec(g, h0 , h1 , d0 , d1 ) satisﬁes
f (~x, ε : ~y ) = g(~x : ~y )f (~x, xi : ~y ) = hi (~x, x : f (~x, x>>|di (~x, x :)| : ~y ))LOGSPACE evaluation of BCε−
Møller-Neergaard proves LOGSPACE soundness by implementing
BCε− in SML/NJ:• Binary words are modelled as functions of type (N → 3).
• Function f (~x; ~y ) is implemented as SML-function of type

(N → 3) → · · · → (N → 3) → (N → 3) .
Example:type bit = int option
type input = int -> bit
fun succ1 (y1 : input) (bt : int) =if bt = 0 then SOME 1 else y1 (bt - 1))• Recursion on notation by computational amnesia[Ong, Mairson, Møller-Neergaard]

Implementing Recursion by Computational Amnesiagh0h1: (N → 3): (N → 3) → (N → 3)
: (N → 3) → (N → 3)

f = saferec(h0 , h1 , g) : (N → 3)
f (01011) = h1 (h1 (h0 (h1 (h0 (g)))))• Whenever hi applies its argument, forget the call stack and justcontinue.
• When some hi or g returns a value, we may not know what to

do with it — we have forgotten the call stack.
⇒ Remember the returned value (one bit) and its depth andrestart the computation.

[Møller-Neergaard 2004]

exception Restartn
val NORESULT = { depth = ~1, res = NONE, bt=~1 }fun saferec (g : program-(m − 1)-n)(h0 : program-m-1) (d0 : program-m-0)(h1 : program-m-1) (d1 : program-m-0)(x1 : input) . . . (xm : input)(y1 : input) . . . (yn : input) (bt : int) =let val result = ref NORESULT
val goal = ref ({ bt=bt, depth=0 })fun loop1 body = if body () then () else loop1 bodyfun loop2 body = if body () then () else loop2 bodyfun findLength (z : input) =let fun search i = if z i <> NONE then search (i + 1) else iinsearch 0
end
fun x’ (bt : int) = x1 (1 + bt + #depth (!goal))
fun recursiveCall (d : program-m-0) (bt : int) =let val delta = 1 + findLength (d x’ x2 . . . xm)
inif #depth (!goal) + delta = #depth (!result)andalso #bt (!result) = bt
then #res (!result)else
goal := { bt=bt, depth = #depth (!goal) + delta };raise Restartnendin( loop1 (fn () =>(* Loops until we have the bit at depth 0 *)( goal := { bt=bt, depth=0 };loop2 (fn () => (* Loops while the computation is restarted *)let val res =case x1 (#depth (!goal)) of
NONE => g x2 . . . xm y1 . . . yn (#bt (!goal))| SOME b =>let val (h, d) = if b=0 then (h0,d0) else (h1,d1)
in
h x’ x2 . . . xm (recursiveCall d) (#bt (!goal))endin ( result := { depth = #depth (!goal),
res = res,bt = #bt (!goal) };true )
end handle Restartn => false
0 = #depth (!result) ));#res (!result))
endControl Flowcallcc : (γ · ([α] ⊸ β) ⊸ [α]) ⊸ [α]Implemented using hack:
1
α

α

−

γ × β+

γ×β
γ×α

1
γ×1

String Diagram for parity
ResultTensorTensorDoor

TensorTensorTensorADoor

TensorDer

ADoor

Tensor

Door

Door

ADoor

Door

Contr

Axiom

Tensor

Door

Der

Axiom

Axiom

Door

Epsilon

Door

Door

TensorTensorTensorAxiom

Tensor

ADoor

Door

Der

Tensor

ADoor

ADoor

Contr

Axiom

Der

Der

Axiom

Door

Door

Der

Axiom

Contr

Door

Door

Axiom

Der

TensorContr

Der

TensorDoor

Door

TensorTensorTensorTensor

Contr

Door

Door

Der

Axiom

Contr

Door

TensorAxiom

TensorADoor

Tensor

ADoor

ADoor

ADoor

TensorDer

TensorTensorDoor

TensorDoor

EpsilonDoor

TensorADoor

TensorDoor

Tensor

ADoor

Door

Der

Der

Door

Door

Door

Axiom

Axiom

Der

TensorTensor

ADoor

Der

Contr

Door

Tensor

Door

Door

ADoor

Der

TensorTensorDer

Axiom

TensorContr

Tensor

Door

ADoor

Der

Door

Door

Door

Axiom

Contr

Der

Der

Tensor

Contr

Axiom

Der

Der

Door

Door

Door

Axiom

Contr

Door

TensorTensorDoor

Tensor

Der

Door

Der

Contr

Der

Door

Door

Epsilon

Axiom

Door

Contr

TensorDoor

TensorEpsilon

Der

Door

Door

Der

TensorTensor

Axiom

Door

Der

TensorDoor

Door

TensorDer

Tensor

ADoor

ADoor

EpsilonTensorDoor

Door

Tensor

ADoor

Contr

Contr

Door

Der

Der

ADoor

Der

TensorTensor

ADoor

ADoor

Tensor

ADoor

ADoor

Tensor

Der

ADoor

ADoor

Door

ADoor

ADoor

ADoor

ADoor

Der

ADoor

ADoor

ADoor

Door

Der

ADoor

ADoor

Door

Der

Door

Door

Contr

Der

Door

Door

ADoor

TensorADoor

Tensor

Der

Der

ADoor

Contr

Door

Contr

Axiom

Epsilon

EpsilonTensorTensorEpsilon

ADoor

Door

Tensor

Door

Der

Door

Der

Der

Der

TensorDoor

Epsilon

Epsilon

Door

Door

Door

TensorDoor

Door

TensorTensor

Door

Axiom

ADoor

Der

Door

Door

EpsilonADoor

TensorTensorTensor

ADoor

ADoor

Door

Door

Der

Axiom

ADoor

Contr

Der

Der

Door

Axiom

Der

Door

Tensor

ADoor

Door

Der

Door

Axiom

TensorEpsilonDer

TensorTensorTensorDer

Tensor

Door

Contr

Der

Tensor

Door

Door

Door

Tensor

Der

Door

ADoor

Der

ADoor

Door

TensorTensor

Door

ADoor

Door

Tensor

Door

Door

Door

Door

Axiom

TensorContr

TensorTensorDer

Contr

Tensor

ADoor

Der

ADoor

Der

TensorDoor

TensorTensorDoor

TensorTensorDoor

TensorTensorADoor

TensorDoor

TensorTensorTensorADoor

Der

Tensor

Door

ADoor

Door

Door

TensorDer

Contr

TensorDoor

Tensor

Door

Door

Door

Axiom

Axiom

ADoor

TensorDoor

Der

TensorTensor

Door

Door

Door

ADoor

Der

Door

Tensor

ADoor

ADoor

Der

Der

ADoor

ADoor

Door

Der

ADoor

Contr

Contr

ADoor

Der

Der

Door

Door

Door

Axiom

Working Class Term for parity
let (trace x9472. case x9472 of inl(x0) -> let x0 be <x5, x4> in inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(...
inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inr(inl(<x5, inr(x4)>)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))...

…5 Megabyte more(about 150 Kb if injections were represented eﬃciently)Implementing Parity

The term parity is just an example to test saferec.
The standard algorithm for parity can be implemented easily:
parity =U fun x : ['a] --o [1+(1+1)] ->letloop (fun pos_parityU : ['a * (1+1)]->
let pos_parityU be [pos_parity] inlet x [pi1 pos_parity] be [x_pos] incase x_pos ofinl(mblank) -> [inr(pos_parity)]| inr(char) ->if (pi1 pos_parity) = max then[inr(<max, xor char (pi2 pos_parity)>)]else[inl(<succ (pi1 pos_parity), xor char (pi2 pos_parity)>)]) [<min, false>]be [pos_parity] in [pi2 pos_parity];Further Work — Better Formulation of Control
Σ | Γ ` s : ⊥ | Θ, α : A
Σ | Γ ` µα. s : [A] | Θ

Σ | Γ ` s : [A] | Θ, α : A
Σ | Γ ` throw α s : ⊥ | Θ, α : A

Examplecallcc = λy. µα. throw α (y (λx. µβ. throw α x))
Equations
throw β (µα.s) = s[β/α] : ⊥µα. (throw α s) = s : [A]if α ∈/ F V (s)throw α s = s : ⊥let (µβ. throw α s) be [c] in t = µγ. throw α s

if β 6= αCase Study — Graph Algorithms

Adapt the representation of strings by[α] ⊸ [3]to([α] ⊸ [2]) ⊗ ([α × α] ⊸ [2])for graphs.
Standard pointer program for checking acyclicity in undirected
graphs can be implemented without the need for special tricks.
Can implement edge/vertex iterators as higher-order functions.

Conclusion

Space bounded computation has interesting structure,that we have only just begun to explore.
The Int construction seems to be a good ﬁrst stepfor capturing that structure precisely.
Further Work
• Stronger working class calculi: Allowing (certain) function

spaces in the working class may lead to polylogarithmic space?
• Completeness: Can we get completeness by something lesstrivial than hack?