Логика в программировании

Конспект статьи Liu et al. - From logic to programming (2025)

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

Статья выявляет, как в процессе возникновения фундаментальных проблем в логике, математике и теории вычислений образовалась современная наука и технологии. Наряду с философскими следствиями теоремы Гёделя о неполноте, языки формальных логических систем, как и построение доказательства теорем с помощью вывода из аксиом, приводят к неполноте возможностей логического выражения и умозаключений по сравнению с человеческой интуицией, восприятием и сознанием. Пожалуй, это фундаментальные факторы, отличающие человеческий интеллект от машинного (т.е. ИИ).

Введение

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

Эта статья представляет обзор следующих направлений.

• Истоки и формализация логики. Обсуждается логика, основанная на естественном языке. Естественный язык имеет свои ограничения. Аристотель сформулировал формальную логику, включающую силлогизмы. Обсуждаются принципы символической логики. Возникновение математической логики после работ Гильберта и др. по формальным языкам, системам доказательств и моделям. В дальнейшем возникла метатеория формально-логических систем, она затронула такие фундаментальные вопросы, как: непротиворечивость логических систем, корректность, адекватность, полнота и разрешимость. Мы обсудим теорему Гёделя о неполноте и ее философские следствия, включая творческие способности человека и машины.

• Возникновение современных моделей вычислений. Развитие современных вычислительных моделей последовало за ответом на программу Гильберта после доказательства теорем Гёделя. С развитием нашей цивилизации стали развиваться средства вычислений. Ранняя история вычислительных приборов включает изобретение абака и пр. в работах Паскаля, Лейбница и Бэббиджа. Определение рекурсивных функций было дано Гёделем, что стало “поворотной точкой” между логикой и вычислениями. Впоследствии в работах Аккермана, Клини и Чёрча сформировалась теория вычислимости. Разработанное Чёрчем λ-исчисление продемонстрировало, что сформулированная Гильбертом и Аккерманом проблема разрешимости не может быть решена, что приводит к понятию вычислимости. Примерно в то же время Тьюринг предложил машины Тьюринга, чтобы лучше прояснить понятие вычислимой функции. И хотя главной целью Тьюринга было показать, что проблема разрешимости Гильберта и Аккермана не может быть решена, его работы сформировали перспективы для проведения вычислений. В дальнейшем с помощью тезиса Чёрча и тезиса Тьюринга-Чёрча было доказано, что три модели - рекурсивные функции, λ-исчисление и машины Тьюринга - эквивалентны в своей вычислительной способности. Вместе эти модели стали теоретическим основанием современных цифровых вычислений, хотя изначально их цель была в том, чтобы найти ответы на вопросы, поставленные в программе Гильберта. Теоретические модели вычислений совершили революцию в области вычислений. Однако все они имеют логическую природу и поэтому обладают ограничениями, характерными для формальных систем, как следует из теорем Гёделя и теорем о неразрешимости Чёрча и Тьюринга. Эти ограничения касаются глубоких вопросов о человеческом и искусственном интеллекте, способности ИИ к созданию инноваций, логическом выводе, планировании и объяснимости систем искусственного интеллекта.

• Появление цифровых компьютеров и теории языков программирования. Середина XX века ознаменовалась созданием программируемых компьютеров, начиная с машин таких, как ENIAC и Colossus. Архитектура фон Неймана остается основой современных компьютеров, делая возможной автоматизацию сложных вычислений, что привело к цифровой революции. С тех пор произошло существенное развитие языков программирования и инструментальных платформ для разработки, благодаря эволюции программных абстракций. Сначала произошел прогресс от машинных языков к символическим ассемблерам и затем к языкам программирования высокого уровня с компиляторами и интерпретаторами; далее возникли абстрактные типы данных, модульность, объектно-ориентированное программирование и т.д. Следовательно, проектирование и реализация языков программирования стали центральной частью компьютерных наук и системной инженерии. Мы обсудим естественную взаимосвязь между математической логикой, моделями вычислений и языками программирования. Языки программирования - это формальные языки, их синтаксис и семантика определяется аналогично языкам формальной логики. Эта взаимосвязь подтверждает мысль, что всякое вычисление можно представить как построение доказательства, что было показано Тьюрингом и Постом. Чтобы это проиллюстрировать, мы введем минимальный (но полный по Тьюрингу) язык программирования вместе с операциональной семантикой языка, денотационной семантикой и аксиоматической семантикой в логике Хоара. Мы обсудим взаимосвязь между этими семантическими моделями и то, как они соотносятся к алгебраической семантикой.

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

Формализация логики

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

Термин “логическая система” обычно относится к специальной системе, состоящей из правил формулирования, рассуждения или доказательства утверждений.

Логика охватывает множество областей, от науки, инженерии и технологии до лингвистики, гуманитарных и социальных наук, права. Например, определяя понятие, необходимо уточнить и оценить его правильность, чтобы удостовериться в его осмысленности. Делая утверждение или суждение, всегда ставится вопрос о его логичности.

Зачем нужна логика? Всякая система: инженерное устройство, социальная организация или отдельный человек - ведет себя согласно определенной логике. Последовательность суждений обеспечивает гармоничное и правильное функционирование при проектировании, использовании или интеграции любой системы. Прикладные концепции понятности (объяснимости), достоверности и надежности берут свое начало в логике. Логическая непротиворечивости, целостность и полнота упомянутых систем имеют решающее значение для их стабильности, эффективности и надежности.

Формализация логики. Древние участники дебатов и философы изначально пользовались логикой в рамках естественных языков. Неточная структура естественного языка приводит к неоднозначности трактовок, что служит причиной парадоксов. Китайский парадокс: “Если белые лошади - это лошади, то черные лошади - это лошади. Значит, белые лошади - это черные лошади.”

При отсутствии логической структуры сложно избежать в рамках высказывания ссылок на само же это высказывание. Парадокс лжеца: “это утверждение ложно”. Парадокс брадобрея, или парадокс Рассела: противоречие с возможностью определить любое множество как “коллекцию различимых объектов”. Если определить множество всех множеств, не содержащих самого себя в качестве элемента, \(Y = \{S \colon S \notin S\}\), а потом спросить, принадлежит ли это множество самому себе, т.е. \(Y \in Y\), приходим к противоречию.

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

Парадокс Рассела и аксиоматизация теории множеств. Парадокс Рассела стал причиной кризиса в теории множеств как основании математики. За ним последовали многочисленные усилия, направленные на то, чтобы обойти этот парадокс.

Рассел разработал теорию типов, которая предлагает рассматривать иерархическую структуру, состоящую из множеств, определенных на разных слоях. Множество, находящееся на некотором слое, не может быть определено через множества, находящиеся на более нижних слоях. Стоит отметить, что архитектуры многих инженерных систем построены по аналогичному иерархическому принципу.

Другой подход известен как теория множеств Цермело. Она предшествовало современной теории Цермело-Френкеля (ZF) и ее расширениям, таким, как теория множеств Неймана-Бернайса-Гёделя (NBG). На сегодняшний день, в сочетании с аксиомой выбора (аббревиатура ZFC), теория множеств ZF служит стандартной формой аксиоматической теории множеств. Эта теория рассматривается как наиболее важная составляющая оснований математики.

Программа Гильберта и теорема Гёделя о неполноте. В конце XIX - начале XX в. Гильберт привлек значительное внимание к основаниям математики. Сосредоточившись на геометрических аксиомах, Гильберт высказал идею, чтобы свести вопрос о непротиворечивости геометрии к непротиворечивости анализа, интерпретируя геометрическую систему в рамках действительной плоскости. Однако доказательство непротиворечивости его аксиоматизации столкнулось с значительными трудностями ввиду допущений анализа Дедекинда, примерно как и с парадоксом Рассела в теории множеств.

Гильберт подчеркивал важность доказательств непроворечивости аксиоматических систем: “Главное требование теории аксиом должно идти дальше (чем просто избегать известных парадоксов), а именно аксиомы должны давать возможность показать, что в каждой области знания противоречия, основанные на лежащей в ее основе системе аксиом, абсолютно невозможны.”

Помимо вопроса о непротиворечивости, Гильберт интересовался и другими проблемами аксиоматизации, такими, как “разрешимость всякого математического вопроса”.

Сформулированная Гильбертом программа предназначалась для разрешения фундаментального кризиса в математике того времени. Вот цели программы Гильберта:

1. Формальная логическая система для математики: все математические утверждения следует выражать на точном формальном языке и действовать с ними в соответствии с корректно определенными правилами.

2. Полнота: доказательство, что все истинные математические утверждения можно вывести в рамках введенного формализма.

3. Непротиворечивость: доказательство, что в рамках формализма не возникает противоречий. В идеале это доказательство должно использовать только “конечностные” рассуждения о конечных математических объектах.

4. Консервативность: доказательство, что всякий результат о “реальных объектах”, полученный с помощью рассуждений над “идеальными объектами” (такими, как несчетные множества) также можно доказать, не прибегая к идеальным объектам.

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

Однако в 1930 г. Гёдель показал, что большая часть целей этой программы недостижима. Это вытекает из теорем Гёделя о неполноте и результатов Чёрча и Тьюринга о неразрешимости. Теорема Гёделя дает понять, что всякая непротиворечивая логическая система, с помощью которой можно выразить арифметику, будет неполной; всегда будут истинные утверждения в рамках этой системы, которые не могут быть доказаны. Несуществование алгоритма, выясняющего истинность произвольного математического утверждения, показано Чёрчем и Тьюрингом - таким образом, проблема разрешимости Гильберта-Аккермана (известная также как Entscheidungsproblem) не имеет решения.

Теория вычислимости. Хотя программа Гильберта оказалась невыполнимой, многие исследования в математической логике и математике являются продолжением этой программы. Стремление формализовать математику играло важную роль в обходе многочисленных математических парадоксов и помогло создать новые области математики и науки.

Влияние формальной логики и ее формализации выходит далеко за рамки самой математики; благодаря логике возникли и развились компьютерные науки. Доказательство Гёделем его первой теоремы о неполноте ознаменовало начало развития теории рекурсивных функций. Теория рекурсивных функций и доказательство теоремы о неполноте сильно повлияли на развитие λ-исчисления и определение машин Тьюринга, которые изначально предназначались для того, чтобы показать, что проблема разрешимости Гильберта-Аккермана не имеет решения. Теория рекурсивных функций, λ-исчисление и теория машин Тьюринга формируют современную теорию вычислимости.

Компьютерные науки и программная инженерия. Модель компьютера с хранимой программой, которая носит название фон-неймановской архитектуры, была предложена фон Нейманом в 1945 г. Она была основана на модели универсальной машины Тьюринга. Эта концепция открыла дорогу к разработке языков программирования и абстракций программного обеспечения, и формальная логика здесь - твердое основание.

Ранняя форма формальной логики. У естественного языка есть свои ограничения, затрудняющие правильные рассуждения и планирование. Естественного языка недостаточно для строгого мышления, с его помощью затруднительно сформулировать процессы рассуждений и определить правильность рассуждений. Развитие формальной логики началось с основополагающей работы Аристотеля. Мыслитель предложил три ключевые идеи, на которых построена формальная логика. Его идеи оказали значимое влияние на логику, философию, современную науку и технику.

Одна из идей Аристотеля - отделить форму рассуждений от их содержания. Это значит, что правильность рассуждений определяется прежде всего их формой, а не конкретным содержанием предпосылок. Это ранняя идея формализации логических выводов, в которых рассуждения касаются только структуры выводов. Другими словами, корректность логических рассуждений зависит только от формы выводов и не зависит от содержания предмета.

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

Искусственные символы. Аристотель объяснил ограничения естественного языка и предложил использовать искусственные символы. Формальные языки, как в современной формальной логике, он изобретать не стал. Аристотель использовал греческие буквы в своих обозначениях.

В своей работе “Первая аналитика” Аристотель ввел понятие силлогизма. Впоследствии на принципы Аристотеля опирался логик Фреге в своей книге “Язык формул для чистой мысли, основанный на арифметике”. Подход Аристотеля к логике отражает его философию в целом, известную как “Метафизика”. В философии Аристотеля все вещи представляются как единство формы и содержания.

• Форма: Структура и организация объекта. Определяет первичную функцию, назначение и сходство между объектами одного типа.

• Содержание: Разные части, из которых состоит объект. Определяет конкретные свойства объекта, характеристики и индивидуальность.

Для понимания природы любого объекта нужно учесть как форму, так и содержание. Форма дает организационную структуру, а содержание отражает отдельные характеристики объекта. Это соотношение между формой и содержанием имеет далеко идущие следствия за рамками логики и математики (где важны изоморфизмы и гомоморфизмы между алгебраическими структурами), расширяясь до гуманитарных и естественных наук, техники. В этих дисциплинах организационная структура, системная архитектура и алгебраические структуры часто проявляют гомоморфизмы и изоморфизмы, отражая единство формы и содержания. Эти идеи имеют фундаментальное значение в проектировании целостных и эффективных систем, относясь будь то к человеческим организациям, научным моделям или техническим структурам.

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

Центральная часть этого определения - “с необходимостью вытекает”. Это соответствует современному понятию логического следствия: мы говорим, что \(X\) с необходимостью вытекает из \(Y\) и \(Z\), если ситуация, в которой \(X\) ложна при том, что \(Y\) и \(Z\) одновременно истинны, является невозможной. Такой вывод оказывается правильным по своей форме.

В формальной логике предполагаемые вещи называются посылками (т.е. \(Y\) и \(Z\)), а другая вещь, с необходимостью вытекающая из посылок, - это заключение. Чтобы рассуждение было правильным, посылки и заключение должны быть связаны подходящим образом. Вывод по силлогизму состоит из главной посылки, побочной посылки и заключения, которое с необходимостью следует из посылок. Вот пример вывода по силлогизму:

Главная посылка: Все люди смертны.

Побочная посылка: Цинь Шихуанди - человек.

Заключение: Следовательно, Цинь Шихуанди смертен.

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

Главная посылка: Некоторые музыканты - пианисты.

Побочная посылка: Лан Лан - музыкант.

Заключение: Следовательно, Лан Лан - пианист.

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

Назовем сказуемое заключения основной частью вывода (обозначим ее через \(P\)), сказуемое побочной посылки - это средняя часть вывода (обозначим ее через \(M\)), и подлежащее заключения - это побочная часть вывода (обозначим ее через \(S\)). Средняя часть (M) входит в обе посылки, но не входит в заключение, она служит связкой между подлежащим и сказуемым. Стандартный силлогизм можно сформулировать с помощью символов так:

Главная посылка: Все \(M\) суть \(P\).

Побочная посылка: \(S\) суть \(M\).

Заключение: \(S\) суть \(P\).

Всего существует четыре различных конфигурации: \((MP, SM, SP)\), \((PM, SM, SP)\), \((MP, MS, SP)\), \((PM, MS, SP)\), причем слова “все” и “некоторые” (возможно, с частицей “не”) относятся к \(P, M, S\). Всего получаем 256 типов силлогизмов. Известно, что лишь 24 из них правильны.

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

Формально-логические системы. Хотя логика силлогизмов Аристотеля заложила основы формальной логики, она не могла вполне достичь целей формализации, общности и механизации. Американский логик Льюис внес свой вклад в разработку символической логики, введя три ключевые характеристики, которым должна удовлетворять формальная логика:

1. Использование символов для понятий: В формальной логике символы представляют понятия. Например, символ \(\times\) обозначает умножение, и в языках программирования с той же целью пользуются символом *. Символы позволяют достичь абстракции и обобщенности логических рассуждений.

2. Метод логического вывода (дедукции): В формальной логике используется дедуктивный метод, позволяющий получить бесконечно много новых структур из конечного множества простых структур. Из нескольких основных структур получаются сложные процессы. Это обеспечивает возможность систематически получать новые выводы из принятых посылок.

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

Мы можем определить, что составляет формально-логическую систему, согласно этим принципам.

Определение. Формально-логическая система \(\mathcal S\) определяется несколькими компонентами, которые вместе создают структурированную платформу для рассуждений. Вот ключевые компоненты формально-логической системы:

• Алфавит: Множество символов, используемых в этой системе.

• Формальная грамматика: Множество синтаксических правил, определяющих, как могут быть выстроены символы алфавита, чтобы образовать правильные предложения или формулы.

• Правила вывода: Множество правил, определяющее, как одну формула можно пошагово вывести из заданного множества формул (оно может быть пустым), называемых посылками. Эти правила регламентируют процессы логического вывода в системе.

Правило с пустым множеством посылок называется аксиомой.

Итак, формальная система состоит из двух главных частей: формального языка и системы выводов (доказательств). Формальный язык обеспечивает структуру для выражения логических утверждений, а система выводов предлагает правила для получения новых утверждений и проверки правильности логических рассуждений.

Формально-логические системы упрощают точное формулирование и строгий анализ логических утверждений и их формальных доказательств, гарантируя, что выводы получены систематически и надежно. Изучение формально-логических систем также выявило важность формальных или полуформальных языков, таких, как математический язык, языки компьютерного программирования и языки спецификаций (или языки моделирования), вдобавок к формальным языкам логических систем. Если говорить о существенных преимуществах символических языков над прочими языками, в том числе естественными, можно процитировать Льюиса:

“… Во-вторых, идеографическая запись превосходит любую другую по точности. Многие идеи, выражаемые математическими символами, могут быть переданы обычным языком только с величайшими трудностями. Даже арифметика была бы сложной без идеограмм, а более высокие уровни были бы невозможны.” (“Обзор символической логики”, 1918 г.)

Формально-логические системы с гильбертовскими системами доказательств широко используются в науке. Как предложили Гильберт и Аккерман в книге “Принципы математической логики”, эти системы определяют аксиомы и правила вывода в схематической форме. В гильбертовских системах используется много схем аксиом и мало правил вывода.

В другом классе систем, называемых системами естественного вывода, напротив, вводится много правил вывода, но очень мало схем аксиом. Ниже мы представим вариант гильбертовской системы для исчисления предиктов первого порядка.

Определение. Язык логики предикатов первого порядка \(\mathcal L\) определяется с помощью следующих синтаксических категорий.

• Алфавит \(\Sigma\), состоящий из таких символов:

  • \(A = \{a_1, a_2, \ldots \}\) - индивидные константы;

  • \(X = \{x_1, x_2, \ldots\}\) - индивидные переменные;

  • \(F = \{f_1^1, f_2^1, \ldots, f_1^2, f_2^2, \ldots \}\) - функциональные символы;

  • \(R = \{P_1^1, P_2^1, \ldots, P_1^2, P_2^2, \ldots \}\) - предикатные символы;

  • \(()\) - технические символы;

  • \(\forall\) - квантор общности;

  • \(\neg\), \(\to\) - логические связки.

• Синтаксические правила:

  • Термы: \(t ::= a \;|\; x \;|\; f_i^n(t, \ldots, t)\), где \(a \in A\), \(x \in X\), \(f_i^n \in F\);

  • Атомарные формулы: \(AF ::= P^n_i(t, \ldots, t)\), где \(P_i^n \in R\);

  • Формулы: \(\varphi ::= Q \; | \; (\neg \varphi) \; | \; (\varphi \to \varphi) \; | \; (\forall x)\varphi\), где \(Q \in AF\).

Это определение записано с помощью формы Бэкуса-Наура (BNF), которая обычно используется для определения синтаксиса языков программирования. Вообще языки программирования и формально-логические языки определяются сходным образом.

Например, вот так выглядит язык первого порядка \(\mathcal N\) для арифметики:

• Переменные: \(x_1, x_2, \ldots\)

• Индивидные константы: \(a_1\) - это константа \(0\)

• Предикат: \(P_1^2\) - это равенство \(=\)

• Функции:

  • \(f_1^1\) - это функция следования

  • \(f_1^2\) - это сложение

  • \(f_2^2\) - это умножение

Важно отметить, что множество термов \(\mathcal T\) и множество формул \(\mathcal F\) являются рекурсивными. Следовательно, синтаксическая корректность терма или формулы - это разрешимое свойство. Это значит, что его можно проверить с помощью компьютерной программы.

Для языка первого порядка \(\mathcal L\) будем использовать систему доказательств \(\mathcal K_{\mathcal L}\) в виде гильбертовской системы со следующими 6 схемами аксиом и 2 правилами вывода:

• Аксиомы:

  • (K1) \((\varphi \to (\psi \to \varphi))\)

  • (K2) \(((\varphi \to (\psi \to \theta)) \to ((\varphi \to \psi) \to (\varphi \to \theta)))\)

  • (K3) \((((\neg \varphi) \to (\neg \psi)) \to (\psi \to \varphi))\)

  • (K4) \((\forall x_i)\varphi \to \varphi\), где переменная \(x_i\) не имеет свободных вхождений в формулу \(\varphi\)

  • (К5) \((\forall x_i)\varphi \to \varphi(t)\), где терм \(t\) входит вместо всех свободных вхождений переменной \(x_i\) в формулу \(\varphi\)

  • (K6) \((\forall x_i)(\varphi \to \psi) \to (\varphi \to (\forall x_i)\psi)\), где переменная \(x_i\) не имеет свободных вхождений в формулу \(\psi\)

• Правила вывода:

  • Modus Ponens (MP): \(\dfrac{\varphi, \; (\varphi \to \psi)}{\psi}\)

  • Обобщение (Gen): \(\dfrac{\varphi}{(\forall x_i)\varphi}\)

Формулы (K1)-(K6) и правила вывода (MP), (Gen) - это схемы, из которых получается бесконечно много примеров. Например, две следующие формулы - это примеры (K1):

\((p_1 \to (p_2 \to p_2))\)

\((((\neg p_1) \to p_3) \to (((\neg p_3) \to p_4) \to ((\neg p_1) \to p_3)))\)

Вот пример для правила вывода (MP):

\(\dfrac{(p_1 \to ((\neg p_2) \to (\neg p_3))), \;\; ((p_1 \to ((\neg p_2) \to (\neg p_3))) \to (p_3 \to p_4))}{(p_3 \to p_4)}\)

Неформальный анализ показывает, что все примеры 6 схем аксиом правильны. В том смысле, что они выполняются в любой интерпретации.

В формально-логической системе понятия рассуждения (как процесса) и вывода формализовано в виде доказательств. А результат процесса рассуждений определяется как теорема этой системы.

Определение. Для заданной формально-логической системы \(\mathcal S\) доказательство в этой системе определяется как конечная, непустая последовательность \(\varphi_1, \ldots, \varphi_n\) правильно построенных формул, таких, что каждая формула \(\varphi_i\) в этой последовательности - это либо аксиома, либо она выводится из предыдущих формул этой последовательности с помощью одного из правил вывода системы \(\mathcal S\). Последняя формула \(\varphi_n\) в доказательстве называется теоремой этой системы, обозначается \(\vdash_{\mathcal S} \varphi_n\).

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

Пример формального доказательства в системе \(\mathcal K_{\mathcal L}\):

1. \((P_1^1(x_1) \to (P_2^2(x_1, x_2) \to P_1^1(x_1)))\) - из схемы аксиом (K1)

2. \(((P_1^1(x_1) \to (P_2^2(x_1, x_2) \to P_1^1(x_1))) \to ((P_1^1(x_1) \to P_2^2(x_1, x_2)) \to (P_1^1(x_1) \to P_1^1(x_1))))\) - из схемы аксиом (K2)

3. \(((P_1^1(x_1) \to P_2^2(x_1, x_2)) \to (P_1^1(x_1) \to P_1^1(x_1)))\) - по правилу (MP) из 1, 2

4. \((\forall x_1)((P_1^1(x_1) \to P_2^2(x_1, x_2)) \to (P_1^1(x_1) \to P_1^1(x_1)))\) - по правилу (Gen) из 3

5. \((\forall x_2)(\forall x_1)((P_1^1(x_1) \to P_2^2(x_1, x_2)) \to (P_1^1(x_1) \to P_1^1(x_1)))\) - по правилу (Gen) из 4

В формальном доказательстве конкретные примеры схем аксиом и схем правил вывода получаются в результате сопоставления шаблонов.

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

\(\dfrac{(\forall x_i)(\varphi(x_i) \to \psi(x_i)), \;\; \varphi(a_i)}{\psi(a_i)}\)

Правильность данного правила вытекает из правильности формулы

\((((\forall x_i)(\varphi(x_i) \to \psi(x_i)) \land \psi(a_i)) \to \psi(a_i))\)

В качестве упражнения можно построить доказательство этой формулы как теоремы в системе \(\mathcal K_{\mathcal L}\).

Рассуждение в примере неправильного рассуждения можно формализовать следующим образом:

\(\dfrac{(\exists x_i)(\varphi(x_i) \land \psi(x_i)), \;\; \varphi(a_i)}{\psi(a_i)}\)

Легко понять, что это неправильное правило, и соответствующая формула не является теоремой:

\((((\exists x_i)(\varphi(x_i) \land \psi(x_i)) \land \varphi(a_i)) \to \psi(a_i))\)

Поэтому такое рассуждение будет неправильным.

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

Метатеория формально-логических систем. Изучение интерпретаций (или семантики) и представлений, а также свойств доказательств в формально-логических системах - это ключевые аспекты металогики. Первый из них относится к теории моделей, второй - к теории доказательств. Всеобъемлющая цель состоит в том, чтобы изучить, как формальная логика и математика взаиосвязаны с формализмами и их областями применения.

Интерпретация формальных языков. Применяя формально-логическую систему к изучению интересующей области, всегда нужна интерпретация формул (предложений) формального языка как утверждений об этой области. Тем самым форма увязывается с содержанием предмета исследования. Интерпретация формулы относится к семантике (или смысловому значению) формулы в данной области. Следуя индуктивно синтаксису формального языка, производится сопоставление символическим элементам формального языка их семантики, то есть элементов предметной области. Давайте покажем, как вводится интерпретация языка \(\mathcal L\) гильбертовской системы логики первого порядка.

Определение. Интерпретация \(\mathcal I = (D, I)\) языка первого порядка \(\mathcal L\) состоит из носителя интерпретации \(D\), представляющего собой множество, а также многосортного отображения \(I\) из синтаксических категорий в элементы, функции и отношения, заданные на \(D\):

• Семантика константных символов: \(I \colon A = \{a_1, \ldots\} \mapsto D\) - отображение из \(A\) в \(D\). Обозначаем \(I(a_i)\) через \(\overline{a_i}\) - это означивание символа \(a_i\).

• Семантика функциональных символов: \(I \colon F \mapsto \{f^n \colon f^n \text{ - это }n\text{-арная функция на }D\}\). Это отображение сопоставляет каждому функциональному символу функцию из \(D\). Обозначаем \(I(f_i^k)\) через \(\overline{f_i^k}\) - это означивание символа \(f_i^k\).

• Семантика предикатных символов: \(I \colon R \mapsto \{P^n \colon P^n \text{ - это }n\text{-арное отношение на }D\}\). Это отображение сопоставляет каждому предикатному символу отношения на \(D\). Обозначаем \(I(P_i^k)\) через \(\overline{P_i^k}\) - это означивание символа \(P_i^k\).

Для заданной интерпретации \(\mathcal I\) языка первого порядка можно определить значение термов и формул в рамках языка.

Определение. В рамках заданной интерпретации \(\mathcal I = (D, I)\) языка первого порядка \(\mathcal L\) оценка термов сопоставляет термам их значения из \(D\). Оценка формул сопоставляет формулам истинностные значения из множества \(\{tt, ff\}\). Формально, оценка \(\sigma\) термов языка \(\mathcal L\) - это отображение из множества термов \(\mathcal T\) в множество \(D\), т.е. \(\sigma \colon \mathcal T \mapsto D\), которое удовлетворяет следующим условиям:

1. \(\sigma(a_i) = \overline{a_i}\) для \(a_i \in A\);

2. \(\sigma(f_i^n(t_1, \ldots, t_n)) = \overline{f_i^n}(\sigma(t_1), \ldots, \sigma(t_n))\) для \(f_i^n \in F\).

Оценку термов можно расширить для оценки формул, которую также обозначим через \(\sigma\), это отображение \(\sigma \colon \mathcal F \to \{tt, ff\}\), такое, что:

1. \(\sigma(P_i^n(t_1, \ldots, t_n)) = tt\), если и только если \(\overline{P_i^n}(\sigma(t_1), \ldots, \sigma(t_n))\) выполняется в \(D\);

2. \(\sigma(\neg\varphi) = tt\), если и только если \(\sigma(\varphi) = ff\);

3. \(\sigma(\varphi \to \psi) = tt\), если и только если \(\sigma(\varphi) = ff\) или \(\sigma(\psi) = tt\);

4. \(\sigma((\forall x_i)\varphi) = tt\), если и только если \(\sigma'(\varphi) = tt\) для всякой оценки \(\sigma'\), совпадающей с \(\sigma\), кроме, возможно, переменной \(x_i\).

Например, можно определить интерпретацию \(\mathcal I\) для языка первого порядка \(\mathcal N\), задав следующие отображения: \(\overline{a_1}\) - это \(0\), \(\overline{f_1^1}\) - это функция следования (т.е. \(\overline{f_1^1} = x + 1\)), \(\overline{f_1^2}\) - это сложение, \(\overline{f_2^2}\) - это умножение, и \(\overline{P^2_1}\) - это отношение равенства “\(=\)”. При такой интерпретации смысловое значение формул можно проиллюстрировать следующим образом:

1. Формула \((\forall x_1)(\neg P_1^2(f_1^1(x_1), x_1))\) формально обозначает утверждение, что для всех \(x\) выполнено \(x + 1 \neq x\).

2. Формула \((\forall x_1)(\forall x_2)(P_1^2(f_1^2(x_1, x_2), f_1^2(x_2, x_1)))\) формально обозначает утверждение, что для всех натуральных чисел выполнено \(x_1 + x_2 = x_2 + x_1\) (т.е. что сложение коммутативно).

3. Формула \((\forall x_1)(\forall x_2)(\forall x_3)(P_1^2(f_2^2(x_3, f_1^2(x_1, x_2)), f_1^2(f_2^2(x_3,x_1), f_2^2(x_3,x_2))))\) обозначает закон дистрибутивности умножения относительно сложения: \((x_3 \times (x_1 + x_2)) = (x_3 \times x_1) + (x_3 \times x_2)\).

Все три формулы выполняются при любой оценке при указанной интерпретации.

Теперь мы поняли, что формально-логическая система имеет три составляющие: формальный язык, связанная с ним система доказательств и семантика (т.е. интерпретации).

Важные метатеоремы, касающиеся формально-логических систем. Введем основополагающие понятия формально-логических систем.

Определение. Пусть \(\mathcal I\) - интерпретация языка первого порядка \(\mathcal L\). Тогда:

• Говорят, что формула \(\varphi\) выполняется на оценке \(\sigma\) при интерпретации \(\mathcal I\), обозначение \((\mathcal I, \sigma) \models \varphi\), если \(\sigma(\varphi) = tt\).

• Формула \(\varphi\) называется выполнимой при интерпретации \(\mathcal I\), если существует оценка \(\sigma\), такая, что \((\mathcal I, \sigma) \models \varphi\).

• Интерпретация \(\mathcal I\) называется моделью формулы \(\varphi\), если \(\varphi\) выполняется на каждой оценке при интерпретации \(\mathcal I\), обозначение \(\mathcal I \models \varphi\).

Формула \(\varphi\) называется общезначимой, обозначение \(\models \varphi\), если она выполняется при всех интерпретациях (т.е. каждая возможная интерпретация - модель формулы \(\varphi\)).

Эти основополагающие концепции приводят к следующим задачам:

• Если заданы интерпретация и формула, удовлетворяет ли конкретная оценка формуле?

• Если заданы интерпретация и формула, является ли формула выполнимой?

• Является ли данная интерпретация моделью формулы?

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

Пусть имеется логическая система \(\mathcal S\). Следующие метасвойства носят фундаментальный характер, касающийся соотношения между формальным языком и его семантикой, то есть между формальными спецификациями и моделями:

• Непротиворечивость: Логическая система \(\mathcal S\) непротиворечива, если не существует такой формулы \(\varphi\), что как \(\varphi\), так и \(\neg\varphi\) являются теоремами \(\mathcal S\), то есть не бывает одновременно \(\vdash_{\mathcal S} \varphi\) и \(\vdash_{\mathcal S} \neg\varphi\).

• Корректность: Логическая система \(\mathcal S\) корректна, если всякая теорема \(\mathcal S\) верна, т.е. если \(\vdash_S \varphi\), то \(\models\varphi\).

• Адекватность: Логическая система \(\mathcal S\) адекватна, если всякая правильная формула - теорема этой системы, т.е. если \(\models\varphi\), то \(\vdash_{\mathcal S}\varphi\).

• Полнота: Логическая система \(\mathcal S\) полна, если не бывает замкнутой (т.е. без свободных переменных) формулы \(\varphi\), такой, что ни \(\varphi\), ни \(\neg\varphi\) не являются теоремами \(\mathcal S\), т.е. всегда либо \(\vdash_{\mathcal S} \varphi\), либо \(\vdash_{\mathcal S} (\neg \varphi)\).

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

В общем, логическая система первого порядка - это логическая система \(\mathcal S\), определенная на языке первого порядка \(\mathcal L\), такая, что все теоремы гильбертовской системы \(\mathcal K_{\mathcal L}\) также являются теоремами системы \(\mathcal S\). Таким образом, \(\mathcal S\) называется расширением \(\mathcal K_{\mathcal L}\). Формальная математическая система - это расширение \(\mathcal K_{\mathcal L}\), включающее в себя аксиомы для предиката равенства “\(=\)”. Примерами формальной математической системы служат: арифметика натуральных чисел, булева алгебра, аксиоматическая теория групп и аксиоматическая теория множеств ZFC.

Можно показать, что гильбертовская система \(\mathcal K_{\mathcal L}\) для языка первого порядка \(\mathcal L\) обладает одновременно и корректностью (и поэтому непротиворечива), и адекватностью, как показал Гёдель в 1929 г. Однако \(\mathcal K_{\mathcal L}\) неполна, потому что ни \((\forall x_i)P^1_1(x_i)\), ни \((\neg(\forall x_i)P_1^1(x_1))\) не являются теоремами этой системы. Можно доказать, что во всяком противоречивом расширении \(\mathcal K_{\mathcal L}\) любая формула становится теоремой, что делает систему непригодной для использования.

Теорема. (теорема Гёделя о неполноте). Любая непротиворечивая система, в которой можно выразить арифметику натуральных чисел, обладает неполнотой.

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

Важность математической логики и следствия теоремы Гёделя. Главным преимуществом изучения математической логики является ее строгая структура для систематического рассуждения и решения проблем. Дедуктивная логика облегчает точный вывод теорем из установленных аксиом и принципов, часто основанных на наблюдениях и интуиции, и обеспечивает последовательность, надежность (обоснованность) и полноту теорий и технологий.

Сила и полезность формальной логики. Развитие формальной логики демонстрирует ее огромную мощь в создании сложных структур и процессов на основе простых правил, механически выполняя рекурсию и итерацию. Применяя принципы структуры, методы, основанные на синтаксисе, и абстракции, формальная логика обеспечивает систематическую основу для анализа сложности и управления ею. Такие методы, как эквивалентность и подстановка следствия, позволяют точно манипулировать сложными системами, обеспечивая модульность, повторное использование и подход “разделяй и властвуй” в инженерных дисциплинах, в частности в разработке компьютерных систем.

Изучение математической логики развивает строгость, последовательность и многоплановое мышление, что необходимо для построения последовательных моделей мышления. Кроме того, изучение и практика логики развивает независимое и критическое мышление, что делает ее бесценным инструментом для теоретических исследований и решения практических задач.

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

Всякая теория основана на определенной логической системе. В рамках этой системы устанавливаются основные допущения, определяются ключевые концепции, формулируются утверждения и проводится их анализ. “Язык” логической системы неизменен, и теоремы являются всего лишь выводами из этих предположений. Изучение такой теории может привести к доказательству новых теорем и развитию дальнейших идей и приложений. Однако этот процесс не является подлинной “инновацией”, основанной только на рассуждениях.

Новые теории возникают, когда оспариваются существующие аксиомы или предположения, часто в ответ на наблюдения или проблемы, которые не могут быть адекватно решены с помощью существующей логики. Это требует выдвижения новых аксиом, построения новых моделей и определения новых концепций. Переосмысливая эти основополагающие элементы, мы можем формулировать инновационные идеи и теории, расширяя границы знаний за пределы существующей логической системы. Здесь мы определяем “созидание” как инновацию, которая обычно создает новые теории, предполагающие расширение языка, необходимого для формулирования новых концепций, аксиом, правил вывода и моделей.

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

Возможности компьютеров в области логического мышления и инноваций. Это обсуждение приводит нас к убеждению, что способность наблюдать факты или проблемы, которые существующая логическая система не может адекватно решить, и оспаривать ее преобладающие предположения, предлагая новые концепции, аксиомы и, в конечном счете, новые логические системы, является ключевым элементом человеческого интеллекта. Если мы рассматриваем структуру человеческого знания или архитектуру системы человеческого знания как включающую устоявшиеся теории и их взаимосвязи, то ее эволюция определяется 1) открытием новых теорем и применений существующих теорий, а также 2) созданием новых теорий. Даже при таком упрощенном взгляде на знания мы можем утверждать, что, хотя компьютерные программы, включая системы глубокого обучения, обладают огромным потенциалом для развития первого типа, в настоящее время они не могут способствовать развитию второго типа.

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

Философские следствия теоремы Гёделя. Гёдель открыл несколько фундаментальных теорем, включая теорему о неполноте, которые вместе часто называют просто теоремой Гёделя. Эти теоремы могут быть выражены в нескольких эквивалентных формах:

• Математика неисчерпаема.

• Любая непротиворечивая формальная математическая теория должна содержать неразрешимые утверждения.

• Ни один компьютер (или программа), доказывающий теоремы, не может доказать все и только истинные математические утверждения.

• Ни одна формальная математическая система не может быть одновременно непротиворечивой и полной.

• Математика механически (или алгоритмически) неисчерпаема (или неполна).

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

С философской точки зрения теорема Гёделя раскрывает несколько ключевых диалектических аспектов:

• Логика и интуиция – Логика не может полностью охватить все аспекты интуиции.

• Формализм и содержание – Формальные системы представляют собой абстракции, но они не могут охватить все богатство содержания.

• Механическое и умственное – Вопрос о том, все ли аспекты человеческого интеллекта могут быть механизированы, остается под вопросом.

• Язык и мышление – Хотя язык является мощным инструментом для выражения мыслей, он не может в полной мере передать все идеи, эмоции или аспекты человеческого сознания.

• Истина и доказуемость – Формальные системы доказывают не все истины.

• Реальное и познаваемое – Человеческое знание о реальности по своей сути ограничено и постоянно развивается.

Эти философские выводы подчеркивают ограниченность формальных систем и бросают вызов представлению о том, что механические или алгоритмические процессы могут полностью охватывать все аспекты математики, знаний или человеческого мышления. Работа Гёделя побуждает к постоянным размышлениям о границах логики, природе истины, сложности человеческого познания и возможностях машин (или программ). На наш взгляд, эти выводы могут оказать важное влияние на понимание различий и взаимосвязей между возможностями человеческого разума и машин, включая DNN (глубокие нейронные сети) и LLM (большие языковые модели). Гёдель проявил значительный интерес к доказательству того, что человеческий разум превосходит машины в математике, хотя и без особых существенных результатов.

Вычислительные модели и теории

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

Вычисления в истории цивилизации

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

Ранняя история вычислений и устройств. Вычислительная техника - это уникальная способность человека, которая прогрессировала естественным образом и систематически развивается через образование. В современном обществе люди рано приобретают базовые навыки работы с компьютером, проходя различные этапы обучения – от детского сада до начальной и средней школы и, в конечном итоге, до получения высшего образования. На протяжении всего этого образовательного пути учащиеся знакомятся с математическими понятиями, включая арифметику (сложение, вычитание, умножение и деление), решение уравнений, геометрические доказательства, логарифмы, математический анализ и логические рассуждения. Важнейшим элементом вычислений в этом учебном процессе является его неотъемлемая природа, основанная на правилах, где структурированные принципы лежат в основе решения проблем и направляют процесс принятия решений.

Вычисления были движущей силой прогресса человеческой цивилизации, поскольку развитие вычислительных технологий и инструментов неразрывно связано с развитием общества. Человечество стремилось упростить и систематизировать вычисления, которые развивались на протяжении тысячелетий наряду с достижениями в математике, инженерии и технологии. Ранние формы вычислительных методов и инструментов восходят к древним цивилизациям, где были разработаны базовые системы счета. Такие инструменты, как счетные палочки (на рис. 1а) и счеты (на рис. 1б) в Китае, глиняные жетоны в Месопотамии и египетская иероглифическая система счисления заложили основу для более сложных методов арифметики.

В средневековом исламском мире такие ученые, как Аль-Хорезми, ввели алгебру и алгоритмы (термин, образованный от его имени), которые оказали значительное влияние на более поздние европейские математические традиции. Изобретение механических часов в 14 веке продемонстрировало растущую сложность механических вычислений.

К 17 веку европейские математики и изобретатели, такие как Блез Паскаль и Готфрид Вильгельм Лейбниц, начали создавать первые механические калькуляторы, такие как арифмометр Паскаля (рис. 2а) и ступенчатый счетный механизм Лейбница (рис. 2б). Эти устройства, хотя и были ограничены, положили начало автоматизированным вычислениям.

В начале 19 века Чарльз Бэббидж и Ада Лавлейс представили вычислительные машины, которые заложили основу для современных вычислений. В 1820-х годах Бэббидж разработал “разностную машину” для автоматизации математических вычислений. На рис. 3 представлена реконструкция первоначальных планов, хранящихся в Музее науки в Лондоне. В 1830-х годах он разработал более амбициозную “аналитическую машину” - механическое устройство, которое могло выполнять любые вычисления с помощью программируемых инструкций. В 1840-х годах Ада Лавлейс осознала далеко идущий потенциал изобретения Бэббиджа. Часто считающаяся первым компьютерным программистом, она выдвинула теорию о том, что эти машины могут манипулировать символами и выполнять сложные алгоритмы, подготовив почву для цифровой революции более чем за столетие до того, как она произошла.

Истоки вычислительных моделей и вычисляемость. Изучение истории, понимания и практики вычислений, наряду с развитием механических вычислительных устройств и машин, привело к появлению моделей вычислений в начале 20-го века. В первую очередь это стало результатом усилий математиков, которые в рамках программы Гильберта решали, в частности, проблему разрешимости Гильберта-Аккермана. Критический подход заключается в строгом определении того, что означает, что проблема разрешима или что функция или задача вычислима. Наиболее фундаментальными и хорошо изученными моделями являются рекурсивные функции, λ-исчисление и машины Тьюринга. Каждая из них предоставляет различные, но в конечном счете эквивалентные платформы для представления вычислений.

Рекурсивные функции

У рекурсивных функций определяют их значения для нескольких базовых случаев, т.е. для “малых” аргументов, а значения для большего аргумента вычисляется рекурсивно путем применения той же функции к меньшим аргументам, шаг за шагом, пока не будут достигнуты значения для базовых случаев.

Простым примером рекурсивной функции является факториал \(n!\). Обозначим эту функцию через \(fct(n)\), и тогда она будет определена следующим образом:

\(fct(0) = 1, \quad fact(n + 1) = (n + 1) \times fct(n)\).

Эта функция определена для любого аргумента \(n \geq 0\). При \(n = 0\) факториал равен 1, а для любого \(n > 0\) значение функции вычисляется путем последовательного “разворачивания” выражения \((n + 1) \times fct(n)\) до тех пор, пока не будет достигнут базовый вариант \(0! = 1\). Например, значение \(4!\) может быть вычислено следующим образом:

\(fct(4) = 4 \times fct(3) =\)

\( = 4 \times (3 \times fct(2)) =\)

\(= 4 \times (3 \times (2 \times fct(1))) =\)

\(= 4 \times (3 \times (2 \times (1 \times 1))) =\)

\( = 24 \)

Таким образом, значение функции для любого заданного входного аргумента вычисляется шаг за шагом в соответствии с правилом развертывания, которое вытекает из определяющих рекуррентных соотношений. Мы можем понимать определяющие выражения рекурсивной функции как аксиомы и правила дедукции, которые также определяют алгоритм вычисления функции, т.е. эффективную процедуру вычисления ее значений, которую человек или механическое вычислительное устройство может выполнить за конечное число шагов. Эти этапы вычислений имеют ту же форму, что и вывод в доказательствах логических формул первого порядка с заменой эквивалентных.

Позже в этом разделе мы увидим, что λ-исчисление и теория машин Тьюринга показывают, что любое вычисление (процесс) может быть представлено в виде серии формальных логических выводов. Следуя той же линии исследований, что и машины Тьюринга, продукционные системы Поста также моделируют вычисления как вывод доказательства, где вычисления представляют собой поэтапный процесс получения результатов из исходных посылок с использованием правил.

Ранняя история рекурсивных определений. Известным примером такого рекурсивного определения является последовательность чисел Фибоначчи: 0, 1, 1, 2, 3, 5, … В этой последовательности, начиная с третьего числа, каждое последующее число является суммой двух предыдущих:

\(F_0 = 0,\; F_1 = 1,\; F_n = F_{n-1} + F_{n-2} \text{ для } n \geq 2\)

Эта последовательность названа в честь итальянского математика Леонардо Пизанского, также известного как Фибоначчи, который представил ее западноевропейской математике в своей книге “Liber Abaci”, опубликованной в 1202 году. Однако эта последовательность была открыта индийскими математиками еще в 200 году до нашей эры, а описания подобных последовательностей можно найти в греческих, египетских и санскритских источниках, датируемых 700 годом до нашей эры.

Систематические исследования рекурсивных функций основаны на математической логике, в частности, на так называемой теории рекурсивных функций, которую в настоящее время чаще называют теорией вычислимости. Интерес к рекурсивным функциям первоначально возник в результате дискуссий о создании основ арифметики. Повторяющиеся определения сыграли решающую роль в формулировании математической индукции как метода рассуждения о натуральных числах. Первые хорошо известные рекурсивные определения были даны Грассманом (1861) и Пирсом (1881), которые использовали их для определения сложения и умножения натуральных чисел и доказательства ассоциативных, коммутативных и дистрибутивных законов для этих операций.

Похоже, что термин “определение с помощью рекурсии” впервые появился в эссе Дедекинда “Что такое числа и какими свойствами они должны обладать” (1888). В этой статье Дедекинд представил теорию множеств для арифметики и доказал теоремы о существовании и единственности функций, определяемых примитивной рекурсией. Он дополнительно определил сложение, умножение и возведение в степень с помощью рекурсии, а затем методом индукции доказал, что указанные функции удовлетворяют ожидаемым алгебраическим уравнениям. Первые два из этих определений были даны Пеано (1889) для определения символов \(+\) и \(\times\) в аксиоматизации арифметики.

Примитивно-рекурсивные функции. Сколем провел первое исследование в 1920-х годах. Одной из его главных целей была разработка логической основы теории чисел, позволяющей избежать использования кванторов, таких как “для всех” (обозначается \(\forall\)) и “существует” (обозначается \(\exists\)). Его подход заключался в представлении математических теорем в виде функциональных утверждений. Вместо того, чтобы записывать \((\forall x)(\forall y)( x + y = y + x )\), Сколем мог выразить эту идею в виде уравнения (тождества) между двумя функциями или выражениями, как в уравнении:

\(x + y = y + x\)

Эти тождества, позже названные Гильбертом и Бернайсом (1934) “поддающимися проверке”, могут быть проверены путем вычисления отдельных примеров. Это делается путем замены переменных в инструкции фактическими числами и проверки правильности инструкции на основе примитивных, простых, пошаговых вычислений, которые можно применять многократно. Сколем описал этот процесс пошагового определения математических функций и свойств, который можно проверить с помощью вычислений, как рекурсивный способ мышления. Он неформально описал четыре особенности этой системы.

1. Натуральные числа и функция следования: Система начинается с натуральных чисел, 0, 1, 2 и т.д., в качестве базовых объектов вместе с функцией следования \(x + 1\), которая выдает следующее число.

2. Замена описаний функций: Если две функции равны, вы можете заменить одну на другую в разных выражениях.

3. Определения с помощью рекурсии: все функции или родственники натуральных чисел определяются рекурсивно.

4. Доказательство утверждений с помощью индукции: Функциональные утверждения (т.е. математические теоремы, такие как коммутативность сложения) доказываются с помощью математической индукции.

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

Следующей важной вехой в развитии теории рекурсивных функций является формальное описание примитивно-рекурсивных функций. Этот прогресс в значительной степени обусловлен работой над программой Гильберта, а также доказательством теоремы Гёделя о неполноте.

Хотя программа Гильберта была амбициозной и ставила своей целью обеспечить надежную основу для всей математики, первоначально она была сосредоточена на доказательстве непротиворечивости арифметики (1900). План проведения такого доказательства был описан с точки зрения финитности. Идея заключалась в том, что если бы все математические рассуждения можно было свести к конечностным операциям, то можно было бы обеспечить непротиворечивость математики на прочном фундаменте. Гильберт полагал, что абстрактные и потенциально бесконечные концепции можно свести к конечным, надежным рассуждениям с помощью этого конечностного метода. С этой целью он предложил использовать метод, который он назвал метаматематикой, для доказательства непротиворечивости формальной математической системы (или теории).

В рамках своих усилий по развитию метаматематики в 1910-х и 1920-х годах Гильберт в сотрудничестве с Аккерманом и Бернайсом предложил использовать “числовые знаки” для представления натуральных чисел и описания контекстуальной индукции. Идея состояла в том, чтобы рассматривать числа не как абстрактные сущности, а как конкретные, конечные последовательности физических комбинаторных объектов. Цифровые знаки обычно представлялись в виде простых символов или штрихов (например, “|”, “||”, “|||”), которые непосредственно соответствуют натуральным числам (1, 2, 3 и т.д.). С такими выражениями можно работать конкретно, соединяя или удаляя штрихи, отражая арифметические операции последователя и предшественника, описанные в рекурсивном режиме мышления. Гильберт также использует эту идею для объяснения смысла функциональных утверждений типа коммутативности сложения. Их можно доказать, обратившись к тому, как они определяются рекурсивно, используя логические выводы.

Гильберт продолжил разработку логического исчисления для теории конечных чисел, которое включало “рекурсию и интуитивную индукцию для конечных совокупностей”. Он впервые дал определение одновременной рекурсии, которое указывало на то, что позже будет названо рекурсивными схемами. Он и его коллеги продолжили изучение этой системы рекурсивных определений и описали несколько типов рекурсии.

• обычная рекурсия, которая имеет простую структуру и похожа на описание примитивной рекурсии, данное Сколемом;

• трансфинитная рекурсия, которая распространяется на бесконечные последовательности;

• рекурсия высших типов, где схемы рекурсии применяются не только к числам, но и к более абстрактным объектам, таким как сами функции.

Однако этот существенный вклад Гильберта и его сотрудников в рекурсивную определимость и их влияние позже затмила более точная формулировка примитивной рекурсии, данная Гёделем, которая стала краеугольным камнем современной теории рекурсии. Гёдель усовершенствовал описания своих предшественников и дал формальное определение того, что такое рекурсивно определенные функции.

Определение. Числовая функция \(\varphi(x_1, \ldots, x_n)\) определена рекурсивно с помощью числовых функций \(\psi(x_1, \ldots, x_{n-1})\) и \(\mu(x_1, \ldots, x_{n+1})\), если для любых значений \(x_1, \ldots, x_n\) и \(k\) выполняются следующие уравнения:

1. \(\varphi(0, x_2, \ldots, x_n) = \psi(x_2, \ldots, x_n)\)

2. \(\varphi(k+1, \ldots, x_n) = \mu(k, \varphi(k, \ldots, x_n)), x_2, \ldots, x_n)\)

Числовая функция \(\varphi\) называется рекурсивной, если существует конечная последовательность числовых функций \(\varphi_1, \ldots, \varphi_n\), которая заканчивается на функции \(\varphi\), такая, что каждая функция в этой последовательности:

• константа или функция следования

• или рекурсивно определена через две предшествующие ей функции

• или результат подстановки в одну из предшествующих функций.

Это определение дало математически определенный класс функций над натуральными числами, теперь известный как примитивно-рекурсивные функции, хотя Гёдель использовал только термин “рекурсивный”.

Гёдель перешел к определению примитивно-рекурсивных отношений, которые он назвал рекурсивными отношениями, используя характеристические функции.

Определение. Отношение \(R(x_1, \ldots, x_n)\) между натуральными числами называется рекурсивным, если существует примитивно-рекурсивная функция \(\varphi(x_1, \ldots, x_n)\), такая, что для любых значений \(x_1, \ldots, x_n\) выполняется \(R(x_1, \ldots, x_n) \leftrightarrow (\varphi(x_1, \ldots, x_n) = 0)\)

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

Гёделевское определение рекурсии и его теорема о неполноте. Основной целью его знаменитой статьи 1931 года было доказать его теорему о неполноте, которая гласит, что если арифметическая система непротиворечива, то существует формула, которая неразрешима внутри системы – это означает, что ее нельзя ни доказать, ни опровергнуть с помощью аксиом системы. Он впервые разработал формальную логическую систему, которую назвал \(\mathbf P\), на основе труда “Principia Mathematica” Рассела и Уайтхеда (1910-1913). Затем у него возникла идея получить такую неразрешимую формулу в \(\mathbf P\) из соображения, что рекурсивные определения естественным образом связаны с индуктивными определениями синтаксических структур правильно построенных формул и доказательств.

Затем Гёдель разработал технику, известную как арифметизация синтаксиса, для выражения формул и доказательств в виде примитивно-рекурсивных отношений, и он показал, что для каждого примитивно-рекурсивного отношения \(R(x_1, \ldots, x_k)\) существует формула \(\varphi_R( x_1, \ldots , x_k )\) из \(\mathbf P\), такая, что факт, который содержится (или не содержится) в данной последовательности чисел \(n_1, \ldots, n_k\), отражается доказуемостью (или опровержимостью) в \(\mathbf P\) соответствующего экземпляра \(\varphi_R ( x_1, \ldots , x_k )\). Пусть \(\overline{n} = s (\ldots( s (0))) \) - это формальное представление числа \(n\) в \(\mathbf P\) путем применения \(n\) раз функции следования \(s( x )\) к \(0\). Тогда, формально говоря, выполняются свойства:

1. если выполняется \(R(n_1, \ldots, n_k)\), то \(\mathbf P \vdash \varphi_R(\overline{n_1}, \ldots, \overline{n_k})\)

2. если не выполняется \(R(n_1, \ldots, n_k)\), то \(\mathbf P \vdash \neg\varphi_R(\overline{n_1}, \ldots, \overline{n_k})\)

Затем Гёдель установил, что формула \(\varphi_R(x_1, \ldots, x_k)\) представляет отношение \(R(x_1, \ldots, x_k)\), и ввел формулу для представления функции. Функция \(f(x_1, \ldots, x_k)\) представима в \(\mathbf P\), если существует формула \(\varphi_f(x_1, \ldots, x_k, y)\), такая, что для любых чисел \(n_1, \ldots, n_k\), а также числа \(m\):

\(f(n_1, \ldots, n_k) = m\), если и только если \(\mathbf P \vdash \varphi_f(n_1, \ldots, n_k, m)\).

Полученное уравнение выражает взаимосвязь между представимости функции в формальной системе и ее вычислимостью.

Затем Гедель предложил метод кодирования каждого символа в алфавите, терма, формулы и доказательства, обозначаемого \(\alpha\), в виде уникального натурального числа \([\alpha]\), основанного на их индуктивных структурах. Число \([\alpha]\) теперь называется гёделевским номером строки \(\alpha\). В этой системе кодирования индуктивные синтаксические операции в синтаксических элементах соответствуют операциям с гёделевскими номерами, которые могут быть описаны с помощью примитивно-рекурсивных функций. Например, предположим, что \(x\) - это гёделевский номер формулы \(\varphi\), функция \(\neg x\), которая возвращает гёделевский номер формулы \((\neg \varphi)\), может быть задана как \([\neg] * x\). Этот метод кодирования можно понимать как обобщение “конструирования и деконструирования числовых знаков”, описанного Гильбертом.

Важным шагом в получении формулы, неразрешимой в \(\mathbf P\), было определить связь \(Proof(x,y)\), которая имеет место для гёделевского номера числа \(x\) и номера \(y\) последовательности формул \(\varphi_1, \ldots, \varphi_n\), если и только если последовательность \(\varphi_1, \ldots, \varphi_n\) - это доказательство формулы \(\varphi\) в \(\mathbf P\):

\(Proof([\varphi], [\varphi_1, \ldots, \varphi_n]) \text{ если и только если } \vdash_{\mathbf P} \text{ с док-вом } \varphi_1, \ldots, \varphi_n\)

Согласно определению отношения \(R\), существует формула \(WfPrf(x, y)\), которая представляет отношение \(Proof(x, y)\), и поэтому можно определить формулу \((\exists y) WfPrf(x,y)\), обозначаемую \(Proof(x)\). Формула \(Proof(x)\) выражает следующее утверждение: существует доказательство в \(\mathbf P\) теоремы \(\varphi\) с гёделевским номером \(x\).

Финальный шаг Гёделя в конструировании неразрешимой формулы - доказательство леммы о диагонали, которая утверждает, что для всякой формулы \(\varphi(x)\) системы \(\mathbf P\) существует замкнутая формула \(\psi_\varphi\), такая, что

\(\vdash_{\mathbf P} \psi_\varphi \leftrightarrow \varphi(\overline{[\psi_{\varphi}]})\)

Формула \(\psi_\varphi\) называется гёделевской последовательностью формулы \(\varphi\). Затем он применил эту лемму к формуле \(\neg Proof(x)\) и получил гёделевскую последовательность, обозначаемую \(\mathbf G_{\mathbf P}\), такую, что

\(\vdash_{\mathbf P} \mathbf G_{\mathbf P} \leftrightarrow \neg Proof(\overline{[\mathbf G_{\mathbf P}]})\)

Интуитивно можно сказать, что формула \(\mathbf G_{\mathbf P}\) утверждает свою же недоказуемость в рамках системы \(\mathbf P\). Гёдель доказал, что ни эта формула, ни её отрицание недоказуемы в \(\mathbf P\), формально установив, что:

• если \(\mathbf P\) непротиворечива, то \(\nvdash_{\mathbf P} \mathbf G_{\mathbf P}\);

• если \(\mathbf P\) является \(\omega\)-непротиворечивой, то \(\nvdash_{\mathbf P} \neg\mathbf G_{\mathbf P}\).

Теперь это утверждение известно как первая теорема Гёделя о неполноте. В доказательстве своей теоремы Гёдель построил в явном виде представимость отношения \(Proof(x, y)\) в \(\mathbf P\), которая в свою очередь вытекает из своего примитивно-рекурсивного определения.

Примитивно-рекурсивные функции и проблема разрешимости Гильберта-Аккермана. Другой мотивацией для работы над рекурсивными функциями в 1930-х годах было изучение неразрешимых проблем. Это включало определение того, является ли данная формула логики первого порядка общезначимой. Задача была впервые сформулирована как Entscheidungsproblem (или проблема разрешимости) для логической системы первого порядка, приведенной Гильбертом и Аккерманом, которая теперь известна как аксиоматическая система Гильберта.

Основная проблема заключается в том, существует ли процедура, которая может определить для каждой правильно построенной формулы системы, удовлетворяет ли она всем интерпретациям. Из теоремы, касающейся адекватности системы Гильберта, следует, что формула верна тогда и только тогда, когда она является теоремой системы. Таким образом, проблема разрешимости эквивалентна разрешимости логической выводимости в системе. По сути, это касается возможности алгоритмического поиска доказательств, чтобы определить, является ли формула логическим следствием формальной системы.

В 1936 году Черч и Тьюринг доказали несколько отрицательных результатов, касающихся проблемы разрешимости. Их работа считается основополагающей в развитии эффективной вычислимости, главным образом благодаря их определению примитивно-рекурсивных функций как класса эффективно вычислимых функций. Все результаты были основаны на построении неразрешимого множества натуральных чисел \(V\), которое состоит из чисел Геделя в допустимых формулах. Множество \(V\) неразрешимо, поскольку его характеристическая функция не является примитивно-рекурсивной.

Функция Аккермана: за рамками примитивно рекурсивных функций. Примитивно–рекурсивные функции считаются полностью вычислимыми, поскольку их значения для заданных входных данных могут быть систематически вычислены шаг за шагом с помощью рекурсии на основе определяющих выражений - аналогично тому, как формальное доказательство выполняется путем последовательных логических выводов. Однако теперь мы знаем, что существуют функции, значения которых все еще могут быть вычислены рекурсивно, но не классифицируются как примитивно-рекурсивные функции. Еще в конце 1920-х годов Гильберт и его коллеги осознали это ограничение и начали изучать то, что сейчас известно как общерекурсивные функции.

Сколем и Гильберт впервые предложили рекурсию высших типов, используя функционалы для определения рекурсивных функций. Одним из примеров является итерационный функционал \(Iter\), который принимает функцию \(f\) типа \(\mathbb N \to \mathbb N\) и число \(i\) и возвращает значение функции \(f\), примененной к самой себе \(i\) раз. Формально \(Iter\) - это функционал типа \((\mathbb N \to \mathbb N) \to (\mathbb N \to \mathbb N)\). Он принимает функцию на \(\mathbb N\) и возвращает функцию на \(\mathbb N\), которая определяется так:

\(Iter(f, 0) = Id, \quad Iter(f, i+1) = f \circ Iter(f, i)\)

где \((f \circ g)(x) = f(g(x))\). Таким образом, \(Iter(f, i)\) представляет собой \(f^{(i)}\), то есть функцию \(f\), примененную к себе \(i\) раз.

Теперь мы можем использовать функционал \(Iter\), чтобы определить функцию \(\beta\) типа \(\mathbb N \mapsto (\mathbb N \mapsto \mathbb N)\) “рекурсивно”:

\(\beta(0) = s, \quad \beta(i+1) = Iter(\beta(i), x)(\beta(i)(1))\)

Здесь \(s\) - это функция следования, т.е. \(s(x) = x + 1\). Например, \(\beta(0)(1) = 2\), и \(\beta(2)\) - это функция \(s^{(x)}(2) = s \circ s\). Поэтому \(\beta(2)(5) = 7\). В общем случае можем записать \(\beta(i)(j)\) как двухместную функцию \(\pi(x, y)\), которая называется функцией Петер (или функцией Аккермана-Петер). Несмотря на то, что для \(i = 0, 1, \ldots\) функция \(\pi(i, y)\) является вычислимой, она растет крайне быстро и выпадает из класса примитивно рекурсивных функций.

Позднее Аккерман определил функцию, эквивалентную \(\pi(x, y)\), используя рекурсию непосредственно на натуральных числах. Петер и Робинсон упростили ее, и сейчас она называется функцией Аккермана:

\(ACK(0, y) = y + 1\)

\(ACK(x+1, 0) = ACK(x, 1)\)

\(ACK(x+1, y+1) = ACK(x+1, ACK(x,y))\)

Аккерман назвал это определение одновременной рекурсией. Третий шаг определяет \(ACK(x+1, y+1)\) через \(ACK(x,y)\), что приводит к “вложенным вызовам функции”. Не сразу видно, что эта рекурсия завершается, но по мере уменьшения \(y\) или когда \(y\) достигает \(0\), \(x\) начинает уменьшаться, гарантируя, что процесс в конечном итоге завершится. Таким образом, несмотря на свой быстрый рост, функция Аккермана все еще вычислима за конечное число шагов, удовлетворяя требованию Гёделя о том, чтобы рекурсивно определенная функция была вычислима с помощью конечной процедуры.

Интерес к рекурсивным функциям, выходящим за рамки класса примитивно-рекурсивных функций, привел к систематическому изучению рекурсии. Термин “примитивно-рекурсивный” был впервые введен Петер в 1932 году, когда она использовала его для описания функций, определенных в уравнении Геделя. Этот термин стал стандартным после того, как был принят Клини в 1936 году.

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

Общерекурсивные функции. В 1930-х годах Гедель и Эрбран исследовали использование уравнений и подстановки в качестве общего способа описания рекурсии. Этот метод рассматривает вычисление функций как вывод в логике первого порядка без кванторов, где единственными допустимыми правилами являются замена переменных числами (нумералами) и замена термов в уравнениях числами, когда соответствующее тождество уже выведено. Гедель использовал термин “общерекурсивная” для обозначения функции, определенной таким образом. Теперь мы определяем рекурсивные системы, используя следующие синтаксические правила:

Определение.

1. Класс чисел \(Nat\) - это наименьшее множество, такое, что (1) оно содержит \(0\) и (2) если \(\overline{n} \in Nat\), то \(s(\overline{n}) \in Nat\). Здесь \(\overline{n}\) обозначает \(s(s(\ldots s(0)))\) (\(n\) раз).

2. Класс термов \(Term\) - это наименьшее множество, такое, что (а) оно содержит числа из \(Nat\) и переменные \(x_0, x_1, \ldots\), (б) если \(t \in Term\), то \(s(t) \in Term\), (в) если \(t_1, \ldots, t_n \in Term\), то \(\psi^n(t_1, \ldots, t_n) \in Term\) для любой \(n\)-местной примитивно рекурсивной функции.

3. Если \(u\) - это терм и \(t\) - это терм вида \(\psi^n(t_1, \ldots, t_n)\), где каждый терм \(t_i\) не содержит функциональных символов кроме \(s\), то \(t = u\) - это уравнение.

4. Система уравнений - это конечное множество уравнений. Через \(\mathcal E(\psi_1, \ldots, \psi_n, \vec x)\) обозначаем систему уравнений с функциональными символами \(\psi_1, \ldots, \psi_n\) и переменными \(\vec x = x_1, \ldots, x_k\).

Эрбран дал семантическую характеристику того, что означает определение числовой функции системой уравнений, которую Гедель позже формализовал как определение общерекурсивных функций.

Определение. Функция \(f \colon \mathbb N^k \to \mathbb N\) называется общерекурсивной функцией, если существует система уравнений \(\mathcal E(\psi_1, \ldots, \psi_n, \vec x)\) такая, что, если \(\psi_i^k\) - функциональный символ в левой части последнего уравнения в \(\mathcal E\), то для всех значений \(n_1, \ldots, n_k\) и \(m\):

\(f(n_1, \ldots, n_k) = m\)

тогда и только тогда, когда

\(\psi_i^k(\overline{n_1}, \ldots, \overline{n_k}) = \overline{m}\)

выводимо из \(\mathcal E\) по следующим правилам:

• Подстановка числа \(\overline{n}\) вместо любой переменной в уравнении.

• Если \(\psi_j^l(\overline{n_1}, \ldots, \overline{n_l}) = \overline{q}\) выведено, то \(\psi_j^l(\overline{n_1}, \ldots, \overline{n_l})\) можно заменить на число \(\overline{q}\) в правой части уравнения.

В этом случае \(\mathcal E\) определяет \(f\) через \(\psi_i^k\).

Это определение показывает, что значения общерекурсивных функций могут быть механически вычислены с использованием систем рекурсивных уравнений в качестве этапов логического вывода. Теперь известно, что при такой формальной семантической характеристике функция Аккермана-Петер и другие функции, определенные схемами, рассмотренными Гильбертом, а также все примитивно-рекурсивные функции могут быть определены общими системами рекурсивных уравнений. Следовательно, класс \(\mathbf {GR}\), определенный таким образом, образует собственный суперкласс класса примитивно-рекурсивных функций \(\mathbf {PR}\).

Однако серьезная проблема заключается в том, что система уравнений может быть противоречивой, например \(\{\varphi(x) = 0, \; \varphi(x) = s(0)\}\) и не иметь решения, в то время как некоторые другие, такие как \(\{\varphi x = \varphi x\}\), могут иметь более одного решения.

Рекурсивные функции и теория вычислимости. Работа над рекурсией, представленная до сих пор, является главным образом частью математической логики, направленной на создание основ математики, изложенных в программе Гильберта, в частности, касающихся арифметики. Это послужило основой для разработки теории рекурсивных функций в конце 1930-х годов, пионерами которой были Клини, Тьюринг, Черч и Пост. Ключевой темой в этой разработке является переход от метатеорий систем формальной логики к характеристике эффективной вычислимости. По этой причине современным термином для теории рекурсивных функций теперь является теория вычислимости, а рекурсивные функции обычно называют вычислимыми функциями.

Эффективная вычислимость отражает нашу интуицию в отношении алгоритмической вычислимости. Она поддерживает строгие доказательства, абстрагируясь от деталей моделей, таких как общерекурсивные функции Геделя. Позже Клини предложил определение частично рекурсивных функций с использованием оператора неограниченной минимизации, который заменил общерекурсивные уравнения Геделя, принятые в качестве стандарта. Позже это было заменено машинными определениями, такими как определение Тьюринга, которые напоминают современные компьютерные программы. Тем не менее, эти новые характеристики все еще сохраняли идею о вычислениях как об эффективных процессах в рамках “рекурсивного способа мышления”, как это понимали ранние математики и логики, такие как Сколем, Гильберт, Гедель и Петер. В дальнейшем мы введем определения различных замкнутых классов рекурсивных функций.

Во-первых, любой класс \(\mathbf X\) рекурсивных функций определяется на основе набора начальных функций \(\mathbf I_{\mathbf X}\). Для класса примитивных рекурсивных функций \(\mathbf{PR}\) начальные функции \(\mathbf{I_{PR}}\) включают константу \(0\), функцию следования \(s\) и проекционные функции \(\pi_i^k \colon \mathbb N^k \mapsto \mathbb N\), которые определяются для каждого \(i\) и \(k\) по формуле

\(\pi_i^k(x_1, \ldots, i, \ldots, x_k) = x_i\)

Затем примитивно рекурсивные функции определяются через функционалы, называемые композицией (суперпозицией) и примитивной рекурсией.

Определение. Операторы суперпозиции и примитивной рекурсии определяются следующим образом.

• Для любых натуральных чисел \(l\) и \(k\) оператор суперпозиции \(Comp_k^l\) принимает заданные функции \(f \colon \mathbb N^l \mapsto \mathbb N\) и \(g_1, \ldots, g_l \colon \mathbb N^k \mapsto \mathbb N\) и возвращает функцию \(Comp_k^l[f, g_1, \ldots, g_l] \colon \mathbb N^k \mapsto N\), определяемую формулой

\(Comp_k^l(f, g_1, \ldots, g_l)(x_0, \ldots, x_k) = f(g_1(x_1, \ldots, x_k), \ldots, g_l(x_1, \ldots, x_k))\)

• Для любых натуральных чисел \(k\) оператор примитивной рекурсии \(PrimR_k^l\) принимает на вход функции \(f \colon \mathbb N^k \mapsto \mathbb N\) и \(g \colon \mathbb N^{k+2} \mapsto \mathbb N\) и возвращает функцию \(PrimR_k[f, g] \colon \mathbb N^{k+1} \mapsto \mathbb N\), такую, что

\(PrimR_k[f,g](x_1, \ldots, x_k, 0) = f(x_1, \ldots, x_k)\)

\(PrimR_k[f, g](x_1, \ldots, x_k, y+1) = g(x_1, \ldots, x_k, y, PrimR_k[f,g](x_1, \ldots, x_k, y)\)

Введем формальные определения примитивно рекурсивных функций и примитивно рекурсивных отношений.

Определение. Класс примитивно рекурсивных функций \(\mathbf{PR}\) - это наименьший класс функций, содержащий начальные функции \(\mathbf{I_{PR}} = \{0, s, \pi_i^k \colon i, k \in \mathbb N\}\) и замкнутый относительно операторов \(Op_{\mathbf{PR}} = \{Comp_k^l, PrimR_j \colon k, l, j \in \mathbb N\}\).

Отношение \(R \subset \mathbb N^k\) - это примитивно рекурсивное отношение, если его характеристическая функция примитивно рекурсивна:

\( \chi_R(x_1, \ldots, x_k) = \begin{cases} 1, & \text{если выполняется }R(x_1, \ldots, x_k),\\ 0, & \text{если выполняется }\neg R(x_1, \ldots, x_k) \end{cases} \)

Следовательно, для рекурсивного отношения \(R\) существует алгоритм или механическая процедура, которая возвращает \(1\) на входе \(\vec n\), если \(R\) выполняется для \(\vec n\), и выдает \(0\), если \(R\) не выполняется для \(\vec n\).

Теперь класс \(\mathbf{PR}\) рекурсивных функций можно формально определить как минимальное замыкание множества \(\mathbf I_{\mathbf{PR}}\) относительно функций из \(Op_{\mathbf {PR}}\).

Определение. Класс примитивно рекурсивных функций \(\mathbf{PR}\) определяется как подкласс класса \(\bigcup\limits_{k \in \mathbb N} (\mathbb N^k \mapsto \mathbb N)\), такой, что выполняются следующие свойства:

1. \(\mathbf I_{\mathbf{PR}} \subset \mathbf {PR}\);

2. Для \(l, k \in \mathbb N\) и \(f, g_1, \ldots, g_l \in \mathbf{PR}\), если \(f\) - это \(l\)-арная функция и \(g_i\) - это \(k\)-арная (для \(1 \leq i \leq l\)), тогда \(Comp_k^l[f, g_1 ,\ldots, g_l] \in \mathbf {PR}\);

3. Для всех \(k \in \mathbb N\) и любой \(k\)-арной функции \(f\) и любых \((k+2)\)-арных функций \(g\), если \(f, g \in \mathbf{PR}\), то \(PrimR_k[f, g] \in \mathbf{PR}\).

В современной математической логике язык формальных логических систем обычно определяется через свойства замыкания. Хорошо известно, что класс \(\mathbf {PR}\) является счетным, и каждый элемент в этом классе имеет алгоритмические спецификации для вычисления семантики функции. Задача программирования состоит в том, чтобы выразить вычислительную задачу в виде спецификации в рамках \(\mathbf{PR}\). Кроме того, класс примитивно-рекурсивных отношений замкнут относительно базовых логических операций (логическими связями): отрицания (\(\neg\)), конъюнкции (\(\land\)) и дизъюнкции (\(\vee\)). Различные функции, определяемые различными свойствами замыкания, эквивалентны \(\mathbf {PR}\).

Ранее мы видели, что функция Аккермана-Петер, построенная с помощью “рекурсии”, не является элементом класса \(\mathbf {PR}\). Кроме того, известно, что множество всех функций над натуральными числами несчетно. Следовательно, должны существовать функции, которых нет в \(\mathbf{PR}\).

Другой способ понять существование непримитивных рекурсивных функций - это любое перечисление \(\mathbf {PR}\), скажем, \(f_0\), \(f_1\), \(f_2\), … Для перечисления мы можем определить функцию \(g\) таким образом, что \(g (n) = f_n (n) + 1\). Используя метод диагонализации, можно показать, что \(g (n)\) не является элементом \(\mathbf{PR}\). Это показывает, что существуют интуитивно эффективные процедуры для вычисления такой функции \(g\). Задача состоит в том, чтобы определить класс “общих” функций, которые расширяют \(\mathbf {PR}\), сохраняя при этом четко определенные свойства замыкания. Это достигается с помощью оператора минимизации (\(µy\)). Для любой \((k + 1)\)-арной частичной функции \(f\) мы определяем выражения вида \((\mu y ) f( x_1, \ldots , x_k, y )\) следующим образом:

\( (\mu y)f(x_1, \ldots, x_k, y) = \begin{cases}z, & \text{если } f(x_1, \ldots, x_k, z) = 0 \text{ и }\\ & (\forall m < z)(f(x_1, \ldots, x_k, m) > 0), \\ \text{не определена} & \text{иначе} \end{cases} \)

Поэтому \(\mu y\) - это функция, которая отображает \((k+1)\)-арную функцию в \(k\)-арную функцию. Определение указывает для любого заданного входного значения \(\vec n\) процесс поиска наименьшего значения \(m\), такого, что \(f(n, m) = 0\). Значение \(((\mu y )f)(n)\) не определено, если либо нет такого \(m\), для которого \(f(n, m) = 0\), либо если такое \(m\) существует, но \(f(\vec n, w )\) не определено для некоторого \(w < m\). Давайте используем \(\mu_k\) для определения оператора, который отображает \(( k + 1)\)-арную функцию функцию в \(k\)-арную функцию, а затем определим класс частично рекурсивных функций \(\mathbf{PartRF}\), которые также называются \(\mu\)-рекурсивными функциями.

Определение. Класс частично рекурсивных функций \(\mathbf{PartRF}\) - это наименьший подкласс частичных функций \(\bigcup\limits_{k \in \mathbb N} (\mathbb N^k \mapsto \mathbb N)\), содержащий начальные функции \(I_{\mathbf PR} = \{0, s, \pi_k^i \colon i, k \in \mathbf N\}\), замкнутый относительно операторов \(\{Comp_k^l, PrimR_k, \mu_k \colon k, l \in \mathbb N\}\). Назовем \(f \in \mathbf{PartRF}\) рекурсивной функцией, если она тотальна. Класс рекурсивных функций обозначим \(\mathbf {RF}\).

Итак, мы рассказали о развитии теории рекурсивных функций. Изучение рекурсивных функций началось с изучения логических основ математики, в частности программы Гильберта. Это сыграло решающую роль в доказательстве теорем Геделя и систематической формализации рекурсивных уравнений, которые определяют класс общих рекурсивных функций \(\mathbf {GR}\), главным образом благодаря усилиям Клини.

С тех пор теория развивалась с акцентом на вычислимость и в настоящее время широко известна как теория вычислимости. Известный тезис Черча утверждает, что \(\mathbf{GR}\) и \(\mathbf{RF}\) эквивалентны, и Черч называет их вычислимыми функциями. Позже этот тезис был расширен до того, что теперь известно как тезис Черча-Тьюринга, который, по сути, утверждает, что класс рекурсивных функций \(\mathbf{RF}\) эквивалентен классу функций, определяемых в λ-исчислении, а также сравним с классом функций, вычисляемых машиной Тьюринга.

Лямбда-исчисление

Лямбда-исчисление, обычно записываемое как λ-исчисление, представляет собой формальную математическую систему, часто рассматриваемую как теория вычислений, в основном служащую основой для функционального программирования. На заре своего развития λ-исчисление сочеталось с комбинаторной логикой для изучения основ математики. Оно было введено Алонзо Черчем в 1930-х годах как часть математической логики и было предназначено для анализа проблем непротиворечивости и разрешимости.

По сути, λ-исчисление - это простая запись функций и применений функций. Элементы ключевых идей применения функции к аргументу и формирования функций с помощью абстракции можно найти еще в 1890-х годах в работе Фреге. Фреге показал, что достаточно сосредоточиться на унарных функциях, рассматривая операцию многоарности как последовательность абстракций, которые приводят к эквивалентной унарной функции. Например, бинарная функция \(f \colon \mathbb N \times \mathbb N \to \mathbb N\) может быть преобразована с помощью “фрегеирования” в функцию \(Frege( f ) \colon \mathbb N \to (\mathbb N \to \mathbb N)\). Однако теперь это хорошо известно как функция каррирования, по имени логика Хаскелла Карри.

Механизм абстракций в λ-исчислении позволяет описывать функции с помощью выражений (или термов), не прибегая к функциональным символам (или именам). Например, вместо того, чтобы записывать функцию в виде \(f( x ) = 2∗ x^2 + 3∗x + 5\), мы используем терм \((\lambda x.(2∗ x^2 + 3∗ x + 5))\). Применение \(f( x )\) к значению \(x = n\) записывается как терм \(((\lambda x. (2 ∗ x^2 + 3∗x + 5))n)\), где \(n\) также является термом. Например, если \(n = 2\), то у нас есть следующие этапы вывода для вычисления:

\(((\lambda x. (2 ∗ x^2 + 3∗x + 5))2) \to 2 * 2^2 + 3 * 2 + 5\) (подставили \(2\) на место \(x\))

\(= 8 + 6 + 5 = 19\)

Первым шагом в этом вычислении является преобразование абстрактного терма в другой термин путем подстановки. Это преобразование называется \(\beta\)-преобразованием и приблизительно определяется как \(((\lambda x.M ) N ) \triangleright M [ N / x ]\), где \(M [ N / x]\) - это терм, полученный из \(M\) путем подстановки \(N\) за место всех вхождений \(x\).

Синтаксис. Будучи формальной системой, λ-исчисление имеет синтаксическую и семантическую модель.

Определение. Алфавит языка λ-исчисления состоит из открывающих и закрывающих скобок “(”, “)” и бесконечного множества переменных. Класс λ-термов определяется индуктивно:

1. Каждая переменная - это λ-терм.

2. Если \(M\) и \(N\) - это λ-термы, то и \((MN)\) - это λ-терм.

3. Если \(M\) - это λ-терм и \(x\) - это переменная, то \((\lambda x.M)\) - это λ-терм.

Правило 2 носит название аппликации, тогда как правило 3 - это абстракция. Вместо \((\lambda x.M)\) и \((MN)\) мы будем писать \(\lambda x.M\) и \(MN\). В последовательности термов примем левоассоциативное соглашение: запись \(M_1M_2M_3\) понимается следующим образом: \(((M_1M_2)M_3)\).

В рамках этих синтаксических правил операция подстановки в \(\beta\)-преобразовании определяется индуктивно:

1. \(x[N/x] \equiv N\), \(y [N/x] \equiv y\) при условии, что \(y\) - это переменная, отличная от \(x\).

2. \((MN)[L/x] \equiv (M[L/x]N[L/x])\).

3. \((\lambda x.M)[N/x] \equiv (\lambda x.M)\), \((\lambda y.M)[N/x] \equiv (\lambda y.M[N/x])\) при условии, что \(y\) - это переменная, отличная от \(x\).

Как и при использовании кванторов в языке первого порядка, \(M\) в терме \((\lambda x.M )\) называется областью действия абстракции \(\lambda x\), а \(x\) называется связанной этой абстракцией. Любая переменная, которая не входит в область действия какой-либо абстракции, называется свободной. Следовательно, в \(\beta\)-преобразовании \(M [ N / x ] \) обозначает подстановку \(N\) на место свободных вхождений \(x\) в \(M\).

Основные правила вывода. Вывод \(\lambda\)-термов производится с помощью правил преобразования. В базовом \(\lambda\)-исчислении имеется два таких правила:

• \(\alpha\)-преобразование: \((\lambda x.M) \to (\lambda y.M)[x/y]\)

• \(\beta\)-преобразование: \((\lambda x.M)N \to M[N/x]\) при условии, что ни одна из свободных переменных терма \(N\) не станет связанной после подстановки \(N\) в терм \(M\). Другими словами, никакая свободная переменная \(y\) терма \(N\) не должна находиться в области действия абстракции \((\lambda y.N_1)\) в терме \(M\).

Заметим, что α-преобразование является двунаправленным, в то время как β-преобразование отражает смысл абстракции функций и их применения.

Как и в системе первого порядка, принцип, согласно которому свободные переменные должны оставаться свободными при β-преобразовании, называется правилом отсутствия захвата переменных. Это может быть обеспечено путем выполнения достаточного количества α-преобразований всякий раз, когда переменная рискует оказаться связанной во время подстановки. Например, мы не можем применить \((\lambda x. ((\lambda y. ( x ( y− 5)))))\) непосредственно к члену \(2∗ y\). Однако мы можем сначала получить \((\lambda x. ((\lambda z. ( x ( z − 5)))))\), применив α-преобразование к \((\lambda x. ((\lambda y. ( x ( y− 5)))))\), а затем применить β-преобразование:

\((\lambda x.((\lambda z.(x(z-5)))))(2*y) \to (\lambda z.((2*y)(z-5)))\)

Теория равенства. В теории множеств функции рассматриваются как экстенциональные объекты, представляющие функцию как набор пар вход-выход. Две функции \(f\) и \(g\) равны, если соответствующие им множества равны. Другими словами, \(f = g\) тогда и только тогда, когда их выходные данные одинаковы для всех входных данных \(n\), т.е. \(f(n) = g (n)\). Это концепция “функций-множеств”.

\(\lambda\)-исчисление, однако, использует концепцию “функций-правил”, и функции задаются интенционально в виде термов. Преобразования позволяют с ними работать, а аксиомы и правила вывода характеризуют их равенство.

Теория равенства \(\mathbf\Lambda\), прежде всего, содержит правила рефлексивности, симметричности и транзитивности:

\((Ref) \dfrac{}{M=M}\)

\((Sym) \dfrac{M=N}{N=M}\)

\((Tran) \dfrac{M=N,\;N=K}{M=K}\)

Есть также правила для абстракции и аппликации:

\((App) \dfrac{M=N}{AM = AN}, \;\; \dfrac{M=N}{NA=MA}\)

\((Abs) \dfrac{M=N}{\lambda x.M = \lambda x.N}\)

Заключительное и наиболее важное правило вывода - это \(\beta\)-сцепление:

\(\dfrac{}{(\lambda x.M)A = M[A/x]}\)

Таким образом, равенство в этой теории - это отношение конгруэнтности.

Семантические модели. Хотя λ-исчисление в основном описывает функции и их применение, определение их семантики может оказаться неожиданно сложным. Мы могли бы естественным образом интерпретировать каждый λ-член \(M\) как функцию \(f_M\) в некоторой области \(D\), а аппликацию \(MN\) - как применение функции \(f_M ( f_N )\).

Серьезная проблема возникает при самоприменении, например, \(xx\). Семантика \(x\) - это функция \(f_x\), которая возвращает \(f_x( f)\) при задании функции \(f\). Однако применение \(f_x\) к самой себе приводит к \(f_x ( f_x )\) в качестве выходных данных. Если мы представим \(f_x\) как набор пар, то получим \(fx =\{ \ldots ,(f_x, f_x (f_x )), \ldots \}\), что создает циклическое определение. Наборы, подобные этому, исключены из стандартной аксиоматической теории множеств.

Даже если мы будем использовать понятие функций-правил вместо функций-множеств, мы все равно столкнемся с проблемами. Поскольку все λ-термы являются функциями, их применения также являются функциями. Если мы предположим, что функции, соответствующие λ-термам, образуют область \(D\), то мы можем доказать, что существует взаимно однозначное соответствие между \(D\) и \(D \mapsto D\), множеством функций из \(D\) в \(D\). Однако известно, что это невозможно.

Из-за этих трудностей вопрос о том, возможно ли создать теоретико-множественную модель для λ-исчисления, долгое время оставался без ответа. В 1969 году Скотт представил модель под названием \(D_\infty\) в неопубликованной рукописи. Позже это развилось в теорию предметных областей Скотта, которая легла в основу денотационной семантики языков программирования.

В следующем разделе будет рассмотрена денотационная семантика языков программирования, определенная на основе полных частичных порядков (CPOs), ключевого понятия в теории предметных областей Скотта. Далее мы обсудим, как можно определить денотационные модели для λ-исчисления, следуя подходу синтаксических интерпретаций для логических систем первого порядка. Такая семантическая модель называется синтаксической λ-моделью.

Синтаксическая λ-модель основана на математической структуре, называемой аппликативной структурой, которая состоит из пары \(( D, \cdot)\), где \(D\) - множество, а \(\cdot\) - бинарная операция на \(D\). Мы используем оценку \(\sigma\) для присвоения каждой переменной значения \(\sigma( x )\in D\). В теории программирования \(\sigma\) также называется состоянием переменных.

Обновление переменной \(x\) в оценке (или состоянии) \(\sigma\) до значения \(d\in D\) записывается как \(\sigma[ x \in d ]\). Эта обновленная оценка удовлетворяет следующим условиям: \(\sigma [ x \leftarrow d ]( x ) = d\) и \(\sigma [ x \leftarrow d ]( y ) = \sigma ( y )\), если \(y\) отличается от \(x\).

Для данной оценки \(\sigma\) семантический λ-терм \(M\) является функцией в \(D\), которую он представляет.

Определение. Синтаксическая λ-модель представляет собой тройку \(\mathcal M = ( D, \cdot,[[]])\), где \(( D, \cdot)\) - это аппликативная структура, а \([[]]\) - функция, которая присваивает каждому λ-терму \(M\) и оценке \(\sigma\) означивание \([[ M ]]_\sigma \in D\), при соблюдении следующих условий:

1. \([[x]]_\sigma = \sigma(x)\)

2. \([[MN]]_\sigma = [[M]]_\sigma \cdot [[N]]_\sigma\)

3. \([[\lambda x.M]]_\sigma \cdot d = [[M]]_{\sigma[x \leftarrow d]}\) для всех \(d \in D\)

4. \([[\lambda x.M]]_\sigma = [[\lambda x.N]]_\sigma\), если для всех \(d \in D\) выполняется \([[M]]_{\sigma[x \leftarrow d]} = [[N]]_{\sigma[x \leftarrow d]}\)

5. \([[M]]_\rho = [[M]]_\sigma\), если \(\rho(x) = \sigma(x)\) для каждой свободной переменной \(x\) терма \(M\)

Тогда мы говорим, что синтаксическая λ-модель \(\mathcal M\) удовлетворяет уравнению \(M = N\), обозначаемому как \(M = N\), если \([[ M ]]_\sigma =[[ N ]]_\sigma\) для всех оценок \(\sigma\). Таким образом, мы получаем следующую теорему о корректности основной теории равенства \(\mathbf \Lambda\).

Теорема. Для любых \(\lambda\)-термов \(M\) и \(N\), если \(\mathbf \Lambda \vdash M = N\), то \(\mathcal M \models M = N\) для любой синтаксической \(\lambda\)-модели \(\mathcal M\).

Обсудим, в каких случаях существует синтаксическая \(\lambda\)-модель. Рассмотрим класс эквивалентности \([M]_{\mathbf \Lambda} = \{N \colon \mathbf \Lambda \vdash M = N\}\) для каждого \(\lambda\)-терма \(M\). Затем определим аппликативную область \(D_{\mathbf \Lambda} = (\{[M]_{\mathbf \Lambda} \colon M \text{ - это }\lambda\text{-терм}\}, \cdot)\), где \([M]_{\mathbf \Lambda} \cdot [M]_{\mathbf \Lambda} = [MN]_{\mathbf \Lambda}\). Определим семантическую функцию \([[]]\) так, чтобы для любой оценки \(\sigma\) на \(D_{\mathbf \Lambda}\) и любого \(\lambda\)-терма \(M\):

\([[M]]_\sigma = [M[N_1/x_1, \ldots, N_k/x_k]_{\mathbf\Lambda}\), если \(\sigma(x_i) = [N_i]_{\mathbf\Lambda}\) для свободных переменных \(x_i\) терма \(M\)

Тогда \(\mathcal I = (D_{\mathbf \Lambda}, \cdot, [[]])\) - это синтаксическая \(\lambda\)-модель, называемую моделью термов \(\lambda\)-исчисления, и \(\mathcal I \models M = N\) тогда и только тогда, когда \(\Lambda \vdash M = N\). Отсюда вытекает полнота системы \(\mathbf \Lambda\).

Теорема. Для любых \(\lambda\)-термов \(M\) и \(N\), если \(\mathcal M \models M = N\) для всех синтаксических \(\lambda\)-моделей \(\mathcal M\), то \(\mathbf \Lambda \vdash M = N\).

Связь между λ-исчислением и вычислениями устанавливается посредством определения числовых функций в λ-исчислении и тезиса Черча-Тьюринга, который утверждает, что класс функций, определяемых в λ-исчислении, и класс рекурсивных функций \(\mathbf {RF}\) - это одно и то же. Расширением λ-исчисления является типизированное λ-исчисление.

λ-исчисление - это формальная система в математической логике, которая использует функциональный подход к вычислениям. Логическое программирование - это еще один более поздний логический подход к программированию, первоначально разработанный в 1960-х и 1970-х годах, в основе которого лежат отношения, а не функции. Это обеспечивает возможность недетерминированного выполнения, поскольку Prolog - широко используемый язык реализации, основанный на предложениях Хорна, предложенных логиком Альфредом Хорном в 1951 году. Эти предложения обычно записываются в виде импликации \(( p \land q \land \ldots \land t) \Rightarrow u\) или в Прологе с использованием обратной формы u :- p, q, ..., t.

Машины Тьюринга

Машины Тьюринга, представленные Аланом Тьюрингом в его новаторской статье в рамках исследования основ математики, служат абстрактной моделью для изучения того, что может быть вычислено. Тьюринг использовал эти машины для отрицательного ответа на проблему разрешимости Гильберта-Аккермана.

Интуитивно понятно, что машина Тьюринга, которую Тьюринг первоначально назвал автоматической машиной (или а-машиной), имитирует шаги в человеческом решении вычислительной задачи. Машина состоит из следующих элементов:

• бесконечная лента, разделенная на ячейки, в которые могут быть записаны символы из алфавита;

• каретка для считывания и записи, которая указывает на определенную ячейку на ленте в любой момент времени;

• конечное число состояний, которое используется для определения инструкций, управляющих действиями машины на каждом этапе вычислений:

  • В заданном состоянии \(q\), зная символ \(a\) в ячейке под кареткой, машина может заменить \(a\) символом \(b\) (где \(b\) может быть равно или не совпадать с \(a\)), переместить каретку на одну ячейку влево или вправо и изменить состояние с \(q\) на \(q'\) (или остаться в \(q\)).

Машины Тьюринга были предложены для определения вычислимых функций. Функция является вычислимой, если для ее вычисления существует машина Тьюринга. Использование бесконечной ленты и инструкций машины подразумевает, что для вычисления “вычислимой” функции может потребоваться сколь угодно большая память и сколь угодно большое время. Таким образом, машины Тьюринга служат широкой и общей моделью вычислений: ни одна функция не окажется невычислимой исключительно из-за ограничений по времени или памяти. Однако некоторые функции могут быть вычислены по Тьюрингу, но не могут быть вычислены ни на одном существующем физическом компьютере. Основные исследования в области теории сложности вычислений и разработки алгоритмов сосредоточены на функциях, которые реально и эффективно вычисляются существующими компьютерами.

Формальное определение. Дадим формальное определение машин Тьюринга в соответствии с изменениями, внесенными Постом.

Определение. Машина Тьюринга - это четверка \(T = (Q, \Sigma, q_0, \delta)\), где

• \(Q\) - конечное множество состояний,

• \(\Sigma\) - конечное множество символов, называемое алфавитом,

• \(q_0 \in Q\) - начальное состояние,

• \(\delta\) - функция переходов \(\delta \colon (Q \times \Sigma) \to (\Sigma \times \{L, R\} \times Q)\), определяющая переход к следующему шагу вычислений.

Если \(\delta(q, a) = (a', D, q')\), то это означает, что когда машина Тьюринга \(T\) находится в состоянии \(q\) и считывает символ \(a\), она заменяет \(a\) на \(a'\), перемещается в направлении \(D \in \{L, R\}\) и переходит при этом в состояние \(q'\).

Алфавит \(\Sigma\) представляет область определения входных и выходных данных, состояния образуют множество \(Q\), а функция переходов указывает набор инструкций программы для выполнения вычисления. Для машины Тьюринга \(T\) определим \(\Sigma^*\) - набор конечных последовательностей символов из \(\Sigma\), включая пустую последовательность \(\varepsilon\). При наличии двух последовательностей \(\rho, \sigma \in \Sigma^*\), состояния \(q \in Q\) и символа \(a \in \Sigma\) выражение \(\rho q a \sigma\) называется конфигурацией машины \(T\). Когда \(q\) - начальное состояние, она называется начальной конфигурацией, а \(\rho a \sigma\) - входными данными. Если \(\delta (q, a) \) не определено, то \(\rho q a \sigma\) называется конечной (терминальной) конфигурацией.

Работа машины \(T\) начинается с начальной конфигурации \(\rho q_0 a \sigma\), шаг за шагом машина действует согласно своей функции перехода и в конечном итоге достигает конечной конфигурации \(\rho'q' a' \sigma'\), где \(\rho' a' \sigma'\) - это выход машины \(T\) на входе \(\rho a \sigma\). Обратим внимание, что вычисление может никогда не завершиться.

Таким образом, с помощью алфавита и набора состояний конфигурация может быть определена аналогично термам и формулам в системе формальной логики, а функция перехода действует как набор “правил вывода” для вывода. Как и в теории рекурсивных функций и λ-исчислении, вычисления выполняются шаг за шагом в виде последовательности выводов.

Тезис Черча-Тьюринга. Машины Тьюринга изначально были разработаны для формализации концепции вычислимости для решения проблемы принятия решений. Как обсуждалось ранее, эта фундаментальная математическая проблема привела к независимым, но логически эквивалентным формулировкам, таким как рекурсивные функции и λ-исчисление. Сегодня в компьютерном сообществе хорошо известно, что машины Тьюринга, наряду со всеми логически эквивалентными моделями вычислений, охватывают все вычислимые задачи. Для любой вычислимой задачи существует машина Тьюринга, которая ее вычисляет. Это известно как тезис Черча-Тьюринга. Мы можем понять этот тезис в двух ключевых аспектах:

1. Любая задача, не поддающаяся вычислению с помощью машины Тьюринга, не является вычислимой в абсолютном смысле (“по крайней мере, абсолютно относительно человека”) и, следовательно, не может быть выражена в виде рекурсивной функции или определена в λ-исчислении;

2. Для любой задачи, которую мы считаем вычислимой, мы должны быть в состоянии сконструировать машину Тьюринга для ее вычисления. Следовательно, соответствующая машина Тьюринга может быть сконструирована для любой рекурсивной функции или λ-определимой функции.

В своей статье Тьюринг представил свои а-машины для вычисления (вещественных) чисел, которые он назвал вычислимыми числами, стремясь охватить “(все) возможные процессы, которые могут быть выполнены при вычислении числа”. Он предполагал:

“Я утверждаю, что (операции вычислительной машины) включают в себя все те, которые используются при вычислении числа.”

Тьюринг определил действительное число как вычислимое, если существует a-машина, которая вычисляет сколь угодно точное приближение этого числа. Такое вычислимое число теперь называется вычислимым по Тьюрингу числом. Алгебраические числа (корни многочленов с алгебраическими коэффициентами) и многие трансцендентные математические константы, такие как \(e\) и \(\pi\), вычислимы по Тьюрингу.

Вычисления с помощью машин Тьюринга. Теория рекурсивных функций, λ-исчисление и машины Тьюринга изначально разрабатывались для решения проблемы разрешимости Гильберта-Аккермана. Когда-то эти области занимали центральное место в математической логике, а теперь стали основополагающими моделями для вычислимости, теоретической информатики, языков программирования и верификации программ.

Типичная задача принятия решения заключается в следующем: “Обладает ли данный входной сигнал \(x\) свойством P?” Это включает в себя вычисление характеристической функции входных данных, равной \(P\) (true или false). Ключевой задачей при применении этих моделей в информатике является интерпретация как входных данных \(x\), так и свойства \(P\) таким образом, чтобы сделать задачу вычислимой. Это соединяет вычислительную науку и приложения реального мира.

Например, в практических задачах может потребоваться определить, можно ли доверять цифровому источнику. Для этого необходимо определить \(P ( x )\), где \(x\) представляет источник, для которого нужно решить, является ли \(x\) надежным. Чтобы продемонстрировать простое вычисление, мы сложим два натуральных числа на машине Тьюринга.

Мы интерпретируем символы \(\Sigma\) на ленте как представляющие два натуральных числа в унарной записи: \(1\) для \(0\) и \(n + 1\) единиц для числа \(n\) (например, 1111 для числа 3). Два входа разделены значением 0, поэтому 11110111111 представляет собой входы 3 и 4.

Машина Тьюринга \(T_{add2} = (Q, \Sigma, q_0, \delta)\) вычисляет сумму \(n+m\). Определим состояния \(Q = \{q_0, q_1, q_2, q_3, q_f\}\), алфавит ленты \(\Sigma = \{0, 1\}\) и следующую функцию переходов \(\delta\):

\(\delta(q_0, 1) = (0, R, q_1)\), стереть самую левую 1 и пройти до \(q_1\);

\(\delta(q_1, 1) = (1, R, q_1)\), прочитать \(n\) единиц, находясь в состоянии \(q_1\), пока не встретим 0;

\(\delta(q_1, 0) = (1, R, q_2)\), поменять 0 на 1 и перейти в состояние \(q_2\);

\(\delta(q_2, 1) = (1, R, q_2)\), прочитать \(m+1\) единиц, находясь в состоянии \(q_2\), пока не встретим 0;

\(\delta(q_2, 0) = (0, L, q_3)\), переместиться влево и перейти в состояние \(q_3\);

\(\delta(q_3, 1) = (0, R, q_f)\), стереть лишнюю 1 и остановиться.

Эта машина Тьюринга выполняет сложение двух чисел в унарной системе счисления.

От чисел до универсальной машины Тьюринга. То, как вычислимые по Тьюрингу числа соотносятся с общими задачами вычисления и принятия решений, может быть не сразу очевидно. Вычислимая (или разрешимая) задача решается путем выполнения пошаговой процедуры, известной как алгоритм. Тьюринг формализовал эту идею, используя машину Тьюринга. Таким образом, фраза “существует общий процесс определения” переводится как “существует машина, которая будет это определять”. Тьюринг опирался на понимание Геделя о том, что даже абстрактные задачи, такие как логические формулы и доказательства теорем, могут быть закодированы как числовые задачи с использованием гёделевских нумераций. Тьюринг продемонстрировал, что задачи “общего процесса” и решающие их машины могут быть закодированы численно, что имело решающее значение для создания универсальной машины Тьюринга (UTM) и доказательства того, что некоторые проблемы не могут быть решены ни одной машиной Тьюринга.

UTM, по сути, является машиной Тьюринга, способной промоделировать любую другую машину Тьюринга. Согласно тезису Черча-Тьюринга, все, что может быть вычислено с помощью любого процесса, может быть вычислено с помощью UTM. И наоборот, если UTM не может вычислить проблему, то эта проблема не поддается вычислению. Хотя техническая структура UTM выходит за рамки данной главы, мы приводим краткое изложение основных идей.

Согласно Тьюрингу, UTM предназначена для того, чтобы (1) “понимать” программу любой машины \(T_n\) и, основываясь на этом понимании, (2) “имитировать” поведение \(T_n\). Для этого необходим метод, позволяющий взаимозаменяемо обрабатывать программу и поведение \(T_n\), поскольку одна и та же машина обрабатывает и то, и другое на одной и той же ленте. Это делается в два этапа:

1. Тьюринг ввел нотацию для представления как программы, так и поведения машин. Это позволяет представить программу \(T_n\) в виде последовательности символов, которую машина может обрабатывать так же, как и любые другие данные. Тьюринг назвал это описанием того, “что должна делать \(T_n\)”.

2. Тьюринг определил набор элементарных функций, которые работают с символами, записанными на ленте, таких как перемещение ленты, чтение, запись или стирание символов. Эти функции применимы как к программным символам, так и к входным данным. Тьюринг назвал это описанием того, “что делает \(T_n\)”.

Первым и, возможно, самым важным шагом в построении UTM является обозначение для ее четырех элементов \((Q, q_0, \Sigma, \delta)\) на шаге (1) и для конфигураций машины на шаге (2). Тьюринг разделил ленту на две области: область \(A\) содержит программу \(T_n\), а область \(B\) содержит последовательные конфигурации (т.е. функции перехода) \(T_n\). Для разделения двух областей использовался дополнительный символ “::”.

Построение универсальной машины Тьюринга (UTM) сыграло решающую роль в доказательстве Тьюрингом неразрешимости проблемы остановки, что было основной целью его статьи: показать, что проблема разрешимости для логики первого порядка не имеет решения. Доказательство основывалось на критических идеях, таких как кодирование каждой машины Тьюринга описательным номером, включая самореференцию и противоречие, а также использование диагонального метода. В частности, это связывало проблему принятия решения о том, обладает ли машина Тьюринга определенным свойством (например, является круговой), с вопросом о том, удовлетворяет ли число заданному свойству. Метод доказательства также продемонстрировал два основных метода доказательства того, что задача принятия решения \(D\) не поддается вычислению.

• Косвенное доказательство: возьмем некоторую задачу \(D\), о которой уже известно, что она неразрешима, и покажем, что задача “сводится” к \(D\). Это доказывает, что \(D\) также не является вычислимой, поскольку в противном случае \(D\) была бы вычислимой.

• Прямое доказательство: доказать невычислимость \(D\) напрямую, приняв некоторую версию тезиса Черча-Тьюринга.

Широко распространено мнение, что основная идея концепции хранимой программы в архитектуре программируемых компьютеров Джона фон Неймана была вдохновлена методом обработки как программы, так и поведения всех машин Тьюринга на одной и той же ленте UTM. Благодаря теоретической мощи машин Тьюринга и их значительному влиянию на аппаратную реализацию, Тьюринг признан не только отцом-основателем информатики, но и, по некоторым оценкам, отцом современного компьютера.

Единая точка зрения на вычислительные модели. Теория рекурсивных функций, λ-исчисление и машины Тьюринга (включая продукционные системы Поста) - все это демонстрирует, что процесс вычислений эквивалентен формальным логическим выводам. Эти модели – машины Тьюринга и системы Поста – являются основополагающими для понимания того, что любую вычислительную задачу можно рассматривать как формальное доказательство в рамках логической системы. Эта концепция лежит в основе тезиса Черча-Тьюринга, который утверждает эквивалентность различных моделей вычислений с точки зрения выразительности.

Однако важно подчеркнуть, что понятие “доказательство в логической системе” не включает в себя уточнение того, какие теоремы пользователь заранее намеревается доказать. Другими словами, формальное доказательство, получаемое в результате вычисления, не имеет отношения к тому, что семантически предназначено для вычисления или доказательства. При традиционной разработке программы функциональность программы должна быть указана в спецификации. Затем проверка корректности программы включает демонстрацию того, что логическое доказательство, реализованное путем выполнения разработанной программы, удовлетворяет спецификации. Например, предположим, что программа \(GCD( x, y )\) предназначена для вычисления наибольшего общего делителя двух целочисленных входных данных \(x\) и \(y\). Последовательность формальных логических выводов, полученных в результате выполнения \(GCD\), показывает, что ее выходные данные являются наибольшим общим делителем входных данных. Это будет более подробно разъяснено в следующем разделе, посвященном логике программ.

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

Логика в программировании

В предыдущих разделах мы исследовали формализацию логики и ее роль в решении фундаментальных математических проблем, особенно тех, которые были поставлены Гильбертом. Это исследование заложило основу для математической логики и теории вычислимости, что было вызвано стремлением решить такие проблемы, как непротиворечивость математических систем и проблема разрешимости Гильберта-Аккермана. В этом разделе рассказывается о том, как логика первого порядка применяется к разработке языка компьютерного программирования, включая формальный синтаксис, семантику и определения корректности программ. Эти методы составляют основу современной теории программирования и распространяются на формальные методы, используемые при проектировании компьютерных и программных систем, включая формальные подходы к разработке программ, такие как B-метод Абриала.

Алан Тьюринг написал, возможно, первую работу по формальным методам в контексте проверки программ, в статье 1949 года, озаглавленной “Проверка большой рутины”. Хотя в то время это была малоизвестная статья, оказавшая незначительное влияние, впоследствии она была подробно рассмотрена. Она включает в себя такие важные в настоящее время концепции, как установка состояния в программах (см. далее). Роберт У. Флойд и др. заново открыли идеи для создания программ, схожих с разработками Тьюринга в 1960-х годах. Возможно, наиболее влиятельной была статья Тони Хоара 1969 года о том, что сейчас называется “логикой Хоара”, и мы представляем этот подход ниже.

Универсальность компьютера заключается в его способности к программированию. Основанная на универсальной машине Тьюринга (UTM) и архитектуре фон Неймана, универсальная машина может быть настроена для вычисления любой вычислимой функции.

Язык программирования (PL) - это система обозначений для описания программ. Он определяет операции и порядок их выполнения во время вычисления. Программа содержит инструкции, аналогичные инструкциям машины Тьюринга, которые направляют компьютер на вычисление определенной функции. Компьютер имитирует работу машины Тьюринга шаг за шагом, как UTM, для завершения вычисления.

В общем, программа пишется на формально определенном языке программирования. Она состоит из программных переменных, представляющих данные и инструкции (команды), которые компьютер понимает, возможно, с помощью компилятора или интерпретатора.

Пример (алгоритм Евклида). Ниже приведен пример программы, которая реализует алгоритм Евклида для вычисления наибольшего общего делителя целых чисел \(x\) и \(y\):

ProgramGCD (x, y)
    int x, y;
    begin
        x:=m; y:=n;
        while x ≠ y do if x > y then x:=x−y else y:=y−x
    end

Выполнение программы начинается в исходном состоянии, где переменным \(x\) и \(y\) присваиваются входные значения \(m\) и \(n\) соответственно. Команды x:=x−y и y:=y−x затем выполняются шаг за шагом, следуя потоку управления, определяемому условием цикла while и выбором условия if ... else. На каждом шаге можно считывать, записывать или изменять значения переменных.

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

Формальный синтаксис языка программирования

Мы используем простой язык под названием Mini, чтобы показать, что язык программирования - это формальный язык, определяемый индуктивно, аналогичный формальной логике. Несмотря на небольшой размер, Mini является полным по Тьюрингу и может выражать любую вычислимую по Тьюрингу функцию.

Алфавит Mini включает в себя постоянные натуральные числа, логические значения \(\{ ff, tt\}\) и набор переменных, которые мы обозначаем через \(X\). Используя эти символы, мы индуктивно определяем выражения и команды, подобно термам и формулам в логике первого порядка:

• Арифметические выражения \(e ::= n \;|\; e + e \;|\; e \times e \;|\; e/e\), где \(n \in \mathbb N\)

• Булевы выражения \(B ::= ff \; | \; tt \; | \; e = e \; | \; e < e \; | \; \neg B \; | \; B \land B\)

• Атомарные операторы \(Ac ::= \mathbf{skip} \; | \; x := e \), где \(x\) - переменная

• Операторы \(a ::= Ac \; | \; a; a\; | \; a \triangleleft B \triangleright a \; | \; B * a\)

Команда \(\mathbf{skip}\) представляет собой программу, которая ничего не делает и останавливается. Команда \((a; a )\) представляет собой последовательное выполнение команд, в которой выполняется первая команда, а затем вторая, если первая завершается. Условный выбор (\(a \triangleleft B \triangleright a\)) запускает левую команду, если выполняется логическое условие B. В противном случае выполняется правая команда. Оператор цикла \(( B * a )\) повторяет команду \(a\) до тех пор, пока выполняется логическое условие \(B\). Для компактности мы записываем команды как алгебраические выражения, и эта запись полезна для описания алгебраических свойств программ. Например, \((a_1 \triangleleft B \triangleright a_2 ) =( a_2\triangleleft ( \neg B )\triangleright a_1 )\).

Пример (Программа \(GCD(x,y)\) на языке Mini). Программу из предыдущего примера можно переписать на Mini так:

\(x := m; y := n;\)

\((x \neq y) * (((x := x-y) \triangleleft (x>y) \triangleright (y := y - x))\)

Язык программирования - это формальный язык, синтаксис которого определяется индуктивно, во многом подобно синтаксису системы формальной логики. Мы продемонстрируем, что семантика также определяется аналогичным образом, следуя методам, установленным в математической логике. Все наборы выражений и команд рекурсивны, поэтому проверка их корректности поддается вычислению. Мы приводим определения операциональной семантики, денотационной семантики и аксиоматической семантики (т.е. логики Хоара). Формальная семантика обеспечивает правильную реализацию языка и его правильное использование в программировании – спецификации, проектировании и верификации.

Понятие состояний программ имеет решающее значение во всех семантических теориях. Состояние - это функция \(\sigma \colon X \to \mathbb N\), аналогичная оценке в логике первого порядка. Это означает, что \(\sigma(x)\) - это значение \(x\) (представляющее собой чтение из памяти), а \(σ[ x \leftarrow n]\) представляет собой обновление значения \(x\) в состоянии \(\sigma\) до \(n\) (записывает \(n\) в память, где находится \(x\)). Таким образом, \(\sigma[ х \leftarrow n][x \leftarrow m] = \sigma [ х \leftarrow m]\) и \(\sigma[ х \leftarrow n][ y\leftarrow m] =\sigma [ y \leftarrow m][ х \leftarrow n]\), где \(x\) и \(y\) различны.

Операциональная семантика

Язык программирования реализуется в конкретной компьютерной системе с помощью интерпретатора или компилятора семантики языка. Интерпретатор или компилятор можно рассматривать как определение семантики языка, и он сопоставляет элементы синтаксиса языка с системными “операциями”. Этот тип семантики называется операциональной семантикой.

Цель состоит не в том, чтобы определить семантику языка программирования только для одной конкретной компьютерной системы, а в том, чтобы создать абстрактную стандартную семантику, которая может быть применена в различных системах. Подобно взаимосвязи между машинами Тьюринга и архитектурой фон Неймана, основным методом определения операциональной семантики является использование абстрактной машины для моделирования того, как компьютер выполняет программы. Дальнейшие исследования привели к появлению более абстрактных дедуктивных систем, основанных на синтаксической структуре программы, известных как структурная операциональная семантика. Ниже мы приводим определение структурной операциональной семантики языка Mini, показывая, что она определяется с помощью индуктивных правил.

Правила для вычисления выражений. Выполнение присваивания, условного выбора или инструкции цикла требует вычисления арифметических или логических выражений. Правило представлено в виде отношения вывода для пар выражений и состояний. Мы используем \(\Rightarrow\colon (Exp \times States )\times(Exp \times States )\) для обозначения этого отношения дедукции, чтобы отличить дедукцию от импликации в логической системе. В дальнейшем мы используем \(v\) и \(t\), возможно, с нижними индексами, для обозначения целочисленных и логических значений соответственно, а \(e\) и \(e_1\) - для обозначения выражений, не имеющих значения.

(E1) \(\langle x, \sigma \rangle \Rightarrow \langle \sigma(x), \sigma \rangle\)

(E2) \(\langle op (v_1,v_2), \sigma\rangle \Rightarrow \langle v, \sigma \rangle\), где \(v = op(v_1, v_2)\), например \(5 = 3 + 2\), \(ff = 3 < 2\)

(E3) \(\langle t_1 \land t_2, \sigma\rangle \Rightarrow \langle t, \sigma \rangle\), где \(t = t_1 \land t_2\)

(E4) \(\langle \neg t_1, \sigma \rangle \Rightarrow \langle t, \sigma \rangle\), где \(t = \neg t_1\), например \(\neg tt = ff\), \(\neg ff = tt\)

(E5) \(\dfrac{\langle e_1, \sigma\rangle \Rightarrow \langle v, \sigma \rangle}{\langle e, \sigma \rangle \Rightarrow \langle e[v/e_1], \sigma \rangle}\), где \(e_1\) - это подвыражение выражения \(e\)

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

Например, в состоянии \(\sigma = \{( x, 3),( y, 4)\}\) вычисление \((x + 1)\times y\) может происходить следующим образом: применить (E1) для оценить \(x\) как 3, применить (E5), чтобы переписать \((3 + 1)\times y\), применить (E2) для вычисления \(4\), применить (E5), чтобы переписать \(4 \times y\), применить (E1) для получения значения 4 переменной \(y\) и (E2) для вычисления \(4 \times 4 = 16\).

Пусть \(\to^*\) обозначает рефлексивно-транзитивное замыкание \(\to\). Правило (E5) может применяться недетерминированно, позволяя вычислять подвыражения в разных порядках. Однако отношение замыкания \(\to^*\) удовлетворяет свойству Черча-Россера. То есть для любого состояния \(\sigma\) и выражения \(e\), если существуют выражения \(e_1\) и \(e_2\), такие что \(\langle \sigma, e\rangle \to^* \langle \sigma, e_1\rangle\) и \(\langle \sigma, e\rangle \to^* \langle\sigma, e_2\rangle\), существует выражение \(e'\), такое что \(\langle \sigma, e_1\rangle \to^* \langle\sigma, e'\rangle\) и \(\langle \sigma, e_2\rangle \to^* \langle \sigma, e'\rangle\).

Это позволяет нам определить любое состояние \(\sigma\) как частичную функцию из множества выражений в \(\mathbb N\) таким образом, что для любого выражения \(e\) выполняется \(\sigma (e )= v\), если \(\langle e,\sigma\rangle \to^* v\), а иначе \(\sigma (e )\) не определено. Аналогичное обсуждение можно провести и для логических выражений.

Теперь мы приведем правила вывода структурированной операциональной семантики языка Mini. Сначала мы определим конфигурацию (вспомним поведение UTM) как пару операторов и состояний или только как состояние: \(Con :(Statements \times States)\cup States\). У нас есть следующие схемы правил вывода для пяти видов операторов Mini.

(S1) \(\mathbf {skip}\) ничего не делает, но завершает работу: \(\langle \mathbf{skip}, \sigma\rangle \Rightarrow \sigma\)

(S2) Если выражение в присваивании не является значением, сначала оценить выражение, а затем выполнить присваивание. Поэтапное оценивание выражения выполняется в соответствии с правилами (E1), (E2) и (E5):

\(\dfrac{\langle e, \sigma\rangle \Rightarrow \langle e_1, \sigma \rangle}{\langle x := e, \sigma\rangle \Rightarrow \langle x:= e_1, \sigma\rangle},\)

\(\langle x := v, \sigma \rangle \Rightarrow \sigma[x \leftarrow v]\)

(S3) Последовательная композиция:

\(\dfrac{\langle a_1, \sigma\rangle \Rightarrow \langle a_1', \sigma'\rangle}{\langle a_1; a_2, \sigma\rangle \Rightarrow \langle a_1'; a_2, \sigma'\rangle}\),

\(\dfrac{\langle a_1, \sigma\rangle \Rightarrow \sigma'}{\langle a_1; a_2, \sigma\rangle \Rightarrow \langle a_2, \sigma' \rangle}\)

(S4) Условный выбор сначала оценивает логическое условие:

\(\dfrac{\langle B, \sigma \rangle \Rightarrow \langle B', \sigma \rangle}{\langle a_1 \triangleleft B \triangleright a_2, \sigma \rangle \Rightarrow \langle a_1 \triangleleft B' \triangleright a_2, \sigma}\)

\(\langle a_1 \triangleleft tt \triangleright a_2, \sigma \rangle \Rightarrow \langle a_1, \sigma \rangle\),

\(\langle a_1 \triangleleft ff \triangleright a_2, \sigma \rangle \Rightarrow \langle a_2, \sigma \rangle\)

(S5) На каждой итерации инструкции цикла сначала оценивается условие цикла:

\(\langle B * a, \sigma \rangle \Rightarrow \langle (a; B * a) \triangleleft B \triangleright \mathbf{skip}, \sigma \rangle\)

(S6) Наконец, нам нужно правило рефлексивно-транзитивного замыкания:

\(Con \Rightarrow^* Con,\;\;\; \dfrac{Con \Rightarrow^* Con', \; Con' \Rightarrow ^* Con''}{Con \Rightarrow^* Con''}\)

Пример (Операциональная семантика \(GCD(x,y)\)) Предположим, что в начальном состоянии \(\sigma_0\): \(m = 4\) и \(n = 6\); и пусть \(a\) обозначает оператор цикла, \(a_1\) − тело цикла, \(c_1\) − присваивание \(x:=x- y\), а \(a_2\) - присваивание \(y:=y - x\). Выполнение \(GCD\), начиная с \(\sigma_0\), представляет собой следующую последовательность вывода в соответствии с правилами операциональной семантики.

Выполнение завершается в состоянии \(\sigma_4\), в котором \(x = 2\) и \(y = 2\); и \(2\) - это НОД(4, 6).

Нетрудно показать, что \(\Rightarrow^*\) также обладает свойством Черча-Россера. Так, даже при недетерминированности (E5) выполнение программы остается детерминированным, как говорит следующая теорема.

Теорема. Для любых операторов \(a, a_1, a_2\), выражения \(e\), булева выражения \(B\) и состояния \(\sigma\):

1. \(\langle x := e, \sigma\rangle \Rightarrow^* \sigma[x \leftarrow \sigma(e)]\) тогда и только тогда, когда \(\sigma(e)\) определено,

2. \(\langle B, \sigma \rangle \Rightarrow^* \langle tt, \sigma\rangle\) тогда и только тогда, когда \(\langle a_1 \triangleleft B \triangleright a_2, \sigma \rangle \Rightarrow^* \langle a_1, \sigma \rangle\), и \(\langle B, \sigma\rangle \Rightarrow^* \langle ff, \sigma \rangle \) тогда и только тогда, когда \(\langle a_1 \triangleleft B \triangleright a_2, \sigma \rangle \Rightarrow^* \langle a_2, \sigma \rangle\),

3. \(\langle B, \sigma\rangle \Rightarrow^* \langle tt, \sigma\rangle\) тогда и только тогда, когда \(\langle B * a, \sigma \rangle \Rightarrow^* \langle a; B * a, \sigma \rangle\), и \(\langle B, \sigma\rangle \Rightarrow^* \langle ff, \sigma\rangle\) тогда и только тогда, когда \(\langle B*a, \sigma \rangle \Rightarrow^* \sigma\),

4. Если \(\langle a, \sigma \rangle \Rightarrow^* \sigma\) и \(\langle a, \sigma\rangle \Rightarrow^* \sigma'\), то \(\sigma' = \sigma\)

Пусть \(Com \colon Statements \mapsto (States \mapsto States)\) - функция, такая, что для всякого оператора \(a\) и состояний \(\sigma\), \(\sigma'\) справедливо, что \(Com(a)(\sigma) = \sigma'\) тогда и только тогда, когда \(\langle a, \sigma \rangle \to^* \sigma'\). Мы говорим, что состояние \(\sigma'\) достижимо из состояния \(\sigma\) посредством программы \(a\), если \(Com(a)(\sigma) = \sigma'\). Тогда две программы \(a\) и \(a'\) эквивалентны тогда и только тогда, когда для любого состояния \(\sigma\) выполняется \(Com(a)(\sigma) = Com(a')(\sigma)\).

Денотационная семантика

Операционная семантика предоставляет конкретное пошаговое описание выполнения программы, что полезно для понимания синтаксического анализа и обеспечения корректности языковой реализации. Однако она тесно связана с деталями выполнения, что затрудняет рассуждение о свойствах программы или абстрактное сравнение различных реализаций. Именно здесь денотационная семантика становится существенной: она предлагает машинно-независимый математический взгляд на значение программы, позволяющий более просто рассуждать о поведении программы, сравнивать реализации и устанавливать алгебраические законы для программ. В этом подразделе дается определение денотационной семантики Mini, основанное на подходе, аналогичном интерпретации языка первого порядка.

См. оригинал

Логика Хоара

Связь между семантическими теориями

Заключение

В этом обзоре прослеживается путь от логики к программированию, основное внимание уделяется важнейшим этапам формализации логики, моделей, теорий вычислений и языков программирования. Цель состоит в том, чтобы изучить, как эти этапы способствуют написанию программ, выявляя проблемы, проводя исследования и разрабатывая решения. Исследование демонстрирует, как исследования по программе Гильберта повлияли на развитие математической логики, и большинство основных результатов были достигнуты благодаря изучению эффективно вычислимых функций в теории рекурсивных функций, λ-исчислении и машинах Тьюринга. Именно так математическая логика становится естественной основой информатики и системной инженерии.

Двумя важными эрудитами начала 20-го века, обладавшими такими навыками, как математика, логика и компьютерные науки, были Алан Тьюринг, создатель машин Тьюринга, и Джон фон Нейман, создатель ассоциированной архитектуры фон Неймана для компьютеров. В честь этих двух великих ученых установлены бюсты в кампусе Юго-Западного университета. На момент написания статьи они были единственными учеными-компьютерщиками, получившими такое признание. Из нашего обсуждения формальных систем мы заключаем, что естественным языкам присущи недостатки, связанные со строгой и систематической формулировкой и обработкой вычислений и рассуждений. Следовательно, для описания и обработки вычислений, рассуждений и мышления требуются различные уровни формализации. Системы формальной логики демонстрируют мощь конечных дедуктивных методов в анализе, решении задач принятия решений и обращении к сложным структурам и процессам.

Однако язык системы формальной логики фиксирован, и все теоремы, которые она доказывает, выводятся из ее аксиом. В этом смысле формальная логика является замкнутой теорией, что означает, что рассуждения в рамках таких систем не могут генерировать новые концепции для создания новых теорий. Более того, теоремы Геделя о неполноте и теоремы Черча и Тьюринга о невычислимых задачах показывают, что нетривиальные формальные системы не являются ни полными, ни вычислимыми. Эти результаты раскрывают пределы возможностей формальных систем и современных компьютерных технологий, показывая, что человеческая интуиция, которая часто не поддается формализации, иногда необходима для принятия решений. Это означает, что человеческие инновации безграничны.

Рассматривая универсальную машину Тьюринга (UTM) как логическую систему, языки программирования описывают вычислительные процессы на основе базовых операций с конечным числом комбинаций. Это понимание также помогает нам в изучении масштабов и возможностей современных систем искусственного интеллекта. Учитывая недавний ажиотаж вокруг ИИ, особенно больших языковых моделей (LLM), важно учитывать фундаментальные ограничения ИИ, такие как:

• Может ли ИИ рассуждать и планировать так же, как это делают люди?

• Может ли ИИ быть объяснимым и что значит для ИИ быть объяснимым?

• Может ли ИИ автоматически написать все программы для всех вычислимых задач (по Тьюрингу)?

• Какие типы программ могут или не могут быть автоматически написаны ИИ?

• Может ли система ИИ определить, когда и почему ей нужно сгенерировать программу?

Ответы на эти вопросы имеют решающее значение для создания надежного ИИ.