Логика и вычисления: философский взгляд на изоморфизм Карри-Ховарда

Связь между логикой и вычислениями сильнее, чем когда-либо, особенно после установления изоморфизма Карри-Ховарда, определяющего, что это proofsможно рассматривать как programsи formulasкак types.

Я задался вопросом, сможем ли мы найти какие-либо тексты, излагающие философскую точку зрения на связь между логикой и вычислениями. Я не смог найти ни одного документа об этом.

Кроме того, у меня есть несколько сопутствующих вопросов:

1) Поскольку большинство логических систем (например, интуиционистская естественная дедукция, классическое исчисление секвенций) соответствует вычислительным системам (например, просто типизированное λ-исчисление, система F, комбинаторная логика...), можем ли мы сказать, что логика и вычисления имеют одинаковую природу и источник ? Много затруднений вызвал вопрос о природе Логики, дает ли вычисление ответ?

2) Можем ли мы сказать, что любая система, которая не имеет общих вычислительных свойств с вычислительной системой, не является «логикой»? (например, нет теоремы об устранении разрезов, нет свойства слияния/черча-россера)

РЕДАКТИРОВАТЬ: после некоторых исследований

Единственное, что я смог найти, это работы французской группы LIGC , но большинство статей, которые они пишут, написаны только на французском языке.

Кажется, что большинство работ, связывающих философию и вычисления, касаются линейной логики (которая возникает из изоморфизма Карри-Ховарда) и лямбда-исчисления (которые дают формальное описание [функциональных] компьютерных программ).

Если я не ошибаюсь, Linear Logic берет вычисления (устранение правил сокращения, рассматриваемое как оценка программ) в качестве основы для логики. Некоторые свойства программ, такие как теорема об исключении разреза, слияние или свойство Черча-Россера, с точки зрения логики, гарантируют, что наша логика ведет себя согласованным образом. Мы полагаемся на операциональное поведение логики, а не на язык или чисто философские основания.

Похоже, эти работы еще не дошли до англоязычного сообщества, но, возможно, можно найти какие-то статьи на английском языке, написанные участниками группы.

Некоторые не слишком технические документы (к сожалению, на французском языке):

Что касается (1), теория вычислимости и теория доказательств являются ветвями (математической) логики, которая кажется интересующей вас логикой, поэтому я не понимаю, как кто-то может сказать, что они не связаны. Но помните, что понятие вычислимости является неформальным, тезис Черча-Тьюринга основан на неформальном представлении о вычислимости. Что касается (2), это зависит от того, что вы подразумеваете под «логикой», если вы просто имеете в виду любую формальную систему, то нет. Речь идет об очень простой аксиоматической, дедуктивной формальной системе, такой как система МУ Хофштадтера. Используете ли вы «логику» как синоним «формальной системы»?
Но также вы должны подумать о том, что такое «вычислительная система». Существует простой аргумент в пользу того, что даже такую ​​базовую систему, как MU, можно использовать для представления некоторого вида вычислений. Я полагаю, что Скотт Ааронсон в лекции о пределах вычислений пошутил, что можно рассматривать любую систему как вычислительную систему, даже тостер, делающий тосты, но это не означает, что это полезно. Свяжите одно из дедуктивных правил с функцией-преемником, и если вы сможете показать доказательство того, что в этом языке есть производное от некоторой строки, то вы сможете доказать некоторую арифметику.
@Not_Here (1) Я читал, что «природа» логики неясна. Может быть, я немного устарел, но некоторые, кажется, думают, что логика зависит от человеческих идей (психологизм), происходит от разума и т. д., тогда как вычисления «кажутся» исходящими от «природы». Я думал, что это может каким-то образом дать ответы на обоснование логических правил/законов или, например, основ логики.
@Not_Here (2) Я признаю, что это неясно. Я сам не уверен, но думаю, что имею в виду «логику» в неформальном смысле, тот, о котором мы думаем, когда говорим о человеческом мышлении. Может быть, у меня все еще есть наивное представление о логике, но я задавался вопросом, должны ли логические системы, не имеющие никакого соответствия системам, подобным лямбда-исчислению, пользоваться тем же статусом, что и, скажем, естественная дедукция. JY Girard однажды сказал, что он видит логику без вырезания-исключения, как автомобили без двигателя.
Разве трансцендентальный синтаксис Жирара, о котором вы спрашивали ранее, не фокусируется именно на этих типах проблем: изоморфизме Карри-Ховарда, вычислительном обосновании логических правил и т. д.? Думаю, второй вопрос заходит слишком далеко. Классическая логика при стандартной интерпретации, безусловно, не обращает внимания на вычислимость, которая кажется конструктивистской/теоретико-доказательной чертой. Модальная логика, во всяком случае версия Крипке, имеет еще более раздутую платонистскую семантику. Я бы сказал, что можно выделить логику, удобную для вычислений, но это не обязательно.
@Conifold Вы правы насчет трансцендентного синтаксиса, но мне нужны альтернативные мнения по этому вопросу. Я не хочу слишком предвзято относиться к точке зрения Жирара. Что касается классической логики, насколько мне известно, ее вычислительные свойства в настоящее время находятся в стадии изучения. Кажется, что у него все еще есть некоторое вычислительное содержание (классическая реализуемость, лямбда-µ исчисление Париго, лямбда-µ-µ~ исчисление Кюрьена и Гербелина и т. д.). Но я предполагаю, что это не то, что вы имели в виду под «стандартной интерпретацией».
Похоже, что классические применения классической логики уделяли мало внимания ее вычислительным свойствам, какими бы они ни были, и неконструктивное рассуждение появляется уже у Евклида. Если это так, то наш парадигматический пример уже показывает, что идея логики отлична от идеи алгоритма. Интуитивно, даже в вычислительных контекстах логика касается не столько вычислений как таковых, сколько проверки правильности задокументированных вычислений, она нормативна в том смысле, в каком вычисления не таковы.
центральное понятие вычислимости — это интуитивное понятие эффективной процедуры ; центральной задачей логики является интуитивное понятие (логического) следствия . Тьюринг дал нам формальную модель первого; нам все еще не хватает формальной модели первого. см. home.uchicago.edu/~wwtx иphilosophy.su.se /english /research/our-researchers/emeriti/… и следите за библиографией.

Ответы (1)

Я думаю, вы правы, что вас впечатлила переписка Карри-Ховард. Это подробный и обширный изоморфизм «правило за правилом» и «функция за функцией». Это убедительно свидетельствует о том, что доказательство и вычислимость тесно связаны. Я также согласен с тем, что она недооценивается в рамках философии логики и что мы можем и должны позволить ей влиять на наше понимание логики.

Логики любят спорить о логике. Они будут расходиться во мнениях даже по таким базовым вещам, как, например, какое объяснение давать понятию достоверности . Спросите Фреге, Куайна, Тарски, Дэвидсона, Льюиса, Правица, Этчеменди, МакГи, Брэндома и Макфарлейна, и вы получите десять разных ответов. Они также будут спорить о том, существует ли единая «одна логика, чтобы управлять ими всеми», и если да, то какая, и можно ли защитить логический плюрализм. Согласно Даммету, интуитивизм — единственный путь; для Рида это релевантная логика, для Приста паранепротиворечивая логика, для Куайна классическая логика.

Что касается вычислимости, то споров о том, как объяснить вычислимость, относительно мало. Есть некоторые вопросы по поводу того, как именно сформулировать тезис Черча-Тьюринга, применим ли он к интерактивным компьютерам, и если да, то как, и следует ли позволять таким соображениям, как законы природы, определять то, что мы можем назвать вычислением.

Итак, поскольку мы, по-видимому, довольно хорошо понимаем вычислимость и гораздо хуже логику, кажется, имеет смысл позволить нашему пониманию первого помочь нам со вторым.

Важно отметить, что соответствие Карри-Ховарда распространяется на классическую логику. Сами Карри и Ховард не знали об этом, когда формулировали переписку. Они начали с интерпретации интуиционизма БХК и использовали тот факт, что интуиционистские доказательства конструктивны, чтобы читать эти доказательства как рецепты для вычислений. Но последующие работы ученых-компьютерщиков, в том числе Гриффина, Париго, Аскьери и других, показали, что даже классическая логика разделяет соответствие. На практике это означает, что существуют вычислительные интерпретации классических систем, которые нормализуемы и позволяют извлекать вычисления из классических доказательств.

Это не означает, что любое классическое предложение вычислимо: очевидно, что существует любое количество неразрешимых предложений. Полная степень того, что можно вычислить классически, все еще остается областью исследований. Но это означает, что мы можем отказаться от упрощенческой идеи о том, что классическая логика неконструктивна, а интуиционистская логика конструктивна. Классические дизъюнкции, например, могут быть объектами доказательств без разрезов, как отметил Жирар в своей статье « Новая конструктивная логика: классическая логика» .

Чтобы ответить на ваши конкретные вопросы:

  1. Логика и вычислимость действительно тесно связаны. Однако они не идентичны. По крайней мере, вычисления происходят с течением времени и требуют какого-либо вычислительного механизма. Доказательства часто рассматриваются как абстрактные структуры, хотя любой экземпляр доказательства требует некоторой физической формы.

  2. Идея о том, что логика должна обладать некоторым вычислимым аппаратом, чтобы квалифицироваться как логика, не так странна, как может показаться. Это не исключило бы классическую логику из квалификации. Однако это строгое требование, и его могут оспорить те, кто считает, что семантика логики важнее теории доказательств.

В качестве последнего предположения я подозреваю, что связь между логикой и вычислимостью поддерживает точку зрения, согласно которой мы должны понимать логику как по существу формальную по своей природе. С точки зрения логики, преуменьшающей формальность, будет труднее объяснить связь с вычислимостью. Кроме того, некоторые очень широкие представления о том, что считается валидностью, могут быть отвергнуты на том основании, что их нельзя прямо преобразовать в вычислимую форму.

Очень понятный и интересный ответ. Я также чувствовал, что это «недооценено», как вы сказали. Теперь у меня есть несколько вопросов и замечаний. (1) Уверены ли мы, что логика и вычислимость не идентичны? Действительно ли мы понимаем, что такое доказательство? Кажется, что Ludics Жирара придают доказательствам вычислительный / интерактивный характер, я не знаю, уместно ли это в нашем контексте. (2) Что вы подразумеваете под «формальным характером» (о логике) (3) У вас нет ссылок на обсуждение переписки с философской точки зрения?
Можно возразить, что то, что поддается вычислению, ограничено законами природы. Есть несколько предполагаемых «гиперкомпьютеров», т. е. устройств, превосходящих то, что можно вычислить по Тьюрингу, но их нельзя построить в нашей вселенной. Логика обычно понимается как более абстрактная. Под «формальным по своей природе» я просто подразумеваю логические объяснения, в которых формальность является существенной чертой того, что мы понимаем под логикой, а не продуктом того, как мы ее изучаем. Есть несколько различных способов, которыми логика может быть формальной. Если вы ищете докторскую степень Джона Макфарлейна. тезис онлайн, у него есть хороший отчет об этом ...
Что касается философских отсылок к самой переписке Карри-Ховарда, то я думаю, что их очень мало: большинство дискуссий сосредоточено на технических аспектах.
Логика и вычисления: философский взгляд на изоморфизм Карри-Ховарда
СпросиСетьПолитика конфиденциальности1y, 0v