• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

Коллоквиум ФКН: Линейная логика и функциональное программирование. Докладчик: Степан Кузнецов (МИАН/НИУ ВШЭ)

16+
Мероприятие завершено

12 февраля 2019, 18:10, ауд. 205 (Кочновский проезд, 3)

Степан Кузнецов (МИАН/НИУ ВШЭ)

 
Линейная логика и функциональное программирование

Линейная логика (Жирар, 1987) — это система, в которой логические формулы воспринимаются не как высказывания, а как ресурсы, которые разрешается использовать ровно один раз. В связи с этим в линейной логике отсутствуют обыкновенные для логики классической правила сокращения (ресурс A нельзя заменить на две его копии, A и A) и ослабления (каждый ресурс должен быть использован). При этом в линейной логике есть механизм, позволяющий восстанавливать эти правила в ограниченном виде и тем самым моделировать классические рассуждения. Интерес к логическим системам со стороны функционального программирования основан на изоморфизме Карри – Говарда: выражение A → B можно понимать и как логическую операцию импликации, и как обозначение для типа функций из A в B. Обыкновенным системам типов, применяемым в функциональных языках, по Карри – Говарду соответствует интуиционистская логика. Если, однако, заменить её на линейную, то система типов обогатится новыми возможностями — в частности, синтаксическим механизмом отслеживания того факта, что данный объект используется в данный момент ровно одним процессом в многопоточной среде.

Афиша

Регистрация

Все Коллоквиумы ФКН