Докажите, что Санта-Клаус настоящий, используя машинописный текст

Резюме

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

Предпосылка

Если это предложение верно, то Санта-Клаус настоящий.

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

Так как же работает парадокс? Рассмотрим более нормальный пример предложения формы «если А, то Б». Например, рассмотрим следующее предложение:

Если вы добавите соль и воду вместе, вы получите соленую воду

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

Круто, вернемся к исходному примеру

Если это предложение верно, то апельсины зеленые

…Достаточно близко. Чтобы доказать это утверждение, сначала мы предполагаем первый бит (предложение истинно), затем мы смотрим, сбылась ли в результате вторая часть. Мы предположили, что предложение верное, так что это будет означать… апельсины серые. Круто, мы доказали, что апельсины серые, если предложение истинно, так что это означает, что предложение истинно.

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

Карри-Ховард

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

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

// Define salt, pepper, meat, potatoes, and ducks.
type Salt = 'salt'
type Pepper = 'pepper'
type Meat = 'meat'
type Potatoes = 'potatoes'
type Duck = 'duck'
// Define Santa Claus as never existing
type SantaClaus = never;
// A type for A and B
type And<A, B> = {
    theFirstPart: A;
    theSecondPart: B;
}
// To get a christmas quacker, we need Santa Claus and a duck
type CristmasQuacker = And<SantaClaus, Duck>;
// A type for A or B
type Or<A, B> = 
    { theFirstOption: A } |
    { theSecondOption: B };
// To get seasoning we need salt or pepper
type Seasoning = Or<Salt, Pepper>
// To get a meal, we need seasoning, and either meat and potatoes
type Meal = And<Seasoning, Or<Meat, Potatoes>>;

Мы показали, что можем писать базовые операторы, содержащие And и Or. Мы также можем писать операторы, содержащие в себе «если». Логическим символом «если» является стрелка вправо (→), которая соответствует толстой стрелке (=>) в JavaScript:

// If both A and B exist, then A exists
type First = <A, B>(both: And<A, B>) => A;
// If both A and B exists, then B exists
type Second = <A, B>(both: And<A, B>) => B;

Это все хорошо, но это всего лишь определения. Возьмем для примера First. First - это предложение, в котором говорится, что если существуют и A, и B, то A существует. Однако First не является доказательством этого утверждения, это просто само это утверждение.

Чтобы доказать, что что-то верно, мы должны создать экземпляр этого типа. Вот некоторые примеры:

const saltExists: Salt = 'salt';
const pepperExists: Pepper = 'pepper';
const seasoningExists: Seasoning = {
    theSecondOption: 'pepper'
};
const mealsExist: Meal = {
    theFirstPart: seasoningExists,
    theSecondPart: { theFirstOption: 'meat' }
}
// A exists because the first part of A and B is A.
const firstIsTrue: First = (both) => both.theFirstPart;
// B exists because the second part of A and B is B.
const secondIsTrue: Second = (both) => both.theSecondPart;

Основываясь на наших определениях соли, перца, мяса и картофеля, мы доказали существование приправ, блюд! В дополнение к этому мы доказали наши First и Second предикаты сверху.

Ложь

Доказать что-то правдой - это хорошо, но что, если мы хотим доказать что-то ложное? К счастью, TypeScript предоставляет нам тип, который невозможно создать, под названием never. Этот тип иногда называют void, false или bottom. Математический символ для never - это перевернутая буква T: ⊥. Мы можем использовать «A → ⊥» (если A, то ложь), чтобы обозначить «A не существует»:

// A does not exist
type Not<A> = (false_statement: A) => never;

Теперь у нас есть все, чтобы доказать, что это неправда:

// Santa Claus does not exist because we defined him not to exist
const santaClausIsntReal: Not<SantaClaus> =
    (santaClaus) => santaClaus;
// Christmas Quackers do not exist because because the first ingredient
// of a Christmas Quacker (Santa Claus) does not exist.
const christmasQuackersArentReal: Not<ChristmasQuacker> =
    (christmasQuacker) => christmasQuacker.theFirstPart;

Мы даже можем выполнить другие доказательства, используя Not. Например, как насчет принципа взрыва, который гласит, что при противоречии мы можем доказать все, что угодно:

// A contradiction is when something is both true
// and false at the same time
type Contradiction<T> = And<T, Not<T>>;
// Lemma: given a contradiction, we can prove anything
type PrincipleOfExplosion =
    <T, U>(contra: Contradiction<T>) => U;
// ...and here's a proof:
const principleOfExplosionIsTrue: PrincipleOfExplosion =
    (contra) => contra.theSecondPart(contra.theFirstPart)

Захватывающе! Мы можем доказать основные математические теоремы, используя только TypeScript. Теперь у нас есть все необходимое, чтобы перейти к нашему парадоксу.

Парадокс карри

Нам нужен способ выразить утверждение «Если это предложение истинно, то Санта-Клаус реален» как тип. Для начала дадим предложению имя, скажем CurrysParadox.

type CurrysParadox = ??

Таким образом, мы можем переписать наше предложение, чтобы сказать: «Если CurrysParadox истинно, то Санта-Клаус реален». Мы знаем, как написать предложение с «если» в нем, и мы знаем, как написать «Санта-Клаус настоящий», поэтому теперь мы можем заполнить пробел:

type CurrysParadox =
    (paradox: CurrysParadox) => SantaClaus;

Чтобы доказать, что утверждение CurrysParadox истинно, нам нужно создать его экземпляр:

const currysParadoxIsTrue: CurrysParadox =
    (paradox) => ??

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

const currysParadoxIsTrue: CurrysParadox =
    (paradox) => paradox(paradox);

Теперь, когда мы знаем, что CurrysParadox истинно, нам нужно получить экземпляр SantaClaus, чтобы завершить доказательство. Как и выше, currysParadoxIsTrue является экземпляром CurrysParadox. Если мы сможем вызвать currysParadoxIsTrue, то в результате мы получим SantaClaus. Мы можем вызвать currysParadoxIsTrue, передав себя в качестве аргумента:

const santaClausIsReal: SantaClaus =
    currysParadoxIsTrue(currysParadoxIsTrue);

Этот тип проверяет, поэтому после запуска этого кода у нас будет экземпляр SantaClaus. Мы наконец-то доказали, что Санта-Клаус существует только на TypeScript!

Абсурд продолжается. Из принципа взрыва можно доказать что угодно, если сначала у вас будет ложное утверждение:

const anythingIsTrue: <T>() => T = santaClausIsReal;

Что?

Держать на секунду. Когда мы определяли наши типы, мы сказали, что SantaClaus равно never. Когда мы запускаем эту программу, что на самом деле сохраняется в переменной, которую мы назвали santaClausIsReal? Это число? Это функция? Удалось ли нам сохранить Деда Мороза в переменной? Запуск программы дает нам ответ:

Uncaught RangeError: Maximum call stack size exceeded

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

Итак, что случилось?

Если мы напишем currysParadoxIsTrue inline для santaClausIsReal и сократим paradox до p, мы получим следующий оператор:

(p => p(p))((p: CurrysParadox) => p(p));

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

Так как же нам примирить тот факт, что TypeScript вообще позволил нам писать такие абсурдные результаты? TypeScript сломан? Ну нет. Чтобы облегчить написание программ с циклами и другими неочевидными условиями выхода, TypeScript позволяет нам писать программы без завершения. Когда мы даем тип функции, мы объявляем, что, когда она вернется, значение будет иметь указанный тип. Если он никогда не возвращается, мы никогда не нарушаем ни одно из правил набора текста.

Вывод

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

Этот пост изначально был размещен в Блокноте Андрея

typescript Curry-Howard type theory proof Curry's paradox Functional Programming Javascript Santa Claus