Lambda the Ultimate

Checking polynomial time complexity with types
started 2/20/2003; 2:17:45 AM - last post 2/20/2003; 2:25:11 AM

Ehud Lamm - Checking polynomial time complexity with types

2/20/2003; 2:17:45 AM (reads: 1709, responses: 2)

Checking polynomial time complexity with types

Patrick Baillot. Checking polynomial time complexity with types. Foundations of Information Technology in the Era of Network and Mobile Computing (proceedings of TCS2002).

Several researchers have proposed programming languages with intrinsic complexity properties, for instance languages ensuring that all functions representable are PTIME without refering to an explicit time measure. This work follows the same approach.

By relegating the handling of the complexity property to the type system, the programming task becomes easier, since the programmer is freed from manually providing information needed for the complexity analysis. All well typed programs are PTIME.

But is the type system decidable? See section 4 for details!

More information can be found in the preprint Type inference for polynomial time complexity via constraints on words.

Posted to theory by Ehud Lamm on 2/20/03; 2:19:03 AM

Ehud Lamm - Re: Checking polynomial time complexity with types

2/20/2003; 2:23:48 AM (reads: 690, responses: 0)

Obviously, what you want is type inference, so that by assigning a type the system magically proves the complexity property.

Ehud Lamm - Re: Checking polynomial time complexity with types

2/20/2003; 2:25:11 AM (reads: 697, responses: 0)

By the way, remember our discussion of programs vs. data? I mentioned that a type system can ensure termination, and this caused some concern. This sort of result is even sexier...