Hello, I'm Romain Péchou from L'Oréal Laboratory in Nancy, France and I'm going to present you a tier-based type programming language characterizing feasible functionals

a joint work with Emmanuel Henry, Andrew Imarion from L'Oréal and Bruce Capron from University of Victoria So, our goal is to study polynomial time complexity At type 1, everything is well known

There have been several tools that have been designed for program analysis I'm thinking to type systems, such as a type system based on linear logic and its variants interpretation methods, and a lot of other techniques that have been developed by the people of the implicit computational complexity for 30 years

At type 2, we are in the setting of function-sticking functions as input and some complexity classes have been defined, and there are no tractable tools and even no tools at all Some programming languages with semantic restrictions have been defined

I'm thinking to BTLP and ITLP from Irvin Capron and Royé But the semantic restriction makes programming discipline very hard So the goal of this talk will be to find, develop a static analysis technique for certifying type 2 polynomial time complexity

Type 2 polynomial time is a complexity class that has been defined by Mellon in 1976 and it has also been characterized by Cook and Urquhart in 1993 So in particular, you take a set of constant functions

to be the functions computable in polynomial time at type 1 plus some particular kind of recursors defined below And you see that by taking the simply typed lambda closure of this

and restricting everything to type 2 we characterize exactly the class of functions computable in polynomial time at type 2

Another interesting characterization was provided by Cook and Capron in 1990 So the set of type 2 polynomial time computable functions is defined in terms of oracle Turing machine where oracle Turing machines are just Turing machines with special tape with an oracle

And the functions computable at type 2 in polynomial time are exactly the ones that can be computed by an OTM running in polynomial time

in the size of the oracle and in the size of the input So here the size of the oracle is the maximal output of the oracle for some bounded input And you can see that the polynomial is type 2 polynomial

So in particular you have type 0 variables and type 1 variables and you can apply type 1 variables to type 0 data One of the main open problems was how to get rid of type 2 polynomials

because type 2 polynomials are very difficult to check and to infer And one option was suggested by Cook in 1992 So it's called oracle polynomial time, OPT

So define for some given oracle phi and input A, M to be the maximal size of the input A and the maximal size of an oracle answer in the run of the machine M on oracle phi and input A

So an OTM is in OPT if its runtime is bounded by P of M for any input and for some fixed type 1 polynomial P

However, it is well known that BFE for FP2 is strictly contained in OPT because OPT contains exponential functions Consequently, as FP2 is strictly included in OPT

one question of interest is how to recover this class using OPT The first suggestion was made by Kawamura and Steinberg and it is called finite length revision So an oracle Turing machine will have finite length revision

if for any input the number of times the oracle answer has a size bigger than the sizes of all the previous oracle answers is bounded by a constant So look at the two examples below

So in the first example, we have a while loop and the variable x is decreasing and clearly, if we take a strictly decreasing function as oracle the number of times the oracle size is going to increase

will not be bounded by a constant So this program has no finite length revision On the other side, the variable is increasing but every time we take the variable output in y we check that y is bounded by 8

and this program has a finite length revision and the constant is 8 There was another suggestion by Kapur and Steinberg called finite look ahead revision and now we see that an oracle Turing machine has finite look ahead revision even if for any input the number of times a query is posed

whose size extends the size of the previous queries is bounded by a constant So now instead of looking at the output we look at the oracle input So take again the same programs The one on the left now has a finite look ahead revision

with constant zero and this one on the right has no finite look ahead revision So in particular, if we take the oracle to be this constant function then it is not bounded by a constant

Then we define the class of strongly polynomial time to be the intersection of OPT and finite length revision and we define the class of moderately polynomial time to be the intersection between OPT and finite look ahead revision

First, these two classes are strictly included in FP2 but there was a result by Kapur and Steinberg at least 2018 showing that if we take constant in these two classes and we take the simplified lambda closure

from this and restrict everything to type 2 then we recover the set of functions computable in polynomial time at type 2 So to make a summary We want to develop a static analysis tool

for certifying type 2 polynomial time complexity We want the tool to be tractable so we want to get rid of the type 2 polynomials But we want also the tool to be automatic So in particular, we do not want to explicitly provide the polynomial

and this is why we need some kind of tool like the one developed by the implicit computational complexity So the idea is to take such a tool and to adapt it at type 2 to combine it with the MPT technique

in order to characterize the type 2 polynomial time complexity The tool we have in mind is safe recursion or tiering and the programming language we are going to analyze is a small imperative programming language with oracles

So let's make a brief reminder about what safe recursion and tiering techniques are Safe recursion was introduced by Belantoni and Cook and tiering was introduced by Levent So the main intuition is that you take the data and you split them in two categories

Tier 1 and Tier 0 Tier 1 will be the one driving recursion whereas Tier 0 cannot drive recursion and in particular, a Tier 1 data can jump to a Tier 0 position but the converse cannot hold

so that you have a forbidden flow of data from 0 to 1 The theorem by Belantoni and Cook is as follows If you take a class of functions containing some basic functions such as constant, projection, successor, etc and then you close them by composition and by safe recursion

using some previously defined functions of the class then you characterize exactly the class of functions computable in polynomial time at type 1 So let's start with a brief summary of the results

that hold for tiering for imperative programming languages So in particular we take a very small imperative programming language standard 1 with assignments, while loops, conditionals, sequence and all that and we assume that there are some basic operators inside

We still take a domain with two elements that are called tiers and we assume that 0 is smaller than 1, quickly Now the intuition is as follows The tier 0 are data that may grow but they cannot control the program flow, so the conditionals or the while loops

In opposition, tier 1 data are data that cannot grow but they may control the program flow The type system is inspired by non-interference based type systems

For most of the rule, the tier 2 is preserved but there are some particular rules to mention For assignments, when we assign the result of an expression e to a variable x we check that the type of x is smaller than the type of e

so that information may flow from 1 to 0 but not the converse For an operator, we split operators in two categories the destructor and the constructor and when the operator is a constructor we enforce the output tier to be 0

because the data may increase Then, in a while loop, we enforce the tier of the guard to be 1 so that the while loop will only be driven by tier 1 data

Let's mention that our type system has also a subtyping rule but only for commands A command of tier 0 may be typed by 1 but not the converse and this does not hold at all for expression This type system has been extended to more general operators

in particular, polynomial time computable operators You can type an operator with tiers but there are some safety rules to check The first one is that if the operator is computing a predicate

then the output is smaller than the minimum tier of the input so it prevents information to flow from a tier 0 to a tier 1 and then, for any operator that is smaller than the maximum of the size of its input

plus some positive constant then we enforce the output tier to be 0 Let's consider some examples First addition

Here, in this example, you see that the tier of Y is necessarily 0 because here the data is increasing so this expression is of tier 0 and the tier of Y has to be smaller than the tier of this expression so it's enforced to be 0 The tier of X is enforced to be 1

because here X appears in the guard of the while loop So you can type the add program and you can give it this type Now consider the multiplication program and assume for simplicity that we have non-recursive procedures

So here, because of the previous example the output of add is known to be of tier 0 So the tier of Z is smaller and is enforced to be 0 Y is enforced to be of tier 1 because it appears at the left hand side of the add procedure

and X is enforced to be of tier 1 because it appears in the guard of the while loop So the tier of MULT is the following one Now we consider the exponential as a counter example

Here in this example we know that Y is of tier 1 because it is used by the add procedure but the return type of the addition is 0 so it has also to be of tier 0

so X cannot be type which is kind of expected Based on this type system, characterization of polynomial time at type 1 was obtained by Marium so the set of functions computable in polynomial time at type 1

is exactly the set of functions computable by typable and terminating programs This result has been presented by Marium at least 2011 and we have shown at FOSACS 2013 that the type inference can be done in polynomial time by a reduction to 2SAT

Now let's turn back to the imperative language with oracle So we want to design a type system ensuring that programs are in MPT So we consider the same language as previously but we add oracle calls in expressions

So you see that in an oracle call phi of w on point v there are two data w is the oracle input and v is the oracle input bound

So the intuition is as follows If the size of w is smaller than the size of v then we just have a standard call to phi on w and the computation is done in a standard way However, if the size of w is greater than the size of v

then we perform a truncation on w and we will only call the oracle on this location So now we want to design a type system For ensuring the computed function to be in MPT

There are several observations that we can perform So first, the Leukoid revision can be controlled by tiers Observation 1 The problem is that you want a constant number of Leukoid revisions whereas usually in previous systems there were only two tiers

So the solution is to use more than two tiers The second observation is that a restriction on the oracle input bound is needed to enforce the final Leukoid revision

And this will be achieved by the introduction of a new tier that is called Kout that will keep the information on the tier of the outermost wild Leukoid The third observation is that operators are in need of a more flexible treatment

because depending on the place where the operator is called we need to be able to give a distinct type to operator And this will be performed by the introduction of KIn

that keeps track of the tier of the innermost wild Leukoid So finally, judgment will be of this shape So we have a type assignment for variables a type assignment for operators

and every command has a triple of tiers the tier of the command, the innermost tier and the outermost tier Let's start with the easy part of this type system So if you think to the previous type system on an imperative program

that I have just shown and you forgot everything about the innermost and outermost tier then we more or less turn back to the same type system So we still have subtyping and then all the other rules are similar

So let's now look at the non-trivial rules mostly the rules for operators, the rules for oracles and the rules for while loops So for operators, in order to be able to type an operator clearly the operand needs to be of the right tier

but also we have to check that the type of the operator is an admissible type with respect to the typing environment So what does it mean? In particular, the output tier has to be smaller than the input tiers

This is standard to what we had previously on safe operators on imperative programs but the maximal input tier has also to be smaller than the innermost tier which will constrain the way we can use the type of operators

with respect to the tier of the innermost loop where we are And then, last condition the output tier has to be strictly smaller than the innermost tier and if you think to the previous case we were asking the positive operator

so that computes some data that may increase to have tier 0 So this is a similar and equivalent statement for a type system with more than two tiers So now let's look at the oracle rule When we type the oracle rule

we will type the oracle input in a standard way but this will be a bit different for the oracle input bound and in particular we ask the tier of this oracle input bound to be the outermost tier

And then we look at the while loop typing rule and we see that for the guard it's kind of standard but we ask the tier to be greater than 1 there is no while loop for t0

and when we tier the inner command then we update the innermost tier to k This program tests whether there is an integer smaller than the input for which the oracle outputs 0 It is computing a function in MPT

and it is also typable and in particular the innermost tier is equal to the outermost tier that is equal to the tier of x1 and because y is used as the oracle input data it is enforced to be a tier strictly smaller, that is 0

Finally, we obtain the following results Let ST be the class of typable and terminating programs First, a soundness result ST is included in the simply typed lambda closure of MPT restricted to type 2 and then we have completeness results

At type 1, ST is equal to FP and at type 2, the simply typed lambda closure of ST is equal to FP The proof at type 1 holds by showing that Marion's type system is strictly included in ST1

while the proof of completeness at type 2 is shown by simulating a variant of the OR recursion scheme introduced previously We have presented two characterizations of polynomial time at type 1 and type 2 and the one at type 2 is a strict natural extension of the one at type 1

The corresponding type system has a type inference that is decidable in polynomial time and in particular, the termination requirement can be specialized to some decidable termination criterion such as the size change principle

There are still open issues, so how to get rid of the lambda closure What termination techniques can we combine with our technique? Are there other extensions to improve the expressive power as we have false negatives?

Let me thank you for your attention