Исчисления и формальные системы



Скачать 250.47 Kb.
страница1/2
Дата24.12.2012
Размер250.47 Kb.
ТипДокументы
  1   2
Хаскелл Б. Карри (Пенсильванский Государственный Университет, США)

ИСЧИСЛЕНИЯ И ФОРМАЛЬНЫЕ СИСТЕМЫ 1
В своей недавней книге Лоренцен представил представление исчисления, которое в некоторых отношениях более точно, нежели подобно предшествовавшим. Данная статья – это изучение этого представления, и его отношение к формальным системам, которые я рассматриваю в других местах. Представление неформальное, за исключением того, что в §4 есть точная теорема о символической структуре, которая включает в себя, как частный случай, теорему, в которой скобки Лукасевича могут интерпретироваться только одним путем.

ОПРЕДЕЛЕНИЕ ИСЧИСЛЕНИЯ-L1.


Основная идея Лоренца здесь будет называться исчислением-L1. Оно будет описано в терминах, которые не полностью соответствуют тем, которые использовал он сам.

Мы начнем с алфавита. Скажем, что A, которое является конечным множеством простых символов, здесь называемых буквами, называется алфавитом. Конечная последовательность букв будет называться словом. Буква и слова алфавита А иногда будут называться А-буквами и А-словами.

Кроме А-букв нам нужно добавить дополнительные буквы, которые мы назовем словами-переменными. Мы предполагаем, что они составляют алфавит Х (возможно бесконечный). Слова в алфавите будут называться А-формулами.

Задав алфавит А, исчисление-L1 К над алфавитом А определяется множеством правил, каждое из которых имеет вид:

(1) A1, …, Am |- A0

где Аi – А-формула и m>0. Правило с m=0 будет называться начальным правилом, те, у которых m>0 – производными правилами.

Если А-слова заменены на переменные в правиле, то тогда Аi сами становятся А-словами, и мы говорим, что у нас есть правило-пример. Для правила или правила-примера (1) А1,…Аm называются посылками, а А0 – заключением. Заключение начального правила-примера будет называться начальным словом исчисления К.

Правила, интерпретированные как индуктивное определение класса А-слов, называются тезисами над К или К-тезисами. Используя терминологию Клини это индуктивное определение есть следующее:

  • (базисный шаг) каждое начальное слово над К – тезис.

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

Согласно этому индуктивному определению, существуют различные техники построения доказательства, что А-слово – это К-тезис. Лоренцен рассмотрел одну очень подробно.
Однако, нет необходимости рассматривать его здесь.

Если А – конечный алфавит (т. е. с конечным числом букв) и число правил (1) – конечно, то будем говорить, что исчисление имеет конечный базис, иначе оно имеет бесконечный базис. Лоренцен рассматривает, по крайней мере исключительно в основной части книги по логике, только исчисления с конечным базисом. С точки зрения основы – это рациональная процедура, в самом деле, исчисление с бесконечным базисом может быть рассмотрено только тогда, когда оно базируется на более фундаментальном с конечным базисом. Тем не менее, для многих целей ограничение на конечность базиса – неуместно, т.к. после того, как бесконечный случай может быть сведен к конечному, возникает необходимость в проведении обобщения.

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

В другом рассмотрении переменные – это символы, которые используются также и в У-языке. Поэтому они есть то, что я называл в других места У-переменными. Как уже было отмечено они – основа для неопределенных А-слов. Таким образом, символ «|-» рассматривается принадлежащим У-языку, и играет роль глагола. Если мы возьмем «|-» как префикс, выражающий «есть К-тезис», тогда мы можем рассматривать правила (1) как аббревиатуру для:

«Если А1, …, Аm – А-слова такие, что |-A1, …|-Am, тогда |-A0». (2)

Так (1) определяется в терминах предикатов.
2.Обобщения. Представление L1-исчисления допускает различные обобщения. Мы рассмотрим некоторые из них.

Одно такое обобщение было рассмотрено Лоренценом. Пусть К1 является L1-исчислением в алфавите А. Тогда мы можем сформировать второе исчисление К2, как и в §1, за исключением того, что в правилах (1) мы допускаем второй тип переменных, называемых К1-переменными, на которые может быть заменен произвольный К1-тезис. Лоренцен называет эти новые переменные переменные-объекты.

Это предполагает дальнейшее обобщение. Предположим, что мы рассмотрели множество исчислений К0,…, Кr, каждое из которых – множество правил (1). Каждому Кj поставлено в соответствие тип переменных названных Кj-переменные и пусть правила содержат переменные любого или всех типов. Если «|-» в Кj интерпретируется как «есть Кj-тезис» и правила интерпретируются как в (2), которые понимаются так, что произвольный Кj-тезис может быть заменен на Кj-переменные, тогда правила формируют индуктивное определение для всех Кi-тезисов одновременно. Мы назовем такие системы композиционным исчислением ранга r. Кj называются компоненционные подисчислениями.

Если мы предположим такие компоненционные подисчисления, тогда представление слова-переменного становится излишним. Если А – алфавит а1, а2, …, то А-слова определяют тезисы в исчислении, К0 – следующим образом:

«|-аi»

«х|-хаi» i=1,2,3,… (3)

Здесь переменная распространяется над К0-тезисом. Мы, затем, потребуем как часть определения композиционного исчисления ранга r, чтобы переменные, которые получаются, были только Кj-переменными для j=0, 1, …, r. Тогда L1-исчисление над А есть композиционное исчисление ранка 1, не содержащее К1-переменных и содержащее такие, как К1 специальной формы (2).

Особый интерес представляет случай r=0. Такие исчисления я буду называть L0-исчисления. В них есть только один тип переменных, Лоренцен называет их собственными переменными, в данной терминологии – это К0-переменные. Также, их можно называть переменные-тезисы. Исчисление с правилами (3) – L0-исчисление, тезисы – А-слова.

Многие интересные случаи удовлетворяют следующему дополнительному условию: любое Кs для sj-переменные для jj для j
Нет необходимости в том, чтобы все Кj имели один алфавит А, но не будет потери общности в предположении о том, что алфавит один, после того, как А станет объединением алфавитов всех Кj.

Композиционное исчисление не представляет наибольшую полученную индукцией систему, базирующуюся на словах алфавита. Оно имеет две особенности. Во-первых, существенно то, что оно определяет множество размерности r+1 унарных предикатов, где у нас может быть система, определяющая отношения и предикаты произвольной степени. Во-вторых, ограничение на то, что правила имеют вид (1), где Аi – формула, довольно строгое, оно может исключить правила, которые индуктивно определяют слова или последовательности слов, и которые не из типа слов Аi. Термин «сентенциальная система» используется здесь для обобщений данного сорта. Исключительное требование, чтобы предположительное доказательство того, что слово есть тезис такого и только такого типа или, что некоторые специальные отношения содержатся между заданными словами, может быть эффективно проверено.

Композиционное исчисление ранга r можно всегда свести к L1-исчислению. В самом деле, пусть А – алфавит исчисления. И пусть t0, t1,… есть буквы, определенные для каждой отдельно из всех букв алфавита А. Для каждого правила (1) из Кj формируется правило:

tjA1, tjA2, …, tjAm |-tjA0 (4)

и затем, для каждой Kj-переменной, которая появляется, ставим х и добавляем посылку tj к х. Переменные могут быть взяты как слова-переменные. Если так поступают, то тезисы полученного исчисления К1 есть точно слова вида tjВ (j=1,…,r), где В – Кj-тезис.

Эта редукция аналогична редукции формальной системы к логике, и имеет те же преимущества. Она может быть расширена так, что позволяет нам формулировать отношения между словами, классы которых формируют свободные вхождения переменной, в большинстве случаев, tj (и Кj-тезиса). Иногда выгодно опускать tj и рассматривать tr. Однако, для многих целей формулировка композиционного исчисления гораздо более естественна.

Слова-переменные, возникающие в подобных процессах, могут быть сформулированы как L1-исчисление К0 в виде (3), которое гораздо менее обширнее, чем исходное. Таким образом, удобно расширить термин «L1-исчисление», включив все исчисления ранга 1 без К1-переменных. Когда К0-тезисы включают все слова в алфавите, исчисление будет называться пантактическим, когда К0-тезисы – подклассы этих слов , они будут называться хорошо сформированные слова (хсс) и исчисление будет называться еутактическим. Когда композиционное исчисление сведено к L1-исчислению, мы используем термины относящиеся к исходному алфавиту, и нет необходимости в явном включении букв t1,…,tr в хсс.
3.Примеры. Следующие примеры иллюстрируют принципы, рассмотренные в §2. В них мы используем буквы «x, y, z, u, v, w» в качестве переменных. Мы используем верхний индекс, где необходимо пометить компоненционные исчисления, т. е. верхний индекс j помечает переменную как Кj-переменную. Где верхних индексов нет, то там переменные считаются К0-переменными. Мы также рассматриваем верхний индекс у «|-» в порядке устранения окончательных возможностей для сомнения.

Пример 1. Классическая пропозициональная алгебра Черча.

Алфавит: (, ), =>, , p1, p2, …

K0 (предположения):

|-0pi

x, y |-0(x=>y)

x |-0(x)

K1 (утверждения):

|-1(x=>(y=>x))

|-1((x=>(y=>z))=>((x=>y)=>(x=>z)))

|-1(((x)=>(y))=>(x=>y))

(x=>y), x |-1y
Пример 2. Пример 1 сформулирован в бесконечном базисе. Но легко переформулировать его в конечном базисе.

Алфавит: (,), =>, , p, a.

K0 (переменные)

|-0p

x |-1xa

K1 (предположения)

|-1x0

x1, y1 |-1(x1 =>y1)

x1 |-1 (x1)

K2 (утверждения)

|-2 (x1=> (y1 =>x1))

|-2 ((x1=> (y1=>z1))=>((x1=>y1)=>(x1 =>z1)))

|-2 (((x1)=> (y1))=>(x1=>y1))

x1 =>y1, x1 |-2 y1
Пример 3. Следующая переформулировка примера 2 как L0-исчисления иллюстрирует технику, описанную в конце §2.

Алфавит: (, 0, , =>, p, a, V, P, T

K0

как в (3) для алфавита примера 2.

K1

|-Vp

Vx |-Vxa

Vx |- Px

Px, Py |- P(x=>y)

Px |- P(x)

Px, Py |-T(x=>(y=>x))

Px, Py, Pz |- T((x=>(y=>z))=>(x=>y)=>(x=>z))

Px, Py |- T(((x)=.(y))=>(x=>y))

T(x=>y), Tx |- Ty
Пример 4. Префиксное представление Лукасевича

Алфавит: две бесконечные последовательности

e1, e2, …

f1, f2, …

K0

|-ei

x1, …, xnk |- fkx1x2…xnk.

Где целое nk, связанное с fk, мы называем степенью fk.
Пример 5. Предположим, что в Примере 4 бесконечно много ei, и для каждого положительного целого n существует бесконечно много fk степени n. Пусть mk – число fi для ik таких, что ni=nk. Пусть алфавит В состоит из двух букв a и b, и пусть алфавит А – алфавит из примера 4. Если r – целое положительное, ar обозначает последовательность из r штук букв а. Тогда мы можем перевести слово из алфавита А в слово из алфавита В следующим образом:

ei bai

fk  |-1 bbankbamk
Затем мы можем решить, какие В-слова есть переводы А-слов, и если А-слово существует, то оно определяется однозначно. В-слова, котороые являются переводом тезисов примера 4, есть точно К2-тезисы следующего градуированного исчисления ранга 2 в алфавите В:

K0: cлова, начинающиеся с b

|-0 b

x |-0xa

x |-0 xb
K1 (атомы):

|-1 ba

x |-1 xa
K2 (xcc):

|-2 x1

x |-2 bbay1x

x, by1z |-2 by1azx
Пример 6. (представление Геделя). В примере 5 мы перевели пример 4 в алфавит, состоящий из двух символов. Перевод в алфавит с одним символом может быть рассмотрен по методу Геделя. Если С – алфавит, состоящий из одного символа с, то С-слова могут различаться только числом вхождений с, следовательно, могут ввести взаимно однозначное соответствие между С-словами и натуральными числами. Используя обычные арифметические представления для таких чисел, мы можем перевести из слова алфавита А (пример 4) в алфавит С следующим образом

ei  2i+1 i=1, 2, …

fk 2nk3mk k=1, 2, …

где nk и mk такие же, что и в примере 5. Это предполагает следующие правила, где n=nk, m=mk, pj - это j-ый штрих:

K0:

|-0 c

x |-0 xc1

K1:

|-1 2i+1

x1, …,xn |-1 2n 3m p3x1, …, pn+2xn
Тем не менее, это система не подходит под наше определение исчисления, т. к. второе правило К1 не С-формула. Однако, это правило конструктивно в том смысле, что задав любые С-формулы х1,…, хn, заключение конструктивно определяет С-слово. Таким образом, мы имеем сентенциальную форму, которая не является исчислением. У этой системы есть свойство, что она разрешима даже, если С-слово не К-тезис, если же – это К-тезис, то оно соответствует единственному тезису примера 4. Эта система может быть переведена в исчисление добавлением дополнительных букв, но тогда она не будет иметь преимуществ перед примером 5.

В общем случае правил в К1 будет бесконечно много. Но число букв в А – конечно, также конечно и число правил. Но в этом случае достаточно более простого представления. Если в алфавите А числу букв q, то А-слово можно рассматривать как q-ичную систему. Опять же, если есть конечный предел n последовательности {nk}, то мы можем заменить различие в терминах в основном продукте на другое в терминах перенумерации всех n-кратных. Если таким образом получается функция Jn, то мы можем заменить правила К1 на следующие:

|-1Jn+1(0, i, 0, …, 0)

x1, …, xnk |-1Jn+1(k, x1, …, xnk, 0, …, 0)
Пример 7. Следующая формулировка теории Черча о -обращениях – пример сентенциальной системы, которая не является исчислением. Алфавит состоит из четырех букв: е, а, *, . Предикаты состоят из двух унарных префиксов V, W; одного кватернарного префикса S; и семи бинарных инфиксов L, J, F, F’, B, B’, =. Их интерпретация дается ниже, заключения в скобках понимается как предположения.

Vx х - переменная

Wx х - хсс

Sxyzu замена у на х в z дает u (Vx, Wy, Wz, Wu)

хLy х предшествует у в списке переменных (Vx, Vy)

хJy х и у есть определенные переменные (Vx, Vy)

xFy х свободен в у (Vx, Wy)

xF’y x не свободен в y (Vx, Wy)

xBy x предел y (Vx, Wy)

xB’y x не является пределом y (Vx, Wy)

x=y x переводится в y (Wx, Wy)
Система, в том виде как она здесь сформулирована, предполагает пантактическое исчисление К0 как в (3). Из-за своей сложности, правила имеют названия и классификацию, представленную ниже:
Переменные

V1 Ve

V2 VxVxa
ХСС

W1 VxWx

W2 Wx, Wy W*xy

W3 Vx, WyWxy
Определение переменных

L1 VxxLxa

L2 xLyxLya

J1 xLyxJy

J2 xJyyJx
Свободные переменные

F1 VxxFx

F2 xFy, Wz xF*yz

F3 xFy, WzxF*zy

F4 xFy, xJzxFxy

F’1 xJy xF’y

F’2 xF’y, xF’zxF’*yz

F’3 Vx, Wx xF’xy

F’4 xF’y, VzxF’zy
Предельные переменные

B1 Vx, WyxBxy

B2 xBy, WzxB*yz

B3 xBy, WzxB*zy

B4 xBy, VzxBzy

B’1 Vx, VyxB’y

B’2 xB’y, xB’zxB’*yz

B’3 xB’y, xJzxB’zy
Замена

S1 Vx, WySxyxy

S2 Vx, Vy, xJy, WuSxuyy

S3 Sxuvw, SuyzSxu*vy*wz

S4 Vx, Wu, WvSxuxvxv

S5 Sxuvw, xJy, yF’uSxuyvyw

S6 Sxuvw, xJy, xF’vSxuyvyw
Обращения

 Wxx=x

 x=yy=x

 x=y, y=zx=z

 x=y, Wz*zx=*zy

 x=y, Wz*xz=*yz

 Vx, y=zxy=xz

 Vx, Vy, Sxyuv, yF'uxu=yv

 Sxuyz*xyu=z

  • Wy, xF'yx*yx=y

  1   2

Похожие:

Исчисления и формальные системы iconЛекция 4 Исчисления. Формальные системы. Формальные грамматики. Автоматы
...
Исчисления и формальные системы iconЛекция 3 Исчисления. Формальные системы. Формальные грамматики. Автоматы
...
Исчисления и формальные системы iconЭквивалентность двух определений элементарной формальной системы
«Исчисления и формальные системы» (стр. 267) и «Основания математической логики» (стр. 68). Ясно, что эти два определения в некотором...
Исчисления и формальные системы icon4. Введение в формальные (аксиоматические) системы 1 Формальные модели
Принципы построения формальных теорий. Аксиоматические системы, формальный вывод
Исчисления и формальные системы iconМетоды представления знаний Формальные языки и формальные системы
Естественный язык: достоинства (и они же недостатки): неполнота, избыточность, неоднозначность
Исчисления и формальные системы icon1Реляционные исчисления
Иначе говоря алгебра имеет процедурный характер, а исчисления не процедурный. Но на самом деле упомянутые отличия существуют только...
Исчисления и формальные системы iconРабочая программа дисциплины "Математика". Направление подготовки 270800 "Строительство"
Дисциплина “Математика” обеспечивает подготовку по следующим разделам математики: линейной алгебры и аналитической геометрии, метричного...
Исчисления и формальные системы iconРабочая программа дисциплины теория автоматов и формальных языков направление подготовки
Уметь: строить формальные грамматики, деревья вывода, распознающие автоматы; анализировать формальные языки
Исчисления и формальные системы iconФормальные модели программных агентов в задаче семантического индексирования документов
В работе рассматриваются формальные модели делиберативных агентов, т е агентов базирующихся на базируется на принципах и методах...
Исчисления и формальные системы iconСоставляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы
Формальные системы (ФС) – это совокупность чисто абстрактных объектов, не связанных с внешним миром, в котором представлены правила...
Разместите кнопку на своём сайте:
ru.convdocs.org


База данных защищена авторским правом ©ru.convdocs.org 2016
обратиться к администрации
ru.convdocs.org