Propositional Calculus
May. 13th, 2010 05:41 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
thedeemonДля многих моих френдов описанное в этом посте - детский сад, поэтому они могут смело пропустить текст и просто полюбоваться фотографией типизированной лямбды в конце. Я же с данной темой познакомился недавно, мне было интересно, возможно кому-то еще будет тоже. Недавно я писал про логику высказываний и ее параллели в программировании. Но там связи этих двух областей были неформальные, на уровне аналогий. Оказывается, до их формализации был всего один шаг.
Пусть мы оперируем некоторыми высказываниями A,B,C и т.д. Пусть у нас есть доказательство a достоверности высказывания А. Этот факт будем обозначать как a : А.
Пусть теперь у нас есть два высказывания вместе с их доказательствами: a : A и b : B. Тогда мы можем вывести достоверность высказывания A & B, его доказательством будет пара (a,b). Т.е. (a,b) : A & B. Это правило ввода конъюнкции.
Обратным для этого правила будет правило избавления от конъюнкции. Если у нас есть высказывание A & B и его доказательство p, то мы можем вывести достоверность высказывания А и высказывания В. Их доказательствами будут fst p и snd p, т.е. fst p : A и snd p : B. Кроме того, можно описать правило упрощения такого доказательства: fst (a,b) --> a и snd (a,b) --> b. Т.е. более сложное доказательство можно заменить более простым.
Если мы из высказывания А с его доказательством a можем каким-то образом (следуя правилам) получить высказывание В с его доказательством b, то из этого факта мы можем вывести достоверность высказывания A => B. Его доказательство запишем как λa.b или (λa:А).b. Здесь из произвольного доказательства a высказывания А строится доказательство b высказывания В. А вся конструкция доказывает A => B. Это правило ввода импликации. Популярна нотация, где исходные факты записываются над горизонтальной чертой, а то, что из них выводится, - под чертой. Запись данного правила в такой нотации можно внезапно обнаружить на юзерпике![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif)
deni_ok:
Первая строчка в квадратных скобках, потому что это допущение, а не утверждение. Для достоверности импликации достаточно умения построить доказательство В из доказательства А, достоверность самого А не требуется.
Обратное правило - избавление от импликации. Если у нас есть доказательство f высказывания A => B и доказательство a высказывания А, то из этого можно вывести достоверность высказывания В, его доказательством будет применение нашего умения строить из А В. Запишем это применение как f a. Оно дает доказательство В, поэтому (f a) : B. Для него есть правило упрощения:
(λx.e) a --> e[a/x]
Если f имеет форму λx.e, то (f a) можно заменить на e, где вместо каждого свободного вхождения x (т.е. не связанного лямбдой внутри e) стоит a.
Дальше, если у нас есть доказательство a высказывания А или доказательство b высказывания B, то мы можем вывести достоверность высказывания A | B. Его доказательством будет пара из имеющегося у нас доказательства и тэга, говорящего, которое из этих двух доказательств у нас есть. Обозначим их как Left a и Right b. Это правило ввода дизъюнкции.
Правило избавления от дизъюнкции: если у нас есть доказательство р высказывания A | B, а также доказательства f : A=>C и g : B=>C, то из них мы можем вывести достоверность С. Его доказательство запишем как cases p f g. Его смысл в том, чтобы посмотреть которое из двух высказываний (А или В) имеется в р и применить одну из импликаций. Для такого доказательства тоже есть правило упрощения:
cases (Left a) f g --> f a
cases (Right b) f g --> g b
В систему также вводится высказвание ⊥, означающее противоречие, абсурд. Для него нет правила ввода, т.к. мы не можем (и не должны мочь) конструктивно его доказать. Зато есть правило избавления: если вдруг каким-то образом у нас появилось доказательство р : ⊥, то вся наша система должна порушиться, а из доказательства абсурда мы можем вывести все, что угодно. Записывается это как (abortA p) : A.
Отрицание определяется следующим образом: -А = А => ⊥.
Что все это дает? Возможность конструктивно строить доказательства разных утверждений.
Пример 1. Эквивалентность (A & B) => C и A => (B => C).
Высказвания эквивалентны, когда следуют друг из друга. Сперва докажем в одну сторону:
((A & B) => C) => (A => (B => C))
Самая внешняя связка - импликация, поэтому доказательством будет лямбда: λf.e, где
f : (A & B) => C и e : A => (B => C).
По правилу избавления от импликации, если (a,b) : A & B, то (f (a,b)) : C.
Тогда ((λa:A) . (λb:B). f (a,b)) : A => (B => C), а значит
(λf : (A & B) => C) . (λa:A) . (λb:B). f (a,b)
и есть искомое доказательство.
Теперь в обратную сторону:
(A => (B => C)) => ((A & B) => C)
Опять лямбда λf.e, где
f : A => (B => C)
e : (A & B) => C
Если a:A и b:B, то (f a) : B => C и ((f a) b) : C.
Значит, e = (λp: A & B). (f (fst p)) (snd p), и искомое доказательство:
(λf : A => (B => C)) . (λp: A & B). (f (fst p)) (snd p)
Пример 2. A => --A.
По определению отрицания -A = A => ⊥, а значит --A = (A => ⊥) => ⊥.
Нам нужно построить доказательство вида (λa:A) . f, где f : (A => ⊥) => ⊥.
Если n : A => ⊥ и а : А, то (n a) : ⊥.
Тогда f = (λn : A => ⊥) . n a, и все доказательство:
(λa:A) . (λn : A => ⊥) . n a
Можно ли доказать обратное (--A => A)? Для этого нам потребуется построить лямбду, которая бы из доказательства f : (A => ⊥) => ⊥ строила бы доказательство а : А. Чтобы применить f, нужно конструктивное доказательство A => ⊥, но т.к. у нас нет правила ввода ⊥, его взять неоткуда. Поэтому доказать исходное высказывание не получится. А значит, логика здесь получилась не классическая (двойное отрицание не означает утверждения), и совсем не булева.
Пример 3.
В предыдущем посте на эту тему говорилось об эквивалентности A=>B и -(A & -B). В классической логике они эквивалентны, а можно ли доказать их эквивалентность в данной системе? Сперва в одну сторону:
(A=>B) => -(A & -B)
т.е. (A=>B) => ((A & (B=>⊥)) => ⊥)
Опять доказательством будет λf.e, где
f : A=>B
e : (A & (B=>⊥)) => ⊥
Заметим, что если a : A и n : B=>⊥, то (f a) : B и (n (f a)) : ⊥.
Тогда e = (λp : A & (B=>⊥)). (snd p) (f (fst p)), и все доказательство:
(λf:A=>B) . (λp : A & (B=>⊥)). (snd p) (f (fst p))
Чтобы доказать в обратную сторону, нужно уметь из доказательства -(A & -B) получить доказательство A=>B. Первое есть импликация, избавиться от которой опять не получается, т.к. неоткуда взять аргумент. Поэтому в данной системе A=>B и -(A & -B) не эквивалентны, но по крайней мере из первого следует второе.
Пример 4. -A | B => (A => B)
Опять импликация, (λp : -A | B). f, где f : A => B.
Мы знаем, что p содержит либо доказательство -А, либо доказательство В. Проведем анализ вариантов:
f = cases p g h
g : -A => (A => B)
h : B => (A => B)
Построить h совсем просто: (λb:B) . (λa:A) . b.
А вот с g интересней.
g = (λn: -A) . (λa:A) . abortB(n a)
Имея доказательство a:A и доказательство n : -A, мы можем получить доказательство (n a) : ⊥ (противоречие). А из него по правилу для ⊥ мы можем получить все, что угодно, например, доказательство В. В итоге все доказательство выглядит так:
(λp : -A | B). cases p ((λn:-A).(λa:A).abortB(n a)) ((λb:B).(λa:A).b)
Такой трюк с извлечением доказательства из противоречия, вроде, вполне вписывается в систему, но мне кажется каким-то жульничеством. Если кто прояснит этот момент, буду признателен.
Везде выше мы говорили о высказываниях и доказательствах, но в приведенных правилах и формулах, я думаю, все уже узнали вариант типизированного лямбда-исчисления.
Действительно, из данной логической системы получается типизированное лямбда-исчисление простой заменой наименований: высказывания назовем типами, доказательства - термами (объектами), конъюнкцию - product type (tuple), дизъюнкцию - sum type, импликацию - функциональным типом, а правила упрощения - правилами вычисления. При этом первый пример дает нам карринг. Вот такой изоморфизм сами знаете кого.
Пусть мы оперируем некоторыми высказываниями A,B,C и т.д. Пусть у нас есть доказательство a достоверности высказывания А. Этот факт будем обозначать как a : А.
Пусть теперь у нас есть два высказывания вместе с их доказательствами: a : A и b : B. Тогда мы можем вывести достоверность высказывания A & B, его доказательством будет пара (a,b). Т.е. (a,b) : A & B. Это правило ввода конъюнкции.
Обратным для этого правила будет правило избавления от конъюнкции. Если у нас есть высказывание A & B и его доказательство p, то мы можем вывести достоверность высказывания А и высказывания В. Их доказательствами будут fst p и snd p, т.е. fst p : A и snd p : B. Кроме того, можно описать правило упрощения такого доказательства: fst (a,b) --> a и snd (a,b) --> b. Т.е. более сложное доказательство можно заменить более простым.
Если мы из высказывания А с его доказательством a можем каким-то образом (следуя правилам) получить высказывание В с его доказательством b, то из этого факта мы можем вывести достоверность высказывания A => B. Его доказательство запишем как λa.b или (λa:А).b. Здесь из произвольного доказательства a высказывания А строится доказательство b высказывания В. А вся конструкция доказывает A => B. Это правило ввода импликации. Популярна нотация, где исходные факты записываются над горизонтальной чертой, а то, что из них выводится, - под чертой. Запись данного правила в такой нотации можно внезапно обнаружить на юзерпике
deni_ok:Первая строчка в квадратных скобках, потому что это допущение, а не утверждение. Для достоверности импликации достаточно умения построить доказательство В из доказательства А, достоверность самого А не требуется.
Обратное правило - избавление от импликации. Если у нас есть доказательство f высказывания A => B и доказательство a высказывания А, то из этого можно вывести достоверность высказывания В, его доказательством будет применение нашего умения строить из А В. Запишем это применение как f a. Оно дает доказательство В, поэтому (f a) : B. Для него есть правило упрощения:
(λx.e) a --> e[a/x]
Если f имеет форму λx.e, то (f a) можно заменить на e, где вместо каждого свободного вхождения x (т.е. не связанного лямбдой внутри e) стоит a.
Дальше, если у нас есть доказательство a высказывания А или доказательство b высказывания B, то мы можем вывести достоверность высказывания A | B. Его доказательством будет пара из имеющегося у нас доказательства и тэга, говорящего, которое из этих двух доказательств у нас есть. Обозначим их как Left a и Right b. Это правило ввода дизъюнкции.
Правило избавления от дизъюнкции: если у нас есть доказательство р высказывания A | B, а также доказательства f : A=>C и g : B=>C, то из них мы можем вывести достоверность С. Его доказательство запишем как cases p f g. Его смысл в том, чтобы посмотреть которое из двух высказываний (А или В) имеется в р и применить одну из импликаций. Для такого доказательства тоже есть правило упрощения:
cases (Left a) f g --> f a
cases (Right b) f g --> g b
В систему также вводится высказвание ⊥, означающее противоречие, абсурд. Для него нет правила ввода, т.к. мы не можем (и не должны мочь) конструктивно его доказать. Зато есть правило избавления: если вдруг каким-то образом у нас появилось доказательство р : ⊥, то вся наша система должна порушиться, а из доказательства абсурда мы можем вывести все, что угодно. Записывается это как (abortA p) : A.
Отрицание определяется следующим образом: -А = А => ⊥.
Что все это дает? Возможность конструктивно строить доказательства разных утверждений.
Пример 1. Эквивалентность (A & B) => C и A => (B => C).
Высказвания эквивалентны, когда следуют друг из друга. Сперва докажем в одну сторону:
((A & B) => C) => (A => (B => C))
Самая внешняя связка - импликация, поэтому доказательством будет лямбда: λf.e, где
f : (A & B) => C и e : A => (B => C).
По правилу избавления от импликации, если (a,b) : A & B, то (f (a,b)) : C.
Тогда ((λa:A) . (λb:B). f (a,b)) : A => (B => C), а значит
(λf : (A & B) => C) . (λa:A) . (λb:B). f (a,b)
и есть искомое доказательство.
Теперь в обратную сторону:
(A => (B => C)) => ((A & B) => C)
Опять лямбда λf.e, где
f : A => (B => C)
e : (A & B) => C
Если a:A и b:B, то (f a) : B => C и ((f a) b) : C.
Значит, e = (λp: A & B). (f (fst p)) (snd p), и искомое доказательство:
(λf : A => (B => C)) . (λp: A & B). (f (fst p)) (snd p)
Пример 2. A => --A.
По определению отрицания -A = A => ⊥, а значит --A = (A => ⊥) => ⊥.
Нам нужно построить доказательство вида (λa:A) . f, где f : (A => ⊥) => ⊥.
Если n : A => ⊥ и а : А, то (n a) : ⊥.
Тогда f = (λn : A => ⊥) . n a, и все доказательство:
(λa:A) . (λn : A => ⊥) . n a
Можно ли доказать обратное (--A => A)? Для этого нам потребуется построить лямбду, которая бы из доказательства f : (A => ⊥) => ⊥ строила бы доказательство а : А. Чтобы применить f, нужно конструктивное доказательство A => ⊥, но т.к. у нас нет правила ввода ⊥, его взять неоткуда. Поэтому доказать исходное высказывание не получится. А значит, логика здесь получилась не классическая (двойное отрицание не означает утверждения), и совсем не булева.
Пример 3.
В предыдущем посте на эту тему говорилось об эквивалентности A=>B и -(A & -B). В классической логике они эквивалентны, а можно ли доказать их эквивалентность в данной системе? Сперва в одну сторону:
(A=>B) => -(A & -B)
т.е. (A=>B) => ((A & (B=>⊥)) => ⊥)
Опять доказательством будет λf.e, где
f : A=>B
e : (A & (B=>⊥)) => ⊥
Заметим, что если a : A и n : B=>⊥, то (f a) : B и (n (f a)) : ⊥.
Тогда e = (λp : A & (B=>⊥)). (snd p) (f (fst p)), и все доказательство:
(λf:A=>B) . (λp : A & (B=>⊥)). (snd p) (f (fst p))
Чтобы доказать в обратную сторону, нужно уметь из доказательства -(A & -B) получить доказательство A=>B. Первое есть импликация, избавиться от которой опять не получается, т.к. неоткуда взять аргумент. Поэтому в данной системе A=>B и -(A & -B) не эквивалентны, но по крайней мере из первого следует второе.
Пример 4. -A | B => (A => B)
Опять импликация, (λp : -A | B). f, где f : A => B.
Мы знаем, что p содержит либо доказательство -А, либо доказательство В. Проведем анализ вариантов:
f = cases p g h
g : -A => (A => B)
h : B => (A => B)
Построить h совсем просто: (λb:B) . (λa:A) . b.
А вот с g интересней.
g = (λn: -A) . (λa:A) . abortB(n a)
Имея доказательство a:A и доказательство n : -A, мы можем получить доказательство (n a) : ⊥ (противоречие). А из него по правилу для ⊥ мы можем получить все, что угодно, например, доказательство В. В итоге все доказательство выглядит так:
(λp : -A | B). cases p ((λn:-A).(λa:A).abortB(n a)) ((λb:B).(λa:A).b)
Такой трюк с извлечением доказательства из противоречия, вроде, вполне вписывается в систему, но мне кажется каким-то жульничеством. Если кто прояснит этот момент, буду признателен.
Везде выше мы говорили о высказываниях и доказательствах, но в приведенных правилах и формулах, я думаю, все уже узнали вариант типизированного лямбда-исчисления.
Действительно, из данной логической системы получается типизированное лямбда-исчисление простой заменой наименований: высказывания назовем типами, доказательства - термами (объектами), конъюнкцию - product type (tuple), дизъюнкцию - sum type, импликацию - функциональным типом, а правила упрощения - правилами вычисления. При этом первый пример дает нам карринг. Вот такой изоморфизм сами знаете кого.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2010-05-13 03:14 pm (UTC)M:σ _____________________ (Λ α . M):(∀α . σ)M:(∀α . σ) __________________ (M τ):σ[α:=τ]После чего все остальные логические связки выражаются так
То есть ⊥ вводится как ненаселённый тип ∀α . α и, соответственно, операционные проблемы с abort решаются чисто синтаксически.
Введение ¬. Тип
Терм этого типа
Это даёт доказательство приведением к нелепости — reductio ad absurdum.
Удаление ¬. Тип
Терм этого типа
Из противоречия следует все что угодно.
no subject
Date: 2010-05-13 03:18 pm (UTC)no subject
Date: 2010-05-13 03:50 pm (UTC)no subject
Date: 2010-05-13 11:46 pm (UTC)Anyway, интересно, спасибо! Ещё один взгляд на (как мне кажется) одну и ту же вещь.
no subject
Date: 2010-05-15 07:40 pm (UTC)no subject
Date: 2010-05-17 12:15 pm (UTC)просто полюбоваться фотографией типизированной лямбды в конце
Это что, у меня есть фотография монады.
no subject
Date: 2010-05-17 12:25 pm (UTC)Суть в том, что у дизъюнкции два конструктора данных, а у абсурда ноль. Поэтому abort и cases являются частными случаями pattern matching. Поскольку у abort ноль конструкторов данных, то pattern matching содержит ноль веток. Поскольку тип pattern matching определяется типом веток, то тип abort не зависит ни от чего, то есть произвольный.
Похоже, это известные грабли. Есть упоминание в исторических трудах:
Наверное, с «из абсурда следует что угодно» надо смириться как с тем, что Земля круглая или теорией относительности. :)
Вот ещё один повод помедитировать. В GHCi:
Получаем доказательство произвольного высказывания, то есть тривиальную логическую теорию.
no subject
Date: 2010-05-17 03:16 pm (UTC)no subject
Date: 2010-05-17 05:38 pm (UTC)no subject
Date: 2010-05-17 07:08 pm (UTC)no subject
Date: 2010-05-17 09:38 pm (UTC)Допустим сказано, что длина списка не равна нулю. Вы делаете pattern matching списка и первая ветка соответствует пустому списку. Длина пустого списка равна нулю. Следовательно, ноль не равен нулю. Отсюда следует ⊥. Значит, в первой ветке никакого кода писать не нужно.
Таким образом на практике используется этот ⊥.
no subject
Date: 2010-05-17 09:38 pm (UTC)no subject
Date: 2010-05-17 09:42 pm (UTC)no subject
Date: 2010-05-18 03:21 am (UTC)no subject
Date: 2010-05-18 03:23 am (UTC)Это я почитываю Simon Thompson "Type Theory & Functional
Programming".
no subject
Date: 2010-05-18 09:50 am (UTC)Я в этих тонкостях не разбираюсь.