Via Dual Light Affine Logic

(1)

Verification of Ptime Reducibility for System F terms

Via Dual Light Affine Logic

Kazushige Terui

National Institute of Informatics, Japan joint work with

Vincent Atassi

^ª

Patrick Baillot LIPN CNRS University Paris 13

Verification of Ptime Reducibilityfor System F termsVia Dual Light Affine Logic – p.1/32

(2)

Characterizations of Ptime

Explicit characterization of Ptime functions:

Turing Machine

is P-clocked and computes

(3)

Characterizations of Ptime

Turing Machine

is P-clocked and computes Implicit characterizations of Ptime functions:

(4)

Characterizations of Ptime

Turing Machine

Replace Turing Machines with higher model of computation

(5)

Characterizations of Ptime

Turing Machine

Replace Turing Machines with higher model of computation Replace P-clocked with structural/logical conditions

satisfies and computes

(6)

Characterizations of Ptime

Implicit characterizations of Ptime functions:

satisfies and computes Various approaches:

Primitive Recursion Safety (Bellantoni-Cook, Leivant, . . . ) Term Rewriting PO + Quasi-Interpretation (Marion-Moyen, Bonfante, . . . ) System T Safe-Linear Types (Hofmann, Schwichtenberg. . . ) Proof Nets LLL/LAL Types (Girard, Asperti, . . . )

System F DLAL Types (Baillot-T. LICS04)

(7)

Complexity Verification

In complexity verification, more relevant is

(8)

Complexity Verification

In complexity verification, more relevant is Explicit characterization of Ptime programs:

- degree input

terminates in time

(9)

Complexity Verification

- degree input

terminates in time

- is -complete!

(10)

Complexity Verification

- degree input

terminates in time

- is -complete!

Impossible to characterize by, e.g., a “natural” type system (which is usually ).

(11)

Complexity Verification

Nevertheless, ICC is useful to provide a good approximation of

-:

- satisfies

To be practically useful,

must be a natural, expressive model of computation.

must admit many algorithms.

Complexity of is in question.

(12)

In This Talk

= System F:

reference system for studying polymorphic functional programming languages

various data types are uniformly definable

(13)

In This Talk

= System F:

= Dual Light Affine Logic (DLAL)

A refinement of Light Linear Logic. A type system for

System F lambda terms that ensures Ptime normalization.

(14)

In This Talk

= System F:

= Dual Light Affine Logic (DLAL)

A refinement of Light Linear Logic. A type system for

System F lambda terms that ensures Ptime normalization.

Main Result: Given a system F term , it is decidable in Ptime whether is typable in DLAL.

Typing guarantees that works in Ptime.

The algorithm is already implemented.

(15)

Outline

Background: System F

From Linear Logic to DLAL Main Result

Proof Idea

Example/Implementation Conclusion

(16)

Background: System F typing

Types of System F:

(Explicitly-typed) terms of system F:

with condition: in , may not occur freely in the types of free term variables of (the eigenvariable condition).

(17)

Linear Logic

Decomposition of into ^Æ .

(18)

Linear Logic

Æ uses data exactly once.

(19)

Linear Logic

can be duplicated.

Æ

(20)

Linear Logic

can be duplicated.

Æ

Modality is S4.

Linear Logic linear lambda calculus +

duplication controlled by S4-modality.

(21)

Light Linear Logic

Change the modality from S4 to K-bounded monotone one.

Æ Æ

Æ

Æ Æ

Light Linear Logic linear lambda calculus +

K-bounded monotone duplication.

(22)

Light Linear Logic

Change the modality from S4 to K-bounded monotone one.

Æ Æ

Æ

Æ Æ

Light Linear Logic linear lambda calculus +

K-bounded monotone duplication.

Why is § a K-modality?

It enforces a stratified structure on proofs.

Layers are strictly separated:

Æ Æ

It allows “layer-by-layer normalization”

(23)

Light Linear Logic

Why isn’t ! a K-modality?

Æ Æ

Æ

exponentially many ’s

(24)

Light Linear Logic

If it were, iteration would cause exponential blow-up at one layer

Æ Æ

Æ

(25)

Light Linear Logic

Æ Æ

Æ

exponentially many ’s With ! non-K, the blow-up is at most quadratic.

(26)

Light Linear Logic

Æ Æ

Æ

exponentially many ’s With ! non-K, the blow-up is at most quadratic.

Main Property: Proof net of depth normalizes in steps.

(27)

Light Linear Logic

Æ Æ

Æ

With ! non-K, the blow-up is at most quadratic.

Main Property: Proof net of depth normalizes in steps.

Light Affine Logic (Asperti 98): (Intuitionistic) LLL with full weakening.

(28)

Difficulty of LLL/LAL

Lambda terms typable in LLL/LAL do not normalize in Ptime by

-reduction.

Æ

(29)

Difficulty of LLL/LAL

-reduction.

Æ

Terms of type are sharable, but not all of them are duplicable.

(30)

Difficulty of LLL/LAL

-reduction.

Æ

-calculus confuses them. So it leads to bad exponential blow-up by -reduction.

(31)

Difficulty of LLL/LAL

-reduction.

Æ

Two solutions:

(32)

Difficulty of LLL/LAL

-reduction.

Æ

Two solutions:

Use a syntax with explicit sharing mechanism

(33)

Difficulty of LLL/LAL

-reduction.

Æ

Two solutions:

Use a syntax with explicit sharing mechanism Fobid ^Æ.

(34)

Difficulty of LLL/LAL

Typability in (propositional) LAL is decidable (Baillot 02), but is extremely complicated, because of types like

(35)

Difficulty of LLL/LAL

Type inference involves solving word-constraints over .

(36)

Difficulty of LLL/LAL

Type inference involves solving word-constraints over . Solution: Forbid .

(37)

Difficulty of LLL/LAL

Then, types look like or . Thus type inference boils down to solving (boolean and) integer-constraints.

(38)

Difficulty of LLL/LAL

We also forbid .

(39)

Difficulty of LLL/LAL

We also forbid .

! is only used as ^Æ .

(40)

Difficulty of LLL/LAL

We also forbid .

! is only used as ^Æ .

Then why don’t you come back to ? — DLAL.

(41)

Dual Light Affine Logic

DLAL seen as a refined type system for system F terms.

(42)

Dual Light Affine Logic

Types of DLAL:

(43)

Dual Light Affine Logic

Types of DLAL:

The erasure map to System F types:

(44)

Dual Light Affine Logic

Types of DLAL:

is a decoration of a system F type if .

(45)

Dual Light Affine Logic

Types of DLAL:

is a decoration of a system F type if .

Judgements: of the form , where is a system F term, contains non-linear variables, and linear variables.

(46)

Dual Light Affine Logic

(Id)

½

( i) ^½^½ ^¾^¾

½

¾

½

¾

( e)

½

( i) ^½^½

½

( e)

½

¾

½

¾

(Weak)

½

¾

½

¾

(Cntr)

½

( i)

½

¾

½

¾

½

¾

( e)

½

( i) (*)

½

( e)

(47)

Dual Light Affine Logic

(Id)

½

( i) ^½^½ ^¾^¾

½

¾

½

¾

( e)

½

( i) ^½^½

½

( e)

½

¾

½

¾

(Weak)

½

¾

½

¾

(Cntr)

½

( i)

½

¾

½

¾

½

¾

( e)

½

( i) (*)

½

( e)

(48)

Dual Light Affine Logic

(Id)

½

( i) ^½^½ ^¾^¾

½

¾

½

¾

( e)

½

( i) ^½^½

½

( e)

½

¾

½

¾

(Weak)

½

¾

½

¾

(Cntr)

½

( i)

½

¾

½

¾

½

¾

( e)

½

( i) (*)

½

( e)

(resp.

) corresponds to abstraction on a linear

(resp. non-linear) variable,

(49)

Dual Light Affine Logic

(Id)

½

( i) ^½^½ ^¾^¾

½

¾

½

¾

( e)

½

( i) ^½^½

½

( e)

½

¾

½

¾

(Weak)

½

¾

½

¾

(Cntr)

½

( i)

½

¾

½

¾

½

¾

( e)

½

( i) (*)

½

( e)

an argument

of a term

of type

must have at most one occurrence

of free variable, which is linear.

(50)

Dual Light Affine Logic

(Id)

½

( i) ^½^½ ^¾^¾

½

¾

½

¾

( e)

½

( i) ^½^½

½

( e)

½

¾

½

¾

(Weak)

½

¾

½

¾

(Cntr)

½

( i)

½

¾

½

¾

½

¾

( e)

½

( i) (*)

½

( e)

the rule (

i) allows to turn linear variables (in ) into

non-linear ones.

(51)

Dual Light Affine Logic

(Id)

½

( i) ^½^½ ^¾^¾

½

¾

½

¾

( e)

½

( i) ^½^½

½

( e

½

¾

½

¾

(Weak)

½

¾

½

¾

(Cntr)

½

( i)

½

¾

½

¾

½

¾

( e

½

( i) (*)

½

( e)