Теоретическое и компьютерное моделирование логических рассуждений
2 марта 2011 в 17 часов в ГУ ВШЭ будет доклад К.А.Павлова (ИФРАН) "Теоретическое и компьютерное моделирование логических рассуждений" (инструкция как попасть и полезные ссылки: http://vic-gorbatov.livejournal.com/82950.html).
В рамках моего весеннего логического обострения хочу туда наведаться.
По ссылкам -- очень интересно, я как раз примерно это и подозревал, когда где-то полгода назад в обсуждении тезисов к программе общего верхнего образования писал "мысль про логику-как-основу-всего нужно было тут жестче провести и уж совсем явно описать" (http://ailev.livejournal.com/855472.html?thread=8133040). Только тогда меня вёл чистый нюх, а теперь я это могу как-то пытаться обосновать и дать литературу. Вот, например, из http://vox-journal.org/content/vox9-vanBenthem.doc (ссылка приведена в качестве материала к обсуждаемому докладу): Говоря в современных пост-соматических терминах, предположим, что вы озадачились вопросом о наличии пива на территории кампуса индийского университета в Бомбее. Ответ на этот вопрос вы можете попытаться, во-первых, дедуцировать из множества информации, имеющейся в буклетах, полученных вами по прибытию. Во-вторых, вы можете попробовать обойти весь кампус, используя свою способность наблюдения, чтобы непосредственно убедиться в существовании пивных заведений. И в-третьих, вместо всего этого, вы можете просто пообщаться с каким-нибудь компетентным лицом, например, местным студентом, чтобы получить исчерпывающий ответ на подобный вопрос. Более широкая концепция логики, на мой взгляд, должна включать в себя все три информативных канала как предмет своего теоретизирования; предмет, образующий согласованную картину, выводящую сферу интересов логики далеко за пределы ее гипертрофированного внимания к одному лишь только дедуктивному доказательству. Последнее в действительности есть лишь только один тип логических операций, к тому же целиком упускающий из виду сложнейшие интерактивные аспекты языка, а также и момент коммуникации между агентами логического рассуждения. Иными словами, я утверждаю, что такие коммуникативные действия как задавание вопросов, или осуществление ответных действий, являются столь же значимыми формами логической деятельности как и умение выводить следствия из имеющихся посылок.
Для меня это примерно та же постановка вопроса, с которой я всю жизнь провёл в Программировании, понимаемой мной не как "кодирование", а как именно Программирование с большой буквы. По счастью, у меня довольно много было друзей, с кем можно было подробно обсуждать такую постановку вопроса. Именно так обсуждались и экспертные системы, и агентские системы, и программирование-в-большом и много еще чего. Увы, лингвистическая или чисто философская проблематика не позволяют ставить вопрос таким образом. А логическая -- позволяет. Вот, например, я следующую цитату из этого же текста читаю прямо про наши программистские беды, а не про беды логические, как их понимает van Benthem: К примеру, говорить о логике как о науке,цель которой в значительной мере определяется поиском определенного баланса между выразительной силой формальных языков и многосложностью их использования при решении таких задач как осуществление контроля за согласованностью, адекватностью моделирования и правильностью вывода.
Ну да, чем выразительней язык (тот же Coq, или даже Scala), тем проблемней его использование. Забавно видеть, как решение (поиск баланса между формальностью/выразительностью и простотой использования) этой задачи берет на себя не столько computer science, а именно логика -- от которой еще десяток лет назад такого поворота мысли вряд ли кто ожидал.
Я думаю, что информатика будет прирастать сейчас именно логикой: но, увы, сегодня это еще та же информатика, что и десять, и двадцать, и тридцать лет назад (помним, что компьютерная революция еще не началась) -- но уже другая логика.
Кстати, Prolog когда-то был придуман для задач работы с грамматиками, чтобы писать на нём парсеры. И совсем недаром в проекте FONC стиль программирования -- это описание паттернов и связанных с ними действий, т.е. какие-то "околограмматические" рассуждения, сливающие в одно целое разборки и с синтаксисом, и с семантикой, и с прагматикой в одном "исполняющем парсере". Алан Кей всё время пишет про цель проекта STEPS/FONC как "поиск какой-то математики в решении традиционных задач программирования". У меня сейчас гипотеза, что он не математику там ищет, а логику! Ибо он бьёт в основания, а в основании именно логика, а не математика. Математика тут вторична. Но и логика тут не тридцатилетней давности, а совсем современная -- хотя и тут тоже есть некоторый застой, но отрефлектированный и уже потихоньку преодолеваемый.
В рамках моего весеннего логического обострения хочу туда наведаться.
По ссылкам -- очень интересно, я как раз примерно это и подозревал, когда где-то полгода назад в обсуждении тезисов к программе общего верхнего образования писал "мысль про логику-как-основу-всего нужно было тут жестче провести и уж совсем явно описать" (http://ailev.livejournal.com/855472.html?thread=8133040). Только тогда меня вёл чистый нюх, а теперь я это могу как-то пытаться обосновать и дать литературу. Вот, например, из http://vox-journal.org/content/vox9-vanBenthem.doc (ссылка приведена в качестве материала к обсуждаемому докладу): Говоря в современных пост-соматических терминах, предположим, что вы озадачились вопросом о наличии пива на территории кампуса индийского университета в Бомбее. Ответ на этот вопрос вы можете попытаться, во-первых, дедуцировать из множества информации, имеющейся в буклетах, полученных вами по прибытию. Во-вторых, вы можете попробовать обойти весь кампус, используя свою способность наблюдения, чтобы непосредственно убедиться в существовании пивных заведений. И в-третьих, вместо всего этого, вы можете просто пообщаться с каким-нибудь компетентным лицом, например, местным студентом, чтобы получить исчерпывающий ответ на подобный вопрос. Более широкая концепция логики, на мой взгляд, должна включать в себя все три информативных канала как предмет своего теоретизирования; предмет, образующий согласованную картину, выводящую сферу интересов логики далеко за пределы ее гипертрофированного внимания к одному лишь только дедуктивному доказательству. Последнее в действительности есть лишь только один тип логических операций, к тому же целиком упускающий из виду сложнейшие интерактивные аспекты языка, а также и момент коммуникации между агентами логического рассуждения. Иными словами, я утверждаю, что такие коммуникативные действия как задавание вопросов, или осуществление ответных действий, являются столь же значимыми формами логической деятельности как и умение выводить следствия из имеющихся посылок.
Для меня это примерно та же постановка вопроса, с которой я всю жизнь провёл в Программировании, понимаемой мной не как "кодирование", а как именно Программирование с большой буквы. По счастью, у меня довольно много было друзей, с кем можно было подробно обсуждать такую постановку вопроса. Именно так обсуждались и экспертные системы, и агентские системы, и программирование-в-большом и много еще чего. Увы, лингвистическая или чисто философская проблематика не позволяют ставить вопрос таким образом. А логическая -- позволяет. Вот, например, я следующую цитату из этого же текста читаю прямо про наши программистские беды, а не про беды логические, как их понимает van Benthem: К примеру, говорить о логике как о науке,цель которой в значительной мере определяется поиском определенного баланса между выразительной силой формальных языков и многосложностью их использования при решении таких задач как осуществление контроля за согласованностью, адекватностью моделирования и правильностью вывода.
Ну да, чем выразительней язык (тот же Coq, или даже Scala), тем проблемней его использование. Забавно видеть, как решение (поиск баланса между формальностью/выразительностью и простотой использования) этой задачи берет на себя не столько computer science, а именно логика -- от которой еще десяток лет назад такого поворота мысли вряд ли кто ожидал.
Я думаю, что информатика будет прирастать сейчас именно логикой: но, увы, сегодня это еще та же информатика, что и десять, и двадцать, и тридцать лет назад (помним, что компьютерная революция еще не началась) -- но уже другая логика.
Кстати, Prolog когда-то был придуман для задач работы с грамматиками, чтобы писать на нём парсеры. И совсем недаром в проекте FONC стиль программирования -- это описание паттернов и связанных с ними действий, т.е. какие-то "околограмматические" рассуждения, сливающие в одно целое разборки и с синтаксисом, и с семантикой, и с прагматикой в одном "исполняющем парсере". Алан Кей всё время пишет про цель проекта STEPS/FONC как "поиск какой-то математики в решении традиционных задач программирования". У меня сейчас гипотеза, что он не математику там ищет, а логику! Ибо он бьёт в основания, а в основании именно логика, а не математика. Математика тут вторична. Но и логика тут не тридцатилетней давности, а совсем современная -- хотя и тут тоже есть некоторый застой, но отрефлектированный и уже потихоньку преодолеваемый.