Аннотация:
Я расскажу о мягкой линейной логике. Она позволяет моделировать системы присвоения типов в лямбда-исчислении, которые характеризуют сложностные классы P, NP и PSPACE. А именно, любая задача из данного класса может быть представлена как задача приведения термов определённого рода к нормальной форме. Также я обсужу понятие корректности соответствующих лямбда-исчислений в классах P, NP и PSPACE.