Коллоквиум ФКН: Линейная логика и функциональное программирование. Докладчик: Степан Кузнецов (МИАН/НИУ ВШЭ)
12 февраля 2019, 18:10, ауд. 205 (Кочновский проезд, 3)
Степан Кузнецов (МИАН/НИУ ВШЭ)
Линейная логика и функциональное программирование
Линейная логика (Жирар, 1987) — это система, в которой логические формулы воспринимаются не как высказывания, а как ресурсы, которые разрешается использовать ровно один раз. В связи с этим в линейной логике отсутствуют обыкновенные для логики классической правила сокращения (ресурс A нельзя заменить на две его копии, A и A) и ослабления (каждый ресурс должен быть использован). При этом в линейной логике есть механизм, позволяющий восстанавливать эти правила в ограниченном виде и тем самым моделировать классические рассуждения. Интерес к логическим системам со стороны функционального программирования основан на изоморфизме Карри – Говарда: выражение A → B можно понимать и как логическую операцию импликации, и как обозначение для типа функций из A в B. Обыкновенным системам типов, применяемым в функциональных языках, по Карри – Говарду соответствует интуиционистская логика. Если, однако, заменить её на линейную, то система типов обогатится новыми возможностями — в частности, синтаксическим механизмом отслеживания того факта, что данный объект используется в данный момент ровно одним процессом в многопоточной среде.