Часовой пояс: UTC + 3 часа [ Летнее время ]

Математическая логика и языки программирования
Онлайн-сервисы Нахождение НОД и НОК Разложение числа на простые множители Сравнения по модулю Операции над множествами Операции над векторами Разложение вектора по базису. Доказательство, что векторы образуют базис Чертёж треугольника по координатам вершин Решение треугольника Решение Пирамиды Построение Пирамиды по координатам вершин Чертёж многоугольника по координатам вершин Решение систем методом Крамера и Матричным Онлайн построение графика кривой 2-го порядка Определение вида кривой или поверхности 2-го порядка по инвариантам МНК и регрессионный анализ Онлайн + графики Онлайн число, сумма и дата прописью Алгоритмы JavaScript Алгоритмы поиска Алгоритмы сортировки Уникальные элементы массива Объединение, пересечение и разность массивов НОД и НОК Операции над матрицами Дата прописью Введение в анализ Функции: понятие, определение, графики Непрерывность функции Исследование функции и построение графика Теория множеств Множества: понятие, определение, примеры Точечные множества Замкнутые и открытые множества Мера множества Группы, кольца, поля в математике Поле комплексных чисел Кольцо многочленов Основная теорема алгебры и ее следствия Математическая логика Алгебра высказываний Аксиоматика и логические рассуждения Методы доказательств теорем Алгебра высказываний и операции над ними Формулы алгебры высказываний Тавтологии алгебры высказываний Логическая равносильность формул Нормальные формы для формул высказываний Логическое следование формул Приложение алгебры высказываний для теорем Дедуктивные и индуктивные умозаключения Решение логических задач Принцип полной дизъюнкции Булевы функции Множества, отношения и функции в логике Булевы функции от одного и двух аргументов Булевы функции от n аргументов Системы булевых функций Применение булевых функций к релейно-контактным схемам Релейно-контактные схемы в ЭВМ Практическое применение булевых функций Теория формального Формализованное исчисление высказываний Полнота и другие свойства формализованного исчисления высказываний Независимость системы аксиом формализованного исчисления высказываний Логика предикатов Логика предикатов Логические операции над предикатами Кванторные операции над предикатами Формулы логики предикатов Тавтологии логики предикатов Преобразования формул и следование их предикатов Проблемы разрешения для общезначимости и выполнимости формул Применение логики предикатов в математике Строение математических теорем Аристотелева силлогистика и методы рассуждений Принцип полной дизъюнкции в предикатной форме Метод полной математической индукции Необходимые и достаточные условия Логика предикатов и алгебра множеств Формализованное исчисление предикатов Неформальные и формаль- ные аксиоматические теории Неформальные аксиоматические теории Свойства аксиоматических теорий Формальные аксиоматические теории Формализация теории аристотелевых силлогизмов Свойства формализованного исчисления предикатов Формальные теории первого порядка Формализация математической теории Теория алгоритмов Интуитивное представление об алгоритмах Машины Тьюринга и тезис Рекурсивные функции Нормальные алгоритмы Маркова Разрешимость и перечислимость множеств Неразрешимые алгоритмические проблемы Теорема Гёделя о неполноте формальной арифметики Математическая логика и компьютеры Математическая логика и языки программирования Применение компьютеров для доказательства теорем математической логики Математическая логика и логическое программирование Математическая логика и информатика Математическая логика и искусственный интеллект Дискретная математика Множества и отношения Теория множеств: понятия и определения Операции над множествами Кортеж и декартово произведение множеств Соответствия и бинарные отношения на множествах Операции над соответствиями на множествах Семейства множеств Специальные свойства бинарных отношений Отношения эквивалентности на множестве Упорядоченные множества Теорема о неподвижной точке Мощность множества Парадокс Рассела Метод характеристических функций Группы и кольца Алгебраические структуры и операции Группоиды, полугруппы, группы Кольца, тела, поля Области целостности в теории колец Модули и линейные пространства Подгруппы и подкольца Теорема Лагранжа о порядке конечной группы Гомоморфизмы групп и нормальные делители Гомоморфизмы и изоморфизмы колец Алгебра кватернионов Полукольца и булевы алгебры Полукольца: определение, аксиомы, примеры Замкнутые полукольца Полукольца и системы линейных уравнений Булевы алгебры и полукольца Решетки и полурешетки Алгебраические системы Алгебраические системы: модели и алгебры Подсистемы алгебраических систем Конгруэнции и фактор-системы Гомоморфизмы алгебраических систем Прямые произведения алгебраических систем Конечные булевы алгебры Многосортные алгебры Теория графов Теория графов: основные понятия и определения Способы представления графов Неориентированные и ориентированные деревья Остовное дерево и алгоритм Краскала Методы систематического обхода вершин графа Алгоритмы поиска в глубину и ширину в графах Задача о путях во взвешенных ориентированных графах Изоморфизм, гомоморфизм и автоморфизм графов Топологическая сортировка вершин графа Элементы цикломатики в теории графов Булева алгебра и функции Булевы функции и булев куб Таблицы булевых функций и булев оператор Равенство булевых функций. Фиктивные переменные Формулы и суперпозиции булевых функций Дизъюнктивные и конъюнктивные нормальные формы Построение минимальных ДНФ Теорема Поста и классы Критерий Поста Схемы из функциональных элементов Конечные автоматы и регулярные языки Конечные автоматы и регулярные языки Алфавит, слово, язык в программировании Порождающие грамматики (грамматики Хомского) Классификация грамматик и языков Регулярные языки и регулярные выражения Конечные автоматы Допустимость языка конечным автоматом Теорема Клини Детерминизация конечных автоматов Минимизация конечных автоматов Лемма о разрастании для регулярных языков Обоснование алгоритма детерминизации автоматов Конечные автоматы с выходом Морфизмы и конечные подстановки Машины Тьюринга Контекстно-свободные языки Контекстно-свободные языки и грамматики Приведенная форма КС-грамматики Лемма о разрастании для КС-языков Магазинные автоматы (автомат с магазинной памятью) Алгоритм построения МП-автомата по КС-грамматике Алгоритм построения КС-грамматики по МП-автомату Алгебраические свойства КС-языков Основное свойство суперпозиции КС-языков Пересечение контекстно-свободных языков Методы синтаксического анализа КС-языков Восходящий синтаксический анализ и LR(k)-грамматики Семантика формальных языков Принцип индукции по неподвижной точке Графовое представление МП-автоматов Интегральное исчисление Неопределённый и определённый Неопределенный и определенный интегралы Свойства интегралов Интегрирование по частям Интегрирование методом замены переменной Интегрирование различных рациональных функций Интегрирование различных иррациональных функций Интегрирование различных тригонометрических функций Определенный интеграл и его основные свойства Необходимое и достаточное условие интегрируемости Теоремы существования первообразной Свойства определенных интегралов Несобственные интегралы Интегральное определение логарифмической функции Приложения интегралов Вычисление площадей плоских фигур Площади фигур в различных координатах Вычисление объемов тел с помощью интегралов Объём тела вращения Вычисление длин дуг кривых Формулы длины дуги регулярной кривой Кривизна плоской кривой Площадь поверхности вращения тела Интегралы в физике Статические моменты и координаты центра тяжести Теоремы Гульдина–Паппа Вычисление моментов инерции Другие приложения интегралов в физике Основные интегралы Интеграл Ньютона-Лейбница Интеграл Римана Интеграл Лебега Вариационное исчисление Примеры вариационных задач Дифференциальное уравнение Эйлера Функционалы, зависящие от нескольких функций Задача о минимуме кратного интеграла Финансовый анализ Анализ эффективности Критерии и показатели эффективности предприятия Методы анализа эффективности деятельности Факторный анализ прибыли от операционной деятельности Анализ безубыточности предприятия Операционный рычаг и эффект финансового рычага Анализ и оценка состава, структуры и динамики доходов и расходов Анализ рентабельности и резервов устойчивого роста капитала Анализ распределения прибыли предприятия Анализ и оценка чувствительности показателей эффективности Анализ устойчивости Финансовая устойчивость и долгосрочная платежеспособность Характеристика типов финансовой устойчивости Рыночная активность Финансовый анализ рыночной активности Методика анализа рыночной активности Анализ и оценка дивидендного дохода на одну акцию Инвестиционная деятельность Инвестиции: экономическая сущность и классификация Государственное регулирование инвестиционной деятельности Источники финансовых ресурсов на капитальные вложения Инвестиции в основные фонды Оценка состояния основных фондов Амортизация основных фондов Капитальное строительство в инвестиционном процессе Планирование инвестиций в форме капитальных вложений Экономическая эффективность инвестиций Финансирование капитальных вложений Кредитование капитальных вложений Кредитоспособность Финансирование и кредитование затрат Финансирование и кредитование инвестиционной деятельности потребительской кооперации Финансирование и кредитование капитальных вложений потребительской кооперации Инвестиционное строительное проектирование Анализ инвестиций Инвестиции и инвестиционная деятельность предприятия Задачи финансового анализа инвестиций предприятия Учет фактора времени в инвестиционной деятельности Аннуитет и финансовая рента в инвестициях Учет фактора инфляции при инвестировании Оценка фактора риска инвестиционного проекта Методы оценки эффективности инвестиций Показатели эффективности инвестиционного проекта Стоимость компании Концепция построения международных стандартов финансовой отчетности (МСФО) Экономическое содержание международных стандартов финансовой отчётности Цели и принципы оценки стоимости акций и активов компании Оценка акций и активов предприятия по справедливой стоимости Методы оценки справедливой стоимости акций предприятия Затратный подход к оценки стоимости компаний и акций Сравнительный подход к оценки стоимости предприятий и акций Доходный подход к оценке стоимости компании и акций Выбор ставки дисконтирования при инвестировании в акции Метод капитализации прибыли Сравнение подходов к оценке стоимости компаний и пакетов акций Форвардные контракты Форвардный контракт и цена Форвардная цена акции на бирже Цена форвардного контракта инвестора Форвардная цена акции с учетом величины дивиденда Форвардная цена акции с учетом ставки дивиденда Форвардная цена валюты на рынке форекс Форвардный валютный курс и инфляция на рынке Форвардная цена товара и спотовый рынок Форвардная цена при различии ставок по кредитам и депозитам Синтетический форвардный контракт на акции и валюту Теория вероятностей Основные понятия теории вероятностей Зависимые и независимые случайные события Повторные независимые испытания Формула Бернулли Одномерные случайные величины Многомерные случайные величины Функции случайных величин Законы распределения целочисленных случайных величин Законы распределения непрерывных случайных величин Предельные теоремы теории вероятностей Закон больших чисел и предельные теоремы Вероятностные закономерности Математическая статистика Элементы математической статистики Выборочный метод Оценки параметров генеральной совокупности Статистические гипотезы Критерии согласия Теоретические и эмпирические частоты Теория очередей (СМО) Определение системы массового обслуживания Уравнения Колмогорова Предельные вероятности состояний Определение СМО с отказами Определение СМО с ожиданием (очередью) Аналитическая геометрия Векторная алгебра Метрические понятия и аксиомы геометрии Равенство и подобие геометрических фигур Бинарные отношения Вектор, его направление и длина Линейные операции над векторами Линейная зависимость и независимость векторов Отношение коллинеарных векторов Проекции векторов на прямую и на плоскость Угол между векторами Ортогональные проекции векторов Координата вектора на прямой и базис Координаты вектора на плоскости и базис Координаты вектора в пространстве и базис Операции над векторами в координатной форме Ортогональный и ортонормированный базисы Cкалярное произведение векторов и его свойства Выражение скалярного произведения через координаты векторов Векторное произведение векторов и его свойства Смешанное произведение векторов и его свойства Ориентированные площади и объемы Двойное векторное произведение и его свойства Применение векторов в задачах на аффинные свойства фигур Применение произведений векторов при решении геометрических задач Применение векторной алгебры в механике Системы координат Прямоугольные координаты Преобразования прямоугольных координат Полярная система координат Цилиндрическая система координат Сферические координаты Аффинные координаты Аффинные преобразования координат Аффинные преобразования плоскости Примеры аффинных преобразований плоскости Аффинные преобразования пространства Многомерное координатное пространство Линейные и аффинные подпространства Скалярное произведение n-мерных векторов Преобразования систем координат Геометрия на плоскости Алгебраические линии на плоскости Общие уравнения геометрических мест точек Алгебраические уравнения линий на плоскости Уравнения прямой, проходящей через точку перпендикулярно вектору Уравнения прямой, проходящей через точку коллинеарно вектору Уравнения прямой, проходящей через две точки Уравнения прямой с угловым коэффициентом Взаимное расположение прямых Примеры задач с прямыми на плоскости Системы неравенств с двумя неизвестными Системы линейных уравнений с двумя неизвестными Линии 2-го порядка Канонические уравнения линий второго порядка Порядок приведения уравнения линии к каноническому виду Эллипс Гипербола Парабола Квадратичные неравенства с двумя неизвестными Применение линий 1-го и 2-го порядков в задачах на экстремум функций Инварианты линий Классификация линий 2-го порядка по инвариантам Приведение уравнения линии к каноническому виду по инвариантам Геометрия в пространстве Способы задания ГМТ в пространстве Алгебраические уравнения поверхностей Уравнения плоскости, проходящей через точку перпендикулярно вектору Уравнения плоскости, компланарной двум неколлинеарным векторам Уравнения плоскости, проходящей через три точки Взаимное расположение плоскостей Типовые задачи с плоскостями Уравнения прямых в пространстве Взаимное расположение прямых в пространстве Типовые задачи с прямыми в пространстве Поверхности 2-го порядка Канонические уравнения поверхностей Порядок приведения уравнения поверхности к каноническому виду Поверхности второго порядка Эллипсоиды Гиперболоиды Конусы Параболоиды Применение поверхностей 1-го и 2-го порядков в задачах на экстремум функций Инварианты поверхностей Классификация поверхностей 2-го порядка по инвариантам Квадратичные неравенства с тремя неизвестными Приведение уравнения поверхности к канониче-скому виду по инвариантам Линейная алгебра Матрицы и операции Линейные операции над матрицами Умножение матриц Возведение матриц в степень Многочлены от матриц Транспонирование и сопряжение матриц Блочные матрицы Произведение и сумма матриц Кронекера Метод Гаусса приведения матрицы к ступенчатому виду Элементарные преобразования матриц Определители Определители матриц и их основные свойства Формула полного разложения определителя Формула Лапласа полного разложения определителя Определитель произведения матриц Методы вычисления определителей Ранг матрицы Линейная зависимость и линейная независимость строк (столбцов) матрицы Ранг матрицы и базисный минор матрицы Методы вычисления ранга матрицы Ранг системы столбцов (строк) Обратная матрица Обратные матрицы и их свойства Ортогональные и унитарные матрицы Способы нахождения обратной матрицы Матричные уравнения Односторонние обратные матрицы Скелетное разложение матрицы Полуобратная матрица Псевдообратная матрица Системы уравнений Системы линейных алгебраических уравнений Метод Гаусса решения систем линейных уравнений Структура общего решения системы уравнений Решение систем с помощью полуобратных матриц Псевдорешения системы линейных уравнений Функциональные матрицы Функциональные матрицы скалярного аргумента Производные матриц по векторному аргументу Линейные и квадратичные формы и их преобразования Приведение форм к каноническому виду Закон инерции вещественных квадратичных форм Знакоопределенность форм вещественных квадратичных Формы и исследование функций на экстремум Многочленные матрицы Многочленные матрицы (лямбда-матрицы) Операции над лямбда-матрицами Простые преобразования многочленных матриц Инвариантные множители многочленной матрицы Функции от матриц Собственные векторы и значения матрицы Подобие числовых матриц Характеристический многочлен матрицы Минимальный многочлен матрицы Теорема Гамильтона-Кэли Жорданова форма матрицы Приведение матрицы к жордановой форме Многочлены от матриц Применение многочленов от матриц Функции от матриц Линейные пространства Линейные пространства: определение и примеры Линейная зависимость и независимость n-мерных векторов Размерность и базис линейного пространства Преобразования координат в линейном пространстве Изоморфизм линейных пространств Подпространства Подпространства линейного пространства Пересечение и сумма подпространств Способы описания подпространств Нахождение дополнения и суммы подпространств Нахождение пересечения подпространств Линейные отображения Линейные многообразия Линейные отображения Матрица линейного отображения Ядро и образ линейного отображения Линейные операторы Линейные операторы (преобразования) Инвариантные подпространства Собственные векторы и значения оператора Свойства собственных векторов операторов Канонический вид линейного оператора Методика приведения линейного преобразования к каноническому виду Евклидовы пространства Евклидовы пространства Ортогональные векторы евклидова пространства Ортогональный базис евклидова пространства Ортонормированный базис евклидова пространства Ортогональные дополнения в евклидовом пространстве Задача о перпендикуляре Матрица и определитель Грама и его свойства Линейные преобразования евклидовых пространств Канонический вид ортогонального оператора евклидова пространства Сопряженные операторы евклидова пространства Самосопряженные операторы евклидова пространства Приведение квадратичной формы к главным осям Унитарные пространства и их линейные преобразования Комплексный анализ Комплексные числа Комплексные числа в алгебраической форме Комплексные числа в тригонометрической и показательной формах Множества на комплексной плоскости Последовательности и ряды комплексных чисел Комплексные функции Функции комплексного переменного. Предел, непрерывность и производная Элементарные функции комплексного переменного Дифференцирование функций комплексного переменного Аналитические функции и их свойства Конформные отображения и их свойства Интегрирование функций комплексного переменного Функциональные ряды в комплексной области Функциональные ряды и последовательности Степенные ряды и их свойства Разложение функций в степенные ряды Нули аналитических функций Ряд Лорана и разложение функций по целым степеням Особые точки, Вычеты Изолированные особые точки функций и полюсы Вычеты и их применение Вычисление интегралов с помощью вычетов Вычеты и расположение нулей многочлена Операционное исчисление Преобразование Лапласа и его свойства Решение ДУ операционным методом Анализ выходных процессов линейных стационарных систем Z-преобразование и его свойства Дифференциальные уравнения ДУ первого порядка Основные понятия и определения ДУ Метод изоклин для ДУ 1-го порядка Метод последовательных приближений ДУ с разделяющимися переменными Однородные ДУ Линейные ДУ 1-го порядка Дифференциальное уравнение Бернулли ДУ в полных дифференциалах Интегрирующий множитель ДУ, не разрешенные относительно производной Дифференциальное уравнение Риккати Составление ДУ семейств линий Задачи на траектории Особые решения ДУ ДУ высших порядков Понятия и определения ДУ высших порядков ДУ, допускающие понижение порядка Линейная независимость функций Определители Вронского и Грама Однородные и неоднородные дифференциальные уравнения Задача Коши и Уравнение Эйлера Линейные ДУ с переменными коэффициентами Метод Лагранжа решения ДУ Краевые задачи для ДУ высших порядков Разложение решения ДУ в степенной ряд Разложение решения ДУ в обобщенный степенной ряд Нахождение периодических решений ДУ Асимптотическое интегрирование ДУ Системы ДУ Системы ДУ: понятия и определения Сведение системы ДУ к одному уравнению Нахождение интегрируемых комбинаций Интегрирование однородных линейных систем ДУ Методы интегрирования неоднородных систем ДУ Преобразование Лапласа и решение ДУ и систем Теория устойчивости Устойчивость решений ДУ по Ляпунову Простейшие типы точек покоя Метод функций Ляпунова Устойчивость решений ДУ по первому приближению Критерии устойчивости Рауса–Гурвица и Михайлова ДУ с малым параметром при производной Численные методы Методы алгебры Численные методы линейной алгебры Численные методы решения СЛАУ Итерационный метод Шульца обратной матрицы Методы решения задач о собственных значениях и векторах матрицы Методы решения нелинейных уравнений Методы решения систем нелинейных уравнений Методы теории приближений Методы приближения сеточных функций Методы функциональной интерполяции Методы интегрально-дифференциальной интерполяции Методы интегрального сглаживания Методы интерполяции и сглаживания сплайнами Методы численного дифференцирования и интегрирования Методы численного дифференцирования Методы численного интегрирования Методы решения обыкновенных ДУ Численные методы решения задачи Коши Разностные схемы для решения задачи Коши Составные схемы для решения задачи Коши Экстраполяционные методы решения задачи Коши Непрерывно-дискретные методы решения задачи Коши Численные методы решения краевых задач Методы решения ДУ в частных производных Численные методы решения уравнений математической физики с двумя переменными Принципы построения разностных схем для уравнений в частных производных Разностные схемы решения уравнений в частных производных 1-го порядка Разностные схемы решения уравнений в частных производных 2-го порядка Численные методы решения уравнений в частных производных Численные методы решения уравнений математической физики с тремя переменными	Математическая логика и языки программирования Образно выражаясь, можно сказать, что компьютер состоит из материальной части и математического (программного) обеспечения, или, используя профессиональную лексику, из "железа" и "обуви". И к тому, и к другому имеет самое непосредственное отношение математическая логика, ни первое, ни второе без математической логики обойтись не могут. Ранее здесь и здесь было рассмотрено применение математической логики к релейно-контактным (переключательным) схемам, являющимся неотъемлемой составной частью современного компьютера. Часть настоящей главы также посвящена вопросам взаимодействия математической логики и компьютеров. Так, в этой статье рассказывается о применении математической логики к языкам программирования и к самому процессу программирования и получающимся в результате этого программам. В статье дается характеристика обратного процесса — применению компьютеров для поиска доказательств теорем математической логики и других математических дисциплин. Значительное внимание уделено методу резолюций для доказательства теорем в исчислениях высказываний и предикатов. В статье кратко описывается язык ПРОЛОГ — принципиально новый язык программирования, выросший непосредственно из математической логики (логики- предикатов) и призванный стать языком компьютеров пятого поколения. В свою очередь, информатика как наука начала оформляться вместе с созданием и бурным развитием вычислительной техники. Ее формирование и определение ее предмета продолжаются по настоящее время. Информатика — наука о хранении, обработке и передаче информации с помощью компьютеров. Она включает в себя крупные разделы, изучающие алгоритмические, программные и технические средства хранения, обработки и передачи информации. Математическая логика оказалась единственной математической наукой, методы которой стали мощнейшими инструментами познания во всех разделах информатики. Поэтому сколько-нибудь серьезное изучение информатики немыслимо без освоения основ математической логики. Вторая часть настоящего раздела посвящена тем вопросам математической логики, которые находят наиболее яркое применение в информатике, а также краткому показу того, как математическая логика работает в некоторых разделах информатики. Здесь будет рассказано о применении математической логики при исследованиях, посвященных базам данных, базам знаний и системам искусственного интеллекта. Чтобы компьютер работал, он должен быть оснащен программным обеспечением, т.е. комплексом программ, ориентирующих компьютер на решение задач того или иного класса. (Слово "программа" имеет греческое происхождение и означает "объявление", "распоряжение".) Уже само понятие компьютерной программы, предусматривающее четкое алгоритмическое предписание компьютеру о порядке и характере действий, предусматривает проникновение в программу, а также в процесс ее составления (в программирование) теории алгоритмов. Но при более пристальном рассмотрении процесс проникновения логики в программы и программирование оказывается значительно более глубоким и органичным. Не только один ее раздел — теория алгоритмов — работает здесь, но исключительно действенным оказывается само существо математической логики — ее язык, ее аксиоматические теории, выводы и теоремы в них, свойства этих теорий. В данном параграфе дается краткий обзор основных направлений, по которым математическая логика внедряется в программирование, из которых программирование возникло и без которых существовать не может. Теория алгоритмов и математическая логика — фундаментальная основа программирования. В 30-е гг. XIX в. английский математик Чарлз Бэббедж высказал впервые идею вычислительной машины. И только сто лет спустя логики разработали четыре математически эквивалентные модели понятия алгоритма (мы достаточно подробно рассмотрели в предыдущей главе три из них). Именно в теории алгоритмов были предугаданы основные концепции, которые легли в основу принципов построения и функционирования вычислительной машины с программным управлением и принципов создания языков программирования. Идею такой вычислительной машины впервые смогли реализовать болгарский ученый С. Атанасов в 1940 г. и немецкий ученый К. Цузе в 1942 г. Четыре главные модели алгоритма породили разные направления в программировании. Первая модель — это абстрактная вычислительная машина (А. Тьюринг, Р. Пост). Она явилась абстрактным прообразом реальных вычислительных машин. До сих пор все вычислительные машины в некотором смысле базируются на идее Тьюринга: их память физически состоит из битов, каждый из которых содержит либо 0, либо 1. Программное управление унаследовало от этих абстрактных машин и программу, помещенную в "постоянную память" (идея поместить программу ЭВМ в основную память, чтобы иметь возможность изменять ее в ходе вычислений, принадлежит Джону фон Нейману), а структура команды современной ЭВМ в значительной степени напоминает структуру команды машины Тьюринга. В рамках теории машин Тьюринга откристаллизовались важнейшие для компьютерных приложений логики понятия: вычислимая функция, разрешимая задача, неразрешимая (алгоритмически) задача. Собрано большое количество определений абстрактных вычислительных машин и показано, как каждое из них можно свести к другому подходящей кодировкой входов и выходов. Другая модель — это рекурсивные функции, идея которых восходит к гильбертовскому аксиоматическому подходу. От них унаследовало свои основные конструкции современное структурное программирование. Третий способ описания алгоритмов — нормальные алгоритмы А. А. Маркова. Они послужили основой языка Рефал и многих других языков обработки символьной информации. Четвертое направление в теории алгоритмов — так называемое λ-исчисление — базируется на идеях советского логика Р.Шейнфинкеля и американского логика X. Б. Карри. Оказалось, что для определения всех вычислимых функций достаточно операций так называемой λ-абстракции и суперпозиции. Идеи λ-исчисления активно развиваются в языке Лисп, функциональном программировании и во многих других перспективных направлениях современного программирования. Математическая логика стала бурно развиваться в начале XX в. на почве казалось бы исключительно далекой от приложений проблемы обоснования математики. Но именно эти исследования положили начало строгому определению алгоритмических языков, показали их колоссальные возможности и принципиальные ограничения, развили технику формализации. Поэтому, когда в программировании было осознано, что всякая программа есть формализация, то возникшие здесь математические проблемы упали на почву, тщательно подготовленную математической логикой. Описание компьютерных программ с помощью математической логики Первые попытки применить в программировании развитые логические исчисления и методы формализации предпринял американский логик X. Б. Карри. В 1952 г. он сделал доклад "Логика программных композиций", идеи которого опередили свое время по крайней мере на четверть века. Карри рассмотрел задачу программирования как задачу составления более крупных программ из готовых кусков. Были введены две базисные системы конструкций: первая — последовательное исполнение, разветвление и цикл, вторая — последовательное исполнение и условный переход. Он охарактеризовал логические средства, какие можно использовать для композиции программ из подпрограмм в каждом из этих случаев. Как известно, компьютер является своего рода "идеальным бюрократом": он не воспримет программу, написанную на не до конца формализованном языке, и приступит к работе лишь после того, как все выражено в полном соответствии с детальными инструкциями. Поэтому в 1960-е гг. на первый план вышли задачи точного определения формальных языков достаточно сложной структуры. Математическая логика, подпитываемая идеями программирования, успешно с ними справилась, разработав описание синтаксиса сложных и богатых по выразительным средствам формальных языков. В середине 1960-х гг. практически одновременно появился ряд пионерских работ в области описания условий, которым удовлетворяет программа. Советский математик В. М. Глушков в 1965 г. ввел понятие алгоритмической алгебры, послужившее прообразом алгоритмических логик. Ф. Энгелер в 1967 г. предложил использовать языки с бесконечно длинными формулами, чтобы выразить бесконечное множество возможностей, возникающих при разных исполнениях программы. Но наибольшую популярность приобрели языки алгоритмических логик. Эти языки были изобретены практически одновременно американскими логиками Р.У.Флойдом (1967), С.А.Р.Хоаром (1969) и учеными польской логической школы, например А. Сальвицким и др. (1970). Алгоритмическая логика (или динамическая логика, или программная логика, или логика Хоара) — раздел теоретического программирования, в рамках которого исследуются аксиоматические системы, представляющие средства для задания синтаксиса и семантики языков программирования, а также для синтеза компьютерных программ и их верификации (проверки правильности работы). Языки алгоритмических логик основываются на логике предикатов 1-го порядка и включают в себя высказывания вида $\{A\}S\{B\}$ , читающиеся следующим образом: "Если до исполнения оператора $S$ было выполнено $A$ , то после него будет выполнено $B$ ". Здесь $A$ называется предусловием, $B$ — постусловием, либо обещанием $S$ . На этом языке даются логические описания операторов присвоения и условного перехода, ветвления, цикла. Наряду с динамической логикой 1-го порядка рассматривается пропозициональная динамическая логика и ее обобщение — так называемая логика процессов, в которой выразимы некоторые свойства программы, зависящие от процесса ее выполнения. Различные динамические логики получаются при варьировании средств языков программирования, используемых в программах. Эти средства содержат массивы и другие структуры данных, рекурсивные процедуры, циклические конструкции, а также средства задания недетерминированных программ. Динамическая логика является одним из типов логических систем, используемых для логического синтеза компьютерных программ. Логический синтез — один из способов перехода от спецификации программы к реализующему алгоритму, имеющий форму точного рассуждения в некоторой логической системе. В динамической логике спецификация задачи задается в виде двух формул исчисления предикатов — предусловия и постусловия, а аксиомами логической системы являются схемы предусловий и постусловий, связываемых теми или иными конструкциями языка программирования. Синтезируемая программа получается в форме выводимого в динамической логике утверждения, гласящего, что если аргументы задачи удовлетворяют заданному предусловию, то результат выполнения синтезированной программы удовлетворяет заданному постусловию. В теоретических работах по динамическим логикам исследуются вопросы непротиворечивости и полноты аксиоматических систем, алгоритмические сложностные свойства множеств истинных формул, сравнения выразительной мощности языков динамической логики. Принципиально иной способ определения семантики программ, пригодный, скорее для описания всего алгоритмического языка, а не конкретных программ, предложил в 1970 г. американский логик Д. Скотт. Он построил математическую модель λ-исчисления и показал, как переводить функциональное описание языка структурного программирования в λ-исчисление и как определить математическую модель алгоритмического языка через модель λ-исчисления. Эта так называемая денотационная семантика алгоритмических языков, работы по которой насчитываются уже тысячами, стала практическим инструментом построения надежных трансляторов со сложных алгоритмических языков. Так еще одна абстрактная область математической логики нашла прямые практические приложения. Описание программирования и анализ его концепций с помощью математической логики Программирование — это процесс составления программы, плана действий. Было замечено, что классическая логика плохо подходит для описания этого процесса хотя бы потому, что она плохо подходит вообще для описания всякого процесса в математике. Еще в начале XX в. стало ясно, что в математике Давно разошлись понятия "существовать" и "быть построенным", с античных времен трактовавшиеся как синонимы. Были выявлены так называемые математические объекты-"привидения" (множества, Функции, числа), существование которых доказано, но построить которые нельзя. Причиной их появления явился эффект сочетания классической логики с теоремой Гёделя о неполноте формальной арифметики. Один из фундаментальных законов классической логики — закон исключенного третьего $P\lor\lnot P$ в некоторой свободной трактовке фактически означает, что мы знаем все. Этот постулат конечно же никак нельзя назвать реалистическим: мы знаем чрезвычайно мало, и чем больше узнаем, тем лучше это понимаем. Голландский математик Л. Э. Я. Брауэр определил логические корни "привидений" еще до открытия теоремы Гёделя, в 1908 г., и начал построение так называемой интуиционистской математики, не принимающей закон $P\lor\lnot P$ как универсальный. В 1930–1932 гг. другой голландец А. Гейтинг строго сформулировал логику, которой пользовались в интуиционистской математике, — интуиционистскую логику. Ее математическая интерпретация, данная советским математиком А. Н. Колмогоровым в то же время, сохранила свое значение до сих пор. А. Н. Колмогоров рассмотрел логику как исчисление задач. Каждая формула алгебры высказываний рассматривается не просто как формула, но как требование решить задачу, т.е. построить объект, удовлетворяющий некоторым условиям. Это так называемая конструктивная интерпретация логики высказываний. Логические связки понимаются как средства построения формулировок более сложных задач из более простых, аксиомы — как задачи, решения которых даны, правила вывода — как способы преобразования решений одних задач в решения других. Отметим, что решение задачи — это не только сам искомый объект, но и доказательство того, что он удовлетворяет предъявляемым требованиям. Например, формула $A\land B$ понимается в колмогоровской интерпретации как задача, состоящая в том, чтобы построить и решение задачи $A$ , и решение задачи $B$ , правило вывода $A,B\setminus A\land B$ — как преобразование, строящее из объекта $a$ , решающего задачу $A$ , и объекта $b$ , решающего задачу $B$ , пару $(a,b)$ , решающую задачу $A\land B$ . Объект $a$ , решающий задачу, сопоставленную формуле $A$ , называется реализацией $A$ . Этот факт обозначается $aRA$ . Центральным моментом конструктивного понимания логических формул является интерпретация импликации. Конструктивная импликация $A\Rightarrow B$ понимается как требование построить эффективное преобразование $f$ , применимое ко всем реализациям формулы $A$ и переводящее их в реализации формулы $B$ . Нечеткая колмогоровская формулировка логики как исчисления задач породила многочисленные различные конкретизации, дав целую систему точных математических определений. Эта формулировка нашла применение не только в интуиционистской логике, для которой она была создана, но и в других логических системах. Строгие математические семантики, основанные на идее Колмогорова, обычно называют семантиками реализуемости (в отличие от других видов логических семантик, которые базируются на системах истинностных значений). Первую реализуемость построил американский логик С. К. Клини в 1940 г. для арифметики с интуиционистской логикой. В 1960–1980-х гг. появились десятки понятий реализуемости как для систем, базирующихся на интуиционистской логике, так и для других логик. Советский логик А. А. Воронков в 1985 г. вывел условия, при которых классическая логика может рассматриваться как конструктивная. Из них, в частности, следует, что необходимым (но не достаточным) условием конструктивности классической теории является ее полнота, т. е. выводимость в ней для каждой замкнутой формулы $F$ либо самой $F$ , либо ее отрицания $\lnot F$ . (Тем самым еще раз подтвердилось прозрение Брауэра относительно логических корней неконструктивности.) Заметим, что примерами классических теорий, имеющих конструктивное истолкование, служат элементарная геометрия и алгебраическая теория вещественных чисел. Описание программирования с помощью логики основано на определенной аналогии между выводом формулы в некотором логическом исчислении и программой решения задачи, отвечающей этой формуле при конструктивной интерпретации логики. Логическая теория, соответствующая структурным схемам программ, появилась в середине 1980-х гг. Структурные схемы соответствовали нарождающемуся новому типу логики — логики схем программ, которой пользуется программист для создания сложных, многовариантных, итеративных планов действий. Имеется корректная и полная система конструктивных правил вывода (логика $\Omega_1$ ), позволяющих при помощи некоторой структурной схемы построить доказательство возможности преобразовать $A$ в $B$ на базе заданных функций, преобразующих некоторые $A_{i}$ в $B_{i}\colon$ $\frac{A \Rightarrow B,\, C \Rightarrow D}{A\lor C \Rightarrow B\lor D}$ правило условного оператора (ПУО); $\frac{A\to B,\, B \Rightarrow C,\, C\to D}{A \Rightarrow D}$ правило релаксации (ПР); $\frac{A\lor C \Rightarrow B\lor C}{A \Rightarrow B}$ правило зацикливания (ПЗ); $\frac{A \Rightarrow A}{\lnot A}$ правило бесконечного цикла (ПБЦ); $\frac{\lnot A}{A \Rightarrow A}$ правило ошибки (ПО). Все перечисленные правила имеют конструктивное истолкование. Для ПУО и ПЗ оно видно из их названий. В ПУО $A$ и $B$ — охраны создаваемого условного оператора, в ПЗ $C$ — инвариант создаваемого цикла, $B$ — условие его завершения. ПР не преобразует, оно лишь говорит о том, что то же/можно использовать и в более частной ситуации, чем $A\Rightarrow B$ . ПБЦ утверждает, что застой не может быть вечен. ПО постулирует существование нигде не определенной функции "ошибка". Таким образом, конструктивное описание ситуации, где классические средства работают плохо, оказалось весьма компактным и эффективным. Логика $\Omega_1$ — лишь одна из простейших логик схем программ, успешно используемых в автоматизированном планировании действий. Интуиционистская логика из конструктивных логик с точки зрения синтаксиса оказалась наиболее близкой к традиционной логике. Она полностью сохранила язык исчисления предикатов и логические связки классической логики (вложив в них свой, конструктивный, смысл). Она по возможности сохранила и правила классической логики постольку, поскольку они не влекут закона исключенного третьего $P\lor\lnot P$ (принципа всезнания в конструктивной интерпретации) или закона двойного отрицания $\lnot\lnot P\Rightarrow P$ . Этот закон, как выяснил Брауэр, влечет принцип всезнания, а сам конструктивно может быть истолкован как существование Общего Решателя Задач (такой же нонсенс, как вечный двигатель). Задача построения программы выражается в интуиционистской логике с помощью функциональной формулы: $(\forall x) \bigl[A_1\land \ldots\land A_n\, \Rightarrow\, (\exists y)(B_1\land \ldots\land B_k)\bigr].$ Здесь $x$ — входные переменные создаваемой программы; $y$ — ее результаты; $B_{i}$ задают связи вход-выход; $A_{i}$ амбивалентны: они могут представлять как условия на входы, так и входные значения сложных типов (структуры данных, функции-параметры). Например, формула $(\forall x) \bigl[x \geqslant 0\,\Rightarrow\, (\exists y)(y \geqslant 0\land y^2=x)\bigr]$ интерпретируется как задача построения программы вычисления квадратного корня из $x$ , а формула $\begin{gathered}(\forall x,y)\Big[ x<y\land (\forall z)\bigl(x \leqslant z\land z\leqslant y \Rightarrow (\exists u)(M(z,u))\bigr)\,\Rightarrow\\ \Rightarrow (\exists v)(\forall z,u)\bigl(x \leqslant z\land z \leqslant y\land M(z,u)\Rightarrow u<v\bigr)\Big] \end{gathered}$ может трактоваться как задача построения оператора, ставящего в соответствие функции, определенной на $[x,y]$ и перерабатывающей $z$ в ${u}$ , ее верхнюю границу. Из-за отсутствия принципа всезнания выразительные возможности интуиционистской логики существенно повышаются по сравнению с классической. На ее языке можно постулировать не только знание, но порой и незнание. Например, то, что значение действительного числа не может быть задано точно, постулируется в форме $\lnot(\forall x,y)(x>y\lor y>x\lor x=y).$ Но повышение выразительной силы и "аккуратности" выводов в интуиционистской логике по сравнению с классической имеет и оборотную сторону: поиск вывода в ней существенно сложнее. В частности, метод резолюций в ней неприменим, потому что формулы не могут быть разложены на дизъюнкты. Интуиционистская логика хорошо подходит для описания задач, в которых требуется вычислить новые величины по заданным величинам и ни один из вычислительных ресурсов (время, память, надежность) не налагает ограничений. Для других ситуаций интуиционистскую логику приходится варьировать. Впервые на возможности логики в качестве инструмента анализа понятий программирования обратили внимание в середине 1970-х гг. в связи с развитием теории верификации (проверки правильности) программ. Оказалось, что для многих конструкций программирования, совместное использование которых не приводит к алгоритмической невычислимости, невозможно построить полную формальную систему, описывающую их взаимодействие. Например, рассмотрение логики схем программ позволило установить, что операторы GOTO естественно получаются в том случае, если все рассматриваемые действия можно считать глобальными преобразованиями состояния системы. Циклы оказались хорошо совместимы с массивами и плохо — с рекурсивными структурами данных, а процедуры высших типов — наоборот. Массивы и сложные структуры данных плохо совместимы с присваиваниями (в данном случае присваивание дается на целый ряд операторов, несущих различный логический смысл). В общем, можно сделать вывод, что нет средств программирования хороших либо плохих самих по себе; хороши или плохи их комбинации. При этом любая логически разумная комбинация оказывается неуниверсальной, она приспособлена лишь для определенного класса задач. Верификация (доказательство правильности) программ с помощью математической логики Широчайшее использование компьютеров в самых разнообразных сферах человеческой деятельности выдвигает на одно из первых мест вопрос о надежности программного обеспечения компьютеров. Как известно, правильность созданной программы обычно проверяется на ряде так называемых тестовых примеров, на начальных данных, для которых результат известен или его можно предсказать. Нетрудно понять, что такая проверка способна лишь выявить наличие ошибок в программе, но не доказать их отсутствие, что, разумеется, не одно и то же. Поэтому исключительно важна задача строгого доказательства правильности программ, и именно для этой цели и начали разрабатываться программные и динамические логики. С интуиционистской точки зрения программа будет правильной, если в результате ее выполнения будет достигнут тот результат, с целью получения которого и была написана программа. (Обратите внимание, что мы не рассматриваем программы, содержащие синтаксические ошибки, т. е. предполагаем, что с точки зрения языка программирования программа написана безупречно.) Доказательство правильности программы состоит в предъявлении такой цепочки аргументов, которые убедительно свидетельствуют о том, что это действительно так, т.е. что программа на самом деле решает поставленную задачу. Сформулируем теперь точное определение понятия правильности программы. Пусть $\alpha$ — программа, $P$ — утверждение, относящееся к входным данным, которое должно быть истинно перед выполнением программы $\alpha$ (оно называется предусловием программы $\alpha$ ), $Q$ — утверждение, которое должно быть истинно после выполнения программы $\alpha$ (оно называется постусловием программы $\alpha$ ). Различают два вида правильности программ: частичную и тотальную (полную). Программа $\alpha$ называется частично правильной относительно предусловия $P$ и постусловия $Q$ , если всякий раз, когда перед выполнением $\alpha$ предусловие $P$ истинно для входных значений переменных и $\alpha$ завершает работу, постусловие $Q$ также будет истинно для выходных значений переменных. В этом случае будем использовать запись $P[\alpha]Q$ . Программа а называется тотально правильной относительно $P$ и $Q$ , если она частично правильна относительно $P$ и $Q$ и $\alpha$ обязательно завершает свою работу для входных значений переменных, удовлетворяющих условию $P$ . В этом случае пишем $P[\alpha!]Q$ . Обратим внимание на то, что понятие правильности программы а сформулировано относительно соответствующих утверждений (условий) $P$ и $Q$ . Поэтому из истинности утверждения $P[\alpha]Q$ (или $P[\alpha!]Q$ соответственно) не обязательно следует истинность утверждения о правильности программы при других пред- и постусловиях. Аналогичным образом, замена в $P[\alpha]Q$ (или $P[\alpha!]Q$ ) программы $\alpha$ на программу $\beta$ , вообще говоря, не сохраняет истинностного значения утверждения о правильности. Не следует также думать, что при данных условиях $P$ и $Q$ существует только одна программа $\alpha$ , для которой высказывание $P[\alpha]Q$ (или $P[\alpha!]Q$ ) истинно. Говорить о правильности программы самой по себе бессмысленно. Программа пишется с целью решения той или иной конкретной задачи. Каждая правильно поставленная задача содержит в себе условие (то, что дано) и вопрос, на который нужно дать ответ. При составлении программы условие задачи превращается в предусловие, а вопрос преобразуется в постусловие, имеющее уже форму не вопроса, а утверждения, которое должно быть истинно всякий раз, когда ответ на вопрос задачи правилен. Из определений следует, что всякая тотально правильная программа является частично правильной при тех же пред- и постусловиях. Обратное конечно же неверно. Ясно, что тотальная правильность "лучше" частичной, хотя доказать тотальную правильность программы, по-видимому, сложнее, чем частичную. Для доказательства частичной правильности операторных программ обычно используются различные модификации метода Флойда, который состоит в следующем. На схеме программы выбираются контрольные точки так, чтобы любой циклический путь проходил по крайней мере через одну точку. С каждой контрольной точкой ассоциируется специальное условие (индуктивное утверждение или инвариант цикла), которое истинно при каждом переходе через эту точку. С входом и выходом схемы также ассоциируются пред- и постусловия. Затем каждому пути программы между двумя соседними контрольными точками сопоставляется так называемое условие правильности. Выполнимость всех условий правильности гарантирует частичную правильность программы. Один из способов доказательства завершения работы программы состоит во введении в программу дополнительных счетчиков для каждого цикла и в доказательстве их ограниченности в процессе доказательства частичной правильности программы. Одна из модификаций метода Флойда заключается в построении конечной аксиоматической системы (так называемой "логики Хоара"), состоящей из схем аксиом и правил вывода, в которой в качестве теорем выводимы утверждения о частичной правильности программ, в частности на языке программирования Паскаль. Такая система используется и для задания аксиоматической семантики языка Паскаль. Аксиоматические системы, родственные логике Хоара, разработаны и для других алгоритмических языков программирования. Для доказательства правильности рекурсивных программ используется метод математической индукции, связанный с определением наименьшей неподвижной точки, а для программ со сложными структурами данных (например, графами, деревьями) — индукция по структуре данных. При этом в теоретических исследованиях по логике Хоара рассматриваются обычные свойства аксиоматизаций в логике — их непротиворечивость и полнота. Пример 38.2. Рассмотрим простой пример программы и проанализируем ее на правильность. Требуется составить программу, которая для любых натуральных хи у давала бы ответ на вопрос, делится ли $x$ на $y$ . Будем писать " $y\|x$ " вместо " $x$ делится на $y$ ". Тогда определение делимости можно записать следующим образом: $(\forall x\in \mathbb{N})(\forall y\in \mathbb{N}) \bigl[y\|x \leftrightarrow (\exists n\in \mathbb{N})(ny=x)\bigr].$ Что должен делать компьютер, чтобы выяснить, существует ли такое $n$ , что $ny=x$ ? Заменим последнее условие на следующее $x=y+y+\ldots+y$ (п слагаемых), которое, в свою очередь, равносильно следующему: $0=x-y-y-\ldots-y$ ( $n$ вычитаемых). Проверка этого условия уже под силу компьютеру: нужно организовать цикл, который на каждом шаге вычитает сначала из $x$ число $y$ , затем из результата снова $y$ , и так до тех пор, пока не получится число 0 или отрицательное число. В первом случае ответ на вопрос о делимости $x$ на $y$ будет положительным, во втором — отрицательным. Структурная схема программы, реализующей указанный алгоритм, представлена ниже. Итак, условие, налагаемое на входные данные: $x\in\mathbb{N},~ y\in\mathbb{N}$ ; условие, которое необходимо проверить: $z=0$ . Докажем правильность этой структурной схемы и соответствующей программы методом от противного. Суть этого метода состоит в следующем. Допустим, что требуется доказать утверждение $A$ . Мы принимаем гипотезу о том, что $A$ ложно, т.е. истинно $\lnot A$ . Если из $\lnot A$ удается вывести противоречие $B\land\lnot B$ , то заключаем, что $\lnot A$ на самом деле ложно (поскольку влечет противоречие). Значит, истинно $A$ . В случае с рассматриваемой программой мы хотим доказать, что выдача нашей программой результата $z=0$ действительно будет происходить в том и только в том случае, когда $x$ делится на $y$ . Это значит, что доказываемое утверждение $A$ имеет вид: " $z=0 \leftrightarrow y\|x$ ". Допустим, что это утверждение неверно. Это означает, что ложна одна из импликаций " $z=0\to y\|x$ " или " $y\|x\to z=0$ ". Предположим сначала, что ложна первая импликация " $z=0\to y\|x$ ", то есть $z=0$ истинно, но $x$ на $y$ не делится. В соответствии со структурной схемой $z=0$ либо когда $x=0$ , либо когда в процессе вычитания $x-y-y-\ldots-y$ на некотором шаге получится 0. В первом случае $x$ делится на $y$ в противоречие с допущением. То же происходит и во втором случае. Если $x-y-y-\ldots-y=0$ , то $x-ny=0$ , то есть $x=ny$ для некоторого $n$ , что и означает делимость $x$ на $y$ . Допустим теперь, что ложна вторая импликация, т.е. что $x$ делится на $y$ , но $z\ne0$ . Неравенство $z\ne0$ может иметь место в одном из следующих трех случаев: а) при невыполнении условия $x\geqslant y$ , то есть при $x<y$ ; б) после завершения цикла; в) в ходе выполнения цикла. Поскольку присваивание $z\,\colon\!=x$ при $x\ne0$ приводит к вхождению в цикл (так как из $x\ne0$ следует $x>0,\, x>0$ ), поэтому никаких других возможностей для $z\ne0$ , кроме указанных трех, на структурной схеме не существует. Рассмотрим последовательно эти три возможности: а) если $x<y$ , то по структурной схеме $z\,\colon\!=-1$ , то есть $z\ne0$ , а значит, $x$ не делится на $y$ в противоречие с допущением; б) если цикл завершен и $z\ne0$ , то $z<0$ . Это означает, что $x-ky<0$ , то есть $x<ky$ и $\lnot(\exists n\in \mathbb{N})(x=ny)$ . Следовательно, $x$ не делится на $y$ , что также противоречит допущению; в) $z\ne0$ в ходе выполнения цикла. Но в этом случае мы и не требуем, чтобы был дан ответ на вопрос о делимости $x$ на $y$ . Мы рассчитываем его получить после выполнения программы, а не в ходе ее выполнения. Но только что было доказано, что если цикл завершится с $z\ne0$ , то $x$ на $y$ не делится. Здесь мы обнаруживаем, что цикл может и не завершиться, если $z$ будет оставаться положительным. Это будет происходить в том случае, когда $y=0$ и $z-0=z= x>0$ . Но так и должно быть: ведь в этом случае мы будем пытаться установить, делится ли положительное число $x$ на 0, а такая операция запрещена. Таким образом, мы устанавливаем, что если наша программа завершится, то она решит поставленную задачу, т.е. мы доказали частичную правильность нашей программы. Чтобы сделать нашу программу тотально правильной, нужно предусмотреть ее завершение и в выявленном исключительном случае. Для этого можно, например, перед проверкой условия $x\geqslant y$ проверить утверждение " $x>0\land y=0$ ". Если оно истинно, перейти к присваиванию $z\,\colon\!-1$ , если же оно ложно — перейти к проверке $x\geqslant y$ . В заключение отметим, что исследования по логическому описанию программ и программирования убедительно показали, что логический анализ позволяет анализировать концепции языков программирования и находить многие скрытые недоработки в этих концепциях. Пожалуй, до сих пор это применение строгих математических методов в качестве инструмента критики концепций (зачастую совершенно не продуманных, вставляемых ради "усиления" языков программирования) является важнейшим применением математической логики в области программирования. Математический форум (помощь с решением задач, обсуждение вопросов по математике). Если заметили ошибку, опечатку или есть предложения, напишите в комментариях.

Математическая логика и языки программирования

Онлайн-сервисы

Нахождение НОД и НОК Разложение числа на простые множители Сравнения по модулю Операции над множествами Операции над векторами Разложение вектора по базису. Доказательство, что векторы образуют базис Чертёж треугольника по координатам вершин Решение треугольника Решение Пирамиды Построение Пирамиды по координатам вершин Чертёж многоугольника по координатам вершин Решение систем методом Крамера и Матричным Онлайн построение графика кривой 2-го порядка Определение вида кривой или поверхности 2-го порядка по инвариантам МНК и регрессионный анализ Онлайн + графики Онлайн число, сумма и дата прописью

Алгоритмы JavaScript

Алгоритмы поиска Алгоритмы сортировки Уникальные элементы массива Объединение, пересечение и разность массивов НОД и НОК Операции над матрицами Дата прописью

Введение в анализ

Функции: понятие, определение, графики Непрерывность функции Исследование функции и построение графика

Теория множеств

Множества: понятие, определение, примеры Точечные множества Замкнутые и открытые множества Мера множества Группы, кольца, поля в математике Поле комплексных чисел Кольцо многочленов Основная теорема алгебры и ее следствия

Математическая логика

Алгебра высказываний

Аксиоматика и логические рассуждения Методы доказательств теорем Алгебра высказываний и операции над ними Формулы алгебры высказываний Тавтологии алгебры высказываний Логическая равносильность формул Нормальные формы для формул высказываний Логическое следование формул Приложение алгебры высказываний для теорем Дедуктивные и индуктивные умозаключения Решение логических задач Принцип полной дизъюнкции

Булевы функции

Множества, отношения и функции в логике Булевы функции от одного и двух аргументов Булевы функции от n аргументов Системы булевых функций Применение булевых функций к релейно-контактным схемам Релейно-контактные схемы в ЭВМ Практическое применение булевых функций

Теория формального

Формализованное исчисление высказываний Полнота и другие свойства формализованного исчисления высказываний Независимость системы аксиом формализованного исчисления высказываний

Логика предикатов

Логика предикатов Логические операции над предикатами Кванторные операции над предикатами Формулы логики предикатов Тавтологии логики предикатов Преобразования формул и следование их предикатов Проблемы разрешения для общезначимости и выполнимости формул Применение логики предикатов в математике Строение математических теорем Аристотелева силлогистика и методы рассуждений Принцип полной дизъюнкции в предикатной форме Метод полной математической индукции Необходимые и достаточные условия Логика предикатов и алгебра множеств Формализованное исчисление предикатов

Неформальные и формаль-
ные аксиоматические теории

Неформальные аксиоматические теории Свойства аксиоматических теорий Формальные аксиоматические теории Формализация теории аристотелевых силлогизмов Свойства формализованного исчисления предикатов Формальные теории первого порядка Формализация математической теории

Теория алгоритмов

Интуитивное представление об алгоритмах Машины Тьюринга и тезис Рекурсивные функции Нормальные алгоритмы Маркова Разрешимость и перечислимость множеств Неразрешимые алгоритмические проблемы Теорема Гёделя о неполноте формальной арифметики

Математическая логика и компьютеры

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

Дискретная математика

Множества и отношения

Теория множеств: понятия и определения Операции над множествами Кортеж и декартово произведение множеств Соответствия и бинарные отношения на множествах Операции над соответствиями на множествах Семейства множеств Специальные свойства бинарных отношений Отношения эквивалентности на множестве Упорядоченные множества Теорема о неподвижной точке Мощность множества Парадокс Рассела Метод характеристических функций

Группы и кольца

Алгебраические структуры и операции Группоиды, полугруппы, группы Кольца, тела, поля Области целостности в теории колец Модули и линейные пространства Подгруппы и подкольца Теорема Лагранжа о порядке конечной группы Гомоморфизмы групп и нормальные делители Гомоморфизмы и изоморфизмы колец Алгебра кватернионов

Полукольца и булевы алгебры

Полукольца: определение, аксиомы, примеры Замкнутые полукольца Полукольца и системы линейных уравнений Булевы алгебры и полукольца Решетки и полурешетки

Алгебраические системы

Алгебраические системы: модели и алгебры Подсистемы алгебраических систем Конгруэнции и фактор-системы Гомоморфизмы алгебраических систем Прямые произведения алгебраических систем Конечные булевы алгебры Многосортные алгебры

Теория графов

Теория графов: основные понятия и определения Способы представления графов Неориентированные и ориентированные деревья Остовное дерево и алгоритм Краскала Методы систематического обхода вершин графа Алгоритмы поиска в глубину и ширину в графах Задача о путях во взвешенных ориентированных графах Изоморфизм, гомоморфизм и автоморфизм графов Топологическая сортировка вершин графа Элементы цикломатики в теории графов

Булева алгебра и функции

Булевы функции и булев куб Таблицы булевых функций и булев оператор Равенство булевых функций. Фиктивные переменные Формулы и суперпозиции булевых функций Дизъюнктивные и конъюнктивные нормальные формы Построение минимальных ДНФ Теорема Поста и классы Критерий Поста Схемы из функциональных элементов

Конечные автоматы и регулярные языки

Конечные автоматы и регулярные языки Алфавит, слово, язык в программировании Порождающие грамматики (грамматики Хомского) Классификация грамматик и языков Регулярные языки и регулярные выражения Конечные автоматы Допустимость языка конечным автоматом Теорема Клини Детерминизация конечных автоматов Минимизация конечных автоматов Лемма о разрастании для регулярных языков Обоснование алгоритма детерминизации автоматов Конечные автоматы с выходом Морфизмы и конечные подстановки Машины Тьюринга

Контекстно-свободные языки

Контекстно-свободные языки и грамматики Приведенная форма КС-грамматики Лемма о разрастании для КС-языков Магазинные автоматы (автомат с магазинной памятью) Алгоритм построения МП-автомата по КС-грамматике Алгоритм построения КС-грамматики по МП-автомату Алгебраические свойства КС-языков Основное свойство суперпозиции КС-языков Пересечение контекстно-свободных языков Методы синтаксического анализа КС-языков Восходящий синтаксический анализ и LR(k)-грамматики Семантика формальных языков Принцип индукции по неподвижной точке Графовое представление МП-автоматов

Интегральное исчисление

Неопределённый и определённый

Неопределенный и определенный интегралы Свойства интегралов Интегрирование по частям Интегрирование методом замены переменной Интегрирование различных рациональных функций Интегрирование различных иррациональных функций Интегрирование различных тригонометрических функций Определенный интеграл и его основные свойства Необходимое и достаточное условие интегрируемости Теоремы существования первообразной Свойства определенных интегралов Несобственные интегралы Интегральное определение логарифмической функции

Приложения интегралов

Вычисление площадей плоских фигур Площади фигур в различных координатах Вычисление объемов тел с помощью интегралов Объём тела вращения Вычисление длин дуг кривых Формулы длины дуги регулярной кривой Кривизна плоской кривой Площадь поверхности вращения тела

Интегралы в физике

Статические моменты и координаты центра тяжести Теоремы Гульдина–Паппа Вычисление моментов инерции Другие приложения интегралов в физике

Основные интегралы

Интеграл Ньютона-Лейбница Интеграл Римана Интеграл Лебега

Вариационное исчисление

Примеры вариационных задач Дифференциальное уравнение Эйлера Функционалы, зависящие от нескольких функций Задача о минимуме кратного интеграла

Финансовый анализ

Анализ эффективности

Критерии и показатели эффективности предприятия Методы анализа эффективности деятельности Факторный анализ прибыли от операционной деятельности Анализ безубыточности предприятия Операционный рычаг и эффект финансового рычага Анализ и оценка состава, структуры и динамики доходов и расходов Анализ рентабельности и резервов устойчивого роста капитала Анализ распределения прибыли предприятия Анализ и оценка чувствительности показателей эффективности

Анализ устойчивости

Финансовая устойчивость и долгосрочная платежеспособность Характеристика типов финансовой устойчивости

Рыночная активность

Финансовый анализ рыночной активности Методика анализа рыночной активности Анализ и оценка дивидендного дохода на одну акцию

Инвестиционная деятельность

Инвестиции: экономическая сущность и классификация Государственное регулирование инвестиционной деятельности Источники финансовых ресурсов на капитальные вложения Инвестиции в основные фонды Оценка состояния основных фондов Амортизация основных фондов Капитальное строительство в инвестиционном процессе Планирование инвестиций в форме капитальных вложений Экономическая эффективность инвестиций Финансирование капитальных вложений Кредитование капитальных вложений Кредитоспособность Финансирование и кредитование затрат Финансирование и кредитование инвестиционной деятельности потребительской кооперации Финансирование и кредитование капитальных вложений потребительской кооперации Инвестиционное строительное проектирование

Анализ инвестиций

Инвестиции и инвестиционная деятельность предприятия Задачи финансового анализа инвестиций предприятия Учет фактора времени в инвестиционной деятельности Аннуитет и финансовая рента в инвестициях Учет фактора инфляции при инвестировании Оценка фактора риска инвестиционного проекта Методы оценки эффективности инвестиций Показатели эффективности инвестиционного проекта

Стоимость компании

Концепция построения международных стандартов финансовой отчетности (МСФО) Экономическое содержание международных стандартов финансовой отчётности Цели и принципы оценки стоимости акций и активов компании Оценка акций и активов предприятия по справедливой стоимости Методы оценки справедливой стоимости акций предприятия Затратный подход к оценки стоимости компаний и акций Сравнительный подход к оценки стоимости предприятий и акций Доходный подход к оценке стоимости компании и акций Выбор ставки дисконтирования при инвестировании в акции Метод капитализации прибыли Сравнение подходов к оценке стоимости компаний и пакетов акций

Форвардные контракты

Форвардный контракт и цена Форвардная цена акции на бирже Цена форвардного контракта инвестора Форвардная цена акции с учетом величины дивиденда Форвардная цена акции с учетом ставки дивиденда Форвардная цена валюты на рынке форекс Форвардный валютный курс и инфляция на рынке Форвардная цена товара и спотовый рынок Форвардная цена при различии ставок по кредитам и депозитам Синтетический форвардный контракт на акции и валюту

Теория вероятностей

Основные понятия теории вероятностей Зависимые и независимые случайные события Повторные независимые испытания Формула Бернулли Одномерные случайные величины Многомерные случайные величины Функции случайных величин Законы распределения целочисленных случайных величин Законы распределения непрерывных случайных величин Предельные теоремы теории вероятностей Закон больших чисел и предельные теоремы Вероятностные закономерности

Математическая статистика

Элементы математической статистики Выборочный метод Оценки параметров генеральной совокупности Статистические гипотезы Критерии согласия Теоретические и эмпирические частоты

Теория очередей (СМО)

Определение системы массового обслуживания Уравнения Колмогорова Предельные вероятности состояний Определение СМО с отказами Определение СМО с ожиданием (очередью)

Аналитическая геометрия

Векторная алгебра

Метрические понятия и аксиомы геометрии Равенство и подобие геометрических фигур Бинарные отношения Вектор, его направление и длина Линейные операции над векторами Линейная зависимость и независимость векторов Отношение коллинеарных векторов Проекции векторов на прямую и на плоскость Угол между векторами Ортогональные проекции векторов Координата вектора на прямой и базис Координаты вектора на плоскости и базис Координаты вектора в пространстве и базис Операции над векторами в координатной форме Ортогональный и ортонормированный базисы Cкалярное произведение векторов и его свойства Выражение скалярного произведения через координаты векторов Векторное произведение векторов и его свойства Смешанное произведение векторов и его свойства Ориентированные площади и объемы Двойное векторное произведение и его свойства Применение векторов в задачах на аффинные свойства фигур Применение произведений векторов при решении геометрических задач Применение векторной алгебры в механике

Системы координат

Прямоугольные координаты Преобразования прямоугольных координат Полярная система координат Цилиндрическая система координат Сферические координаты Аффинные координаты Аффинные преобразования координат Аффинные преобразования плоскости Примеры аффинных преобразований плоскости Аффинные преобразования пространства Многомерное координатное пространство Линейные и аффинные подпространства Скалярное произведение n-мерных векторов Преобразования систем координат

Геометрия на плоскости

Алгебраические линии на плоскости Общие уравнения геометрических мест точек Алгебраические уравнения линий на плоскости Уравнения прямой, проходящей через точку перпендикулярно вектору Уравнения прямой, проходящей через точку коллинеарно вектору Уравнения прямой, проходящей через две точки Уравнения прямой с угловым коэффициентом Взаимное расположение прямых Примеры задач с прямыми на плоскости Системы неравенств с двумя неизвестными Системы линейных уравнений с двумя неизвестными

Линии 2-го порядка

Канонические уравнения линий второго порядка Порядок приведения уравнения линии к каноническому виду Эллипс Гипербола Парабола Квадратичные неравенства с двумя неизвестными Применение линий 1-го и 2-го порядков в задачах на экстремум функций

Инварианты линий

Классификация линий 2-го порядка по инвариантам Приведение уравнения линии к каноническому виду по инвариантам

Геометрия в пространстве

Способы задания ГМТ в пространстве Алгебраические уравнения поверхностей Уравнения плоскости, проходящей через точку перпендикулярно вектору Уравнения плоскости, компланарной двум неколлинеарным векторам Уравнения плоскости, проходящей через три точки Взаимное расположение плоскостей Типовые задачи с плоскостями Уравнения прямых в пространстве Взаимное расположение прямых в пространстве Типовые задачи с прямыми в пространстве

Поверхности 2-го порядка

Канонические уравнения поверхностей Порядок приведения уравнения поверхности к каноническому виду Поверхности второго порядка Эллипсоиды Гиперболоиды Конусы Параболоиды Применение поверхностей 1-го и 2-го порядков в задачах на экстремум функций

Инварианты поверхностей

Классификация поверхностей 2-го порядка по инвариантам Квадратичные неравенства с тремя неизвестными Приведение уравнения поверхности к канониче-скому виду по инвариантам

Линейная алгебра

Матрицы и операции

Линейные операции над матрицами Умножение матриц Возведение матриц в степень Многочлены от матриц Транспонирование и сопряжение матриц Блочные матрицы Произведение и сумма матриц Кронекера Метод Гаусса приведения матрицы к ступенчатому виду Элементарные преобразования матриц

Определители

Определители матриц и их основные свойства Формула полного разложения определителя Формула Лапласа полного разложения определителя Определитель произведения матриц Методы вычисления определителей

Ранг матрицы

Линейная зависимость и линейная независимость строк (столбцов) матрицы Ранг матрицы и базисный минор матрицы Методы вычисления ранга матрицы Ранг системы столбцов (строк)

Обратная матрица

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

Системы уравнений

Системы линейных алгебраических уравнений Метод Гаусса решения систем линейных уравнений Структура общего решения системы уравнений Решение систем с помощью полуобратных матриц Псевдорешения системы линейных уравнений

Функциональные матрицы

Функциональные матрицы скалярного аргумента Производные матриц по векторному аргументу Линейные и квадратичные формы и их преобразования Приведение форм к каноническому виду Закон инерции вещественных квадратичных форм Знакоопределенность форм вещественных квадратичных Формы и исследование функций на экстремум

Многочленные матрицы

Многочленные матрицы (лямбда-матрицы) Операции над лямбда-матрицами Простые преобразования многочленных матриц Инвариантные множители многочленной матрицы

Функции от матриц

Собственные векторы и значения матрицы Подобие числовых матриц Характеристический многочлен матрицы Минимальный многочлен матрицы Теорема Гамильтона-Кэли Жорданова форма матрицы Приведение матрицы к жордановой форме Многочлены от матриц Применение многочленов от матриц Функции от матриц

Линейные пространства

Линейные пространства: определение и примеры Линейная зависимость и независимость n-мерных векторов Размерность и базис линейного пространства Преобразования координат в линейном пространстве Изоморфизм линейных пространств

Подпространства

Подпространства линейного пространства Пересечение и сумма подпространств Способы описания подпространств Нахождение дополнения и суммы подпространств Нахождение пересечения подпространств

Линейные отображения

Линейные многообразия Линейные отображения Матрица линейного отображения Ядро и образ линейного отображения

Линейные операторы

Линейные операторы (преобразования) Инвариантные подпространства Собственные векторы и значения оператора Свойства собственных векторов операторов Канонический вид линейного оператора Методика приведения линейного преобразования к каноническому виду

Евклидовы пространства

Комплексный анализ

Комплексные числа

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

Комплексные функции

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

Функциональные ряды в комплексной области

Функциональные ряды и последовательности Степенные ряды и их свойства Разложение функций в степенные ряды Нули аналитических функций Ряд Лорана и разложение функций по целым степеням

Особые точки, Вычеты

Изолированные особые точки функций и полюсы Вычеты и их применение Вычисление интегралов с помощью вычетов Вычеты и расположение нулей многочлена

Операционное исчисление

Преобразование Лапласа и его свойства Решение ДУ операционным методом Анализ выходных процессов линейных стационарных систем Z-преобразование и его свойства

Дифференциальные уравнения

ДУ первого порядка

Основные понятия и определения ДУ Метод изоклин для ДУ 1-го порядка Метод последовательных приближений ДУ с разделяющимися переменными Однородные ДУ Линейные ДУ 1-го порядка Дифференциальное уравнение Бернулли ДУ в полных дифференциалах Интегрирующий множитель ДУ, не разрешенные относительно производной Дифференциальное уравнение Риккати Составление ДУ семейств линий Задачи на траектории Особые решения ДУ

ДУ высших порядков

Понятия и определения ДУ высших порядков ДУ, допускающие понижение порядка Линейная независимость функций Определители Вронского и Грама Однородные и неоднородные дифференциальные уравнения Задача Коши и Уравнение Эйлера Линейные ДУ с переменными коэффициентами Метод Лагранжа решения ДУ Краевые задачи для ДУ высших порядков Разложение решения ДУ в степенной ряд Разложение решения ДУ в обобщенный степенной ряд Нахождение периодических решений ДУ Асимптотическое интегрирование ДУ

Системы ДУ

Системы ДУ: понятия и определения Сведение системы ДУ к одному уравнению Нахождение интегрируемых комбинаций Интегрирование однородных линейных систем ДУ Методы интегрирования неоднородных систем ДУ Преобразование Лапласа и решение ДУ и систем

Теория устойчивости

Устойчивость решений ДУ по Ляпунову Простейшие типы точек покоя Метод функций Ляпунова Устойчивость решений ДУ по первому приближению Критерии устойчивости Рауса–Гурвица и Михайлова ДУ с малым параметром при производной

Численные методы

Методы алгебры

Численные методы линейной алгебры Численные методы решения СЛАУ Итерационный метод Шульца обратной матрицы Методы решения задач о собственных значениях и векторах матрицы Методы решения нелинейных уравнений Методы решения систем нелинейных уравнений

Методы теории приближений

Методы приближения сеточных функций Методы функциональной интерполяции Методы интегрально-дифференциальной интерполяции Методы интегрального сглаживания Методы интерполяции и сглаживания сплайнами Методы численного дифференцирования и интегрирования Методы численного дифференцирования Методы численного интегрирования

Методы решения обыкновенных ДУ

Численные методы решения задачи Коши Разностные схемы для решения задачи Коши Составные схемы для решения задачи Коши Экстраполяционные методы решения задачи Коши Непрерывно-дискретные методы решения задачи Коши Численные методы решения краевых задач

Методы решения ДУ в частных производных

Численные методы решения уравнений математической физики с двумя переменными Принципы построения разностных схем для уравнений в частных производных Разностные схемы решения уравнений в частных производных 1-го порядка Разностные схемы решения уравнений в частных производных 2-го порядка Численные методы решения уравнений в частных производных Численные методы решения уравнений математической физики с тремя переменными

Математическая логика и языки программирования

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

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

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

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

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

Теория алгоритмов и математическая логика — фундаментальная основа программирования. В 30-е гг. XIX в. английский математик Чарлз Бэббедж высказал впервые идею вычислительной машины. И только сто лет спустя логики разработали четыре математически эквивалентные модели понятия алгоритма (мы достаточно подробно рассмотрели в предыдущей главе три из них). Именно в теории алгоритмов были предугаданы основные концепции, которые легли в основу принципов построения и функционирования вычислительной машины с программным управлением и принципов создания языков программирования. Идею такой вычислительной машины впервые смогли реализовать болгарский ученый С. Атанасов в 1940 г. и немецкий ученый К. Цузе в 1942 г. Четыре главные модели алгоритма породили разные направления в программировании.

Первая модель — это абстрактная вычислительная машина (А. Тьюринг, Р. Пост). Она явилась абстрактным прообразом реальных вычислительных машин. До сих пор все вычислительные машины в некотором смысле базируются на идее Тьюринга: их память физически состоит из битов, каждый из которых содержит либо 0, либо 1. Программное управление унаследовало от этих абстрактных машин и программу, помещенную в "постоянную память" (идея поместить программу ЭВМ в основную память, чтобы иметь возможность изменять ее в ходе вычислений, принадлежит Джону фон Нейману), а структура команды современной ЭВМ в значительной степени напоминает структуру команды машины Тьюринга. В рамках теории машин Тьюринга откристаллизовались важнейшие для компьютерных приложений логики понятия: вычислимая функция, разрешимая задача, неразрешимая (алгоритмически) задача. Собрано большое количество определений абстрактных вычислительных машин и показано, как каждое из них можно свести к другому подходящей кодировкой входов и выходов.

Другая модель — это рекурсивные функции, идея которых восходит к гильбертовскому аксиоматическому подходу. От них унаследовало свои основные конструкции современное структурное программирование.

Третий способ описания алгоритмов — нормальные алгоритмы А. А. Маркова. Они послужили основой языка Рефал и многих других языков обработки символьной информации.

Четвертое направление в теории алгоритмов — так называемое λ-исчисление — базируется на идеях советского логика Р.Шейнфинкеля и американского логика X. Б. Карри. Оказалось, что для определения всех вычислимых функций достаточно операций так называемой λ-абстракции и суперпозиции. Идеи λ-исчисления активно развиваются в языке Лисп, функциональном программировании и во многих других перспективных направлениях современного программирования.

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

Описание компьютерных программ с помощью математической логики

Первые попытки применить в программировании развитые логические исчисления и методы формализации предпринял американский логик X. Б. Карри. В 1952 г. он сделал доклад "Логика программных композиций", идеи которого опередили свое время по крайней мере на четверть века. Карри рассмотрел задачу программирования как задачу составления более крупных программ из готовых кусков. Были введены две базисные системы конструкций: первая — последовательное исполнение, разветвление и цикл, вторая — последовательное исполнение и условный переход. Он охарактеризовал логические средства, какие можно использовать для композиции программ из подпрограмм в каждом из этих случаев.

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

В середине 1960-х гг. практически одновременно появился ряд пионерских работ в области описания условий, которым удовлетворяет программа. Советский математик В. М. Глушков в 1965 г. ввел понятие алгоритмической алгебры, послужившее прообразом алгоритмических логик. Ф. Энгелер в 1967 г. предложил использовать языки с бесконечно длинными формулами, чтобы выразить бесконечное множество возможностей, возникающих при разных исполнениях программы. Но наибольшую популярность приобрели языки алгоритмических логик. Эти языки были изобретены практически одновременно американскими логиками Р.У.Флойдом (1967), С.А.Р.Хоаром (1969) и учеными польской логической школы, например А. Сальвицким и др. (1970).

Алгоритмическая логика (или динамическая логика, или программная логика, или логика Хоара) — раздел теоретического программирования, в рамках которого исследуются аксиоматические системы, представляющие средства для задания синтаксиса и семантики языков программирования, а также для синтеза компьютерных программ и их верификации (проверки правильности работы). Языки алгоритмических логик основываются на логике предикатов 1-го порядка и включают в себя высказывания вида $\{A\}S\{B\}$ , читающиеся следующим образом: "Если до исполнения оператора $S$ было выполнено $A$ , то после него будет выполнено $B$ ". Здесь $A$ называется предусловием, $B$ — постусловием, либо обещанием $S$ . На этом языке даются логические описания операторов присвоения и условного перехода, ветвления, цикла.

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

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

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

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

Описание программирования и анализ его концепций с помощью математической логики

Программирование — это процесс составления программы, плана действий. Было замечено, что классическая логика плохо подходит для описания этого процесса хотя бы потому, что она плохо подходит вообще для описания всякого процесса в математике. Еще в начале XX в. стало ясно, что в математике Давно разошлись понятия "существовать" и "быть построенным", с античных времен трактовавшиеся как синонимы. Были выявлены так называемые математические объекты-"привидения" (множества, Функции, числа), существование которых доказано, но построить которые нельзя. Причиной их появления явился эффект сочетания классической логики с теоремой Гёделя о неполноте формальной арифметики. Один из фундаментальных законов классической логики — закон исключенного третьего $P\lor\lnot P$ в некоторой свободной трактовке фактически означает, что мы знаем все. Этот постулат конечно же никак нельзя назвать реалистическим: мы знаем чрезвычайно мало, и чем больше узнаем, тем лучше это понимаем. Голландский математик Л. Э. Я. Брауэр определил логические корни "привидений" еще до открытия теоремы Гёделя, в 1908 г., и начал построение так называемой интуиционистской математики, не принимающей закон $P\lor\lnot P$ как универсальный. В 1930–1932 гг. другой голландец А. Гейтинг строго сформулировал логику, которой пользовались в интуиционистской математике, — интуиционистскую логику. Ее математическая интерпретация, данная советским математиком А. Н. Колмогоровым в то же время, сохранила свое значение до сих пор.

А. Н. Колмогоров рассмотрел логику как исчисление задач. Каждая формула алгебры высказываний рассматривается не просто как формула, но как требование решить задачу, т.е. построить объект, удовлетворяющий некоторым условиям. Это так называемая конструктивная интерпретация логики высказываний. Логические связки понимаются как средства построения формулировок более сложных задач из более простых, аксиомы — как задачи, решения которых даны, правила вывода — как способы преобразования решений одних задач в решения других. Отметим, что решение задачи — это не только сам искомый объект, но и доказательство того, что он удовлетворяет предъявляемым требованиям. Например, формула $A\land B$ понимается в колмогоровской интерпретации как задача, состоящая в том, чтобы построить и решение задачи $A$ , и решение задачи $B$ , правило вывода $A,B\setminus A\land B$ — как преобразование, строящее из объекта $a$ , решающего задачу $A$ , и объекта $b$ , решающего задачу $B$ , пару $(a,b)$ , решающую задачу $A\land B$ . Объект $a$ , решающий задачу, сопоставленную формуле $A$ , называется реализацией $A$ . Этот факт обозначается $aRA$ . Центральным моментом конструктивного понимания логических формул является интерпретация импликации. Конструктивная импликация $A\Rightarrow B$ понимается как требование построить эффективное преобразование $f$ , применимое ко всем реализациям формулы $A$ и переводящее их в реализации формулы $B$ .

Нечеткая колмогоровская формулировка логики как исчисления задач породила многочисленные различные конкретизации, дав целую систему точных математических определений. Эта формулировка нашла применение не только в интуиционистской логике, для которой она была создана, но и в других логических системах. Строгие математические семантики, основанные на идее Колмогорова, обычно называют семантиками реализуемости (в отличие от других видов логических семантик, которые базируются на системах истинностных значений). Первую реализуемость построил американский логик С. К. Клини в 1940 г. для арифметики с интуиционистской логикой. В 1960–1980-х гг. появились десятки понятий реализуемости как для систем, базирующихся на интуиционистской логике, так и для других логик. Советский логик А. А. Воронков в 1985 г. вывел условия, при которых классическая логика может рассматриваться как конструктивная. Из них, в частности, следует, что необходимым (но не достаточным) условием конструктивности классической теории является ее полнота, т. е. выводимость в ней для каждой замкнутой формулы $F$ либо самой $F$ , либо ее отрицания $\lnot F$ . (Тем самым еще раз подтвердилось прозрение Брауэра относительно логических корней неконструктивности.) Заметим, что примерами классических теорий, имеющих конструктивное истолкование, служат элементарная геометрия и алгебраическая теория вещественных чисел.

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

Имеется корректная и полная система конструктивных правил вывода (логика $\Omega_1$ ), позволяющих при помощи некоторой структурной схемы построить доказательство возможности преобразовать $A$ в $B$ на базе заданных функций, преобразующих некоторые $A_{i}$ в $B_{i}\colon$

$\frac{A \Rightarrow B,\, C \Rightarrow D}{A\lor C \Rightarrow B\lor D}$ правило условного оператора (ПУО);

$\frac{A\to B,\, B \Rightarrow C,\, C\to D}{A \Rightarrow D}$ правило релаксации (ПР);

$\frac{A\lor C \Rightarrow B\lor C}{A \Rightarrow B}$ правило зацикливания (ПЗ);

$\frac{A \Rightarrow A}{\lnot A}$ правило бесконечного цикла (ПБЦ);

$\frac{\lnot A}{A \Rightarrow A}$ правило ошибки (ПО).

Все перечисленные правила имеют конструктивное истолкование. Для ПУО и ПЗ оно видно из их названий. В ПУО $A$ и $B$ — охраны создаваемого условного оператора, в ПЗ $C$ — инвариант создаваемого цикла, $B$ — условие его завершения. ПР не преобразует, оно лишь говорит о том, что то же/можно использовать и в более частной ситуации, чем $A\Rightarrow B$ . ПБЦ утверждает, что застой не может быть вечен. ПО постулирует существование нигде не определенной функции "ошибка".

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

Логика $\Omega_1$ — лишь одна из простейших логик схем программ, успешно используемых в автоматизированном планировании действий.

Интуиционистская логика из конструктивных логик с точки зрения синтаксиса оказалась наиболее близкой к традиционной логике. Она полностью сохранила язык исчисления предикатов и логические связки классической логики (вложив в них свой, конструктивный, смысл). Она по возможности сохранила и правила классической логики постольку, поскольку они не влекут закона исключенного третьего $P\lor\lnot P$ (принципа всезнания в конструктивной интерпретации) или закона двойного отрицания $\lnot\lnot P\Rightarrow P$ . Этот закон, как выяснил Брауэр, влечет принцип всезнания, а сам конструктивно может быть истолкован как существование Общего Решателя Задач (такой же нонсенс, как вечный двигатель).

Задача построения программы выражается в интуиционистской логике с помощью функциональной формулы:

$(\forall x) \bigl[A_1\land \ldots\land A_n\, \Rightarrow\, (\exists y)(B_1\land \ldots\land B_k)\bigr].$

Здесь $x$ — входные переменные создаваемой программы; $y$ — ее результаты; $B_{i}$ задают связи вход-выход; $A_{i}$ амбивалентны: они могут представлять как условия на входы, так и входные значения сложных типов (структуры данных, функции-параметры). Например, формула

$(\forall x) \bigl[x \geqslant 0\,\Rightarrow\, (\exists y)(y \geqslant 0\land y^2=x)\bigr]$

интерпретируется как задача построения программы вычисления квадратного корня из $x$ , а формула

$\begin{gathered}(\forall x,y)\Big[ x<y\land (\forall z)\bigl(x \leqslant z\land z\leqslant y \Rightarrow (\exists u)(M(z,u))\bigr)\,\Rightarrow\\ \Rightarrow (\exists v)(\forall z,u)\bigl(x \leqslant z\land z \leqslant y\land M(z,u)\Rightarrow u<v\bigr)\Big] \end{gathered}$

может трактоваться как задача построения оператора, ставящего в соответствие функции, определенной на $[x,y]$ и перерабатывающей $z$ в ${u}$ , ее верхнюю границу.

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

$\lnot(\forall x,y)(x>y\lor y>x\lor x=y).$

Но повышение выразительной силы и "аккуратности" выводов в интуиционистской логике по сравнению с классической имеет и оборотную сторону: поиск вывода в ней существенно сложнее. В частности, метод резолюций в ней неприменим, потому что формулы не могут быть разложены на дизъюнкты.

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

Впервые на возможности логики в качестве инструмента анализа понятий программирования обратили внимание в середине 1970-х гг. в связи с развитием теории верификации (проверки правильности) программ. Оказалось, что для многих конструкций программирования, совместное использование которых не приводит к алгоритмической невычислимости, невозможно построить полную формальную систему, описывающую их взаимодействие. Например, рассмотрение логики схем программ позволило установить, что операторы GOTO естественно получаются в том случае, если все рассматриваемые действия можно считать глобальными преобразованиями состояния системы. Циклы оказались хорошо совместимы с массивами и плохо — с рекурсивными структурами данных, а процедуры высших типов — наоборот. Массивы и сложные структуры данных плохо совместимы с присваиваниями (в данном случае присваивание дается на целый ряд операторов, несущих различный логический смысл).

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

Верификация (доказательство правильности) программ с помощью математической логики

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

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

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

Сформулируем теперь точное определение понятия правильности программы. Пусть $\alpha$ — программа, $P$ — утверждение, относящееся к входным данным, которое должно быть истинно перед выполнением программы $\alpha$ (оно называется предусловием программы $\alpha$ ), $Q$ — утверждение, которое должно быть истинно после выполнения программы $\alpha$ (оно называется постусловием программы $\alpha$ ). Различают два вида правильности программ: частичную и тотальную (полную). Программа $\alpha$ называется частично правильной относительно предусловия $P$ и постусловия $Q$ , если всякий раз, когда перед выполнением $\alpha$ предусловие $P$ истинно для входных значений переменных и $\alpha$ завершает работу, постусловие $Q$ также будет истинно для выходных значений переменных. В этом случае будем использовать запись $P[\alpha]Q$ . Программа а называется тотально правильной относительно $P$ и $Q$ , если она частично правильна относительно $P$ и $Q$ и $\alpha$ обязательно завершает свою работу для входных значений переменных, удовлетворяющих условию $P$ . В этом случае пишем $P[\alpha!]Q$ .

Обратим внимание на то, что понятие правильности программы а сформулировано относительно соответствующих утверждений (условий) $P$ и $Q$ . Поэтому из истинности утверждения $P[\alpha]Q$ (или $P[\alpha!]Q$ соответственно) не обязательно следует истинность утверждения о правильности программы при других пред- и постусловиях. Аналогичным образом, замена в $P[\alpha]Q$ (или $P[\alpha!]Q$ ) программы $\alpha$ на программу $\beta$ , вообще говоря, не сохраняет истинностного значения утверждения о правильности. Не следует также думать, что при данных условиях $P$ и $Q$ существует только одна программа $\alpha$ , для которой высказывание $P[\alpha]Q$ (или $P[\alpha!]Q$ ) истинно.

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

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

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

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

Одна из модификаций метода Флойда заключается в построении конечной аксиоматической системы (так называемой "логики Хоара"), состоящей из схем аксиом и правил вывода, в которой в качестве теорем выводимы утверждения о частичной правильности программ, в частности на языке программирования Паскаль. Такая система используется и для задания аксиоматической семантики языка Паскаль. Аксиоматические системы, родственные логике Хоара, разработаны и для других алгоритмических языков программирования.

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

Пример 38.2. Рассмотрим простой пример программы и проанализируем ее на правильность. Требуется составить программу, которая для любых натуральных хи у давала бы ответ на вопрос, делится ли $x$ на $y$ . Будем писать " $y|x$ " вместо " $x$ делится на $y$ ". Тогда определение делимости можно записать следующим образом:

$(\forall x\in \mathbb{N})(\forall y\in \mathbb{N}) \bigl[y|x \leftrightarrow (\exists n\in \mathbb{N})(ny=x)\bigr].$

Что должен делать компьютер, чтобы выяснить, существует ли такое $n$ , что $ny=x$ ? Заменим последнее условие на следующее $x=y+y+\ldots+y$ (п слагаемых), которое, в свою очередь, равносильно следующему: $0=x-y-y-\ldots-y$ ( $n$ вычитаемых). Проверка этого условия уже под силу компьютеру: нужно организовать цикл, который на каждом шаге вычитает сначала из $x$ число $y$ , затем из результата снова $y$ , и так до тех пор, пока не получится число 0 или отрицательное число. В первом случае ответ на вопрос о делимости $x$ на $y$ будет положительным, во втором — отрицательным. Структурная схема программы, реализующей указанный алгоритм, представлена ниже.

Итак, условие, налагаемое на входные данные: $x\in\mathbb{N},~ y\in\mathbb{N}$ ; условие, которое необходимо проверить: $z=0$ . Докажем правильность этой структурной схемы и соответствующей программы методом от противного. Суть этого метода состоит в следующем. Допустим, что требуется доказать утверждение $A$ . Мы принимаем гипотезу о том, что $A$ ложно, т.е. истинно $\lnot A$ . Если из $\lnot A$ удается вывести противоречие $B\land\lnot B$ , то заключаем, что $\lnot A$ на самом деле ложно (поскольку влечет противоречие). Значит, истинно $A$ .

В случае с рассматриваемой программой мы хотим доказать, что выдача нашей программой результата $z=0$ действительно будет происходить в том и только в том случае, когда $x$ делится на $y$ . Это значит, что доказываемое утверждение $A$ имеет вид: " $z=0 \leftrightarrow y|x$ ". Допустим, что это утверждение неверно. Это означает, что ложна одна из импликаций " $z=0\to y|x$ " или " $y|x\to z=0$ ". Предположим сначала, что ложна первая импликация " $z=0\to y|x$ ", то есть $z=0$ истинно, но $x$ на $y$ не делится. В соответствии со структурной схемой $z=0$ либо когда $x=0$ , либо когда в процессе вычитания $x-y-y-\ldots-y$ на некотором шаге получится 0. В первом случае $x$ делится на $y$ в противоречие с допущением. То же происходит и во втором случае. Если $x-y-y-\ldots-y=0$ , то $x-ny=0$ , то есть $x=ny$ для некоторого $n$ , что и означает делимость $x$ на $y$ .

Допустим теперь, что ложна вторая импликация, т.е. что $x$ делится на $y$ , но $z\ne0$ . Неравенство $z\ne0$ может иметь место в одном из следующих трех случаев:

а) при невыполнении условия $x\geqslant y$ , то есть при $x<y$ ;

б) после завершения цикла;

в) в ходе выполнения цикла.

Поскольку присваивание $z\,\colon\!=x$ при $x\ne0$ приводит к вхождению в цикл (так как из $x\ne0$ следует $x>0,\, x>0$ ), поэтому никаких других возможностей для $z\ne0$ , кроме указанных трех, на структурной схеме не существует. Рассмотрим последовательно эти три возможности:

а) если $x<y$ , то по структурной схеме $z\,\colon\!=-1$ , то есть $z\ne0$ , а значит, $x$ не делится на $y$ в противоречие с допущением;

б) если цикл завершен и $z\ne0$ , то $z<0$ . Это означает, что $x-ky<0$ , то есть $x<ky$ и $\lnot(\exists n\in \mathbb{N})(x=ny)$ . Следовательно, $x$ не делится на $y$ , что также противоречит допущению;

в) $z\ne0$ в ходе выполнения цикла. Но в этом случае мы и не требуем, чтобы был дан ответ на вопрос о делимости $x$ на $y$ . Мы рассчитываем его получить после выполнения программы, а не в ходе ее выполнения. Но только что было доказано, что если цикл завершится с $z\ne0$ , то $x$ на $y$ не делится. Здесь мы обнаруживаем, что цикл может и не завершиться, если $z$ будет оставаться положительным. Это будет происходить в том случае, когда $y=0$ и $z-0=z= x>0$ . Но так и должно быть: ведь в этом случае мы будем пытаться установить, делится ли положительное число $x$ на 0, а такая операция запрещена.

Таким образом, мы устанавливаем, что если наша программа завершится, то она решит поставленную задачу, т.е. мы доказали частичную правильность нашей программы. Чтобы сделать нашу программу тотально правильной, нужно предусмотреть ее завершение и в выявленном исключительном случае. Для этого можно, например, перед проверкой условия $x\geqslant y$ проверить утверждение " $x>0\land y=0$ ". Если оно истинно, перейти к присваиванию $z\,\colon\!-1$ , если же оно ложно — перейти к проверке $x\geqslant y$ .

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

Математический форум (помощь с решением задач, обсуждение вопросов по математике).

Если заметили ошибку, опечатку или есть предложения, напишите в комментариях.

Список статей » Список форумов

Часовой пояс: UTC + 3 часа [ Летнее время ]