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-17 12:15 pm (UTC)просто полюбоваться фотографией типизированной лямбды в конце
Это что, у меня есть фотография монады.
no subject
Date: 2010-05-17 03:16 pm (UTC)no subject
Date: 2010-05-17 09:38 pm (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)Я в этих тонкостях не разбираюсь.