Моделирование логических схем посредством теории множеств

Автор: Чечулин Виктор Львович

Журнал: Вестник Пермского университета. Математика. Механика. Информатика @vestnik-psu-mmi

Рубрика: Математика

Статья в выпуске: 1 (9), 2012 года.

Бесплатный доступ

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

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

Короткий адрес: https://sciup.org/14729765

IDR: 14729765

Текст научной статьи Моделирование логических схем посредством теории множеств

В теории множеств с самопринадлежно-стью [1] была построена адекватная модельная область для лямбда-исчисления [2, 3], а также модель логики высказываний [2]. Кроме того, в семантике самопринадлежности были доказаны теоремы о непротиворечивости лямбда-исчисления [4]. Эти результаты позволяют моделировать посредством теории множеств логические схемы, с обоснованием того, что эти модели непротиворечивы. Ниже описан способ и примеры моделирования логических схем 1 .

1.    Обоснование моделирования

Теорема о непротиворечивости лямбда-исчисления доказана в слабой (для модельной области лямбда-исчисления) и сильной (на всем М) форме [4]. Для моделирования логических схем значима вторая (сильная) форма теоремы.

Теорема 1 (сильная непротиворечивость). Лямбда-исчисление, реализуемое на теории множеств с самопринадлежностью, – непротиворечиво.

Схема доказательства такова, что "сильное" доказательство непротиворечивости лямбда-исчисления не использует понятия модельной области (т. е. не зависит от результатов теоремы о слабой непротиворечивости). Рассматривается множество всех множеств М. Множества в нём выделяются схемой свёртывания А = {x e M | (x e0 ) или L(x)}. Если высказывание L дополнить лямбда-абстрактором и внешней по отношению к свертыванию переменной, то имеется реализация лямбда-исчисления в теории множеств

А(у) = {x e M | (x e0 ) или Lz(x, Ху.у)}(у), где y e M.

При этом по теореме о непротиворечивости теории множеств [1] высказывание L λ (х, y) не может задавать одновременно множество A(y) и его дополнение, – таким образом, совокупность высказываний L λ (х, y) (для произвольных y из М) – непротиворечива, это и доказывает теорему. □

1 Первоначальные рукописные наброски этой работы относятся к зиме 1996-1997 гг.

Теорема 1 позволяет рассматривать в качестве выражений L(.) с внешней переменной не только произвольные лямбда-выражения, но и выражения, относящиеся к логике высказываний, для которой имеются модели в теории множеств с самопринадлеж-ностью, см. табл. 1, 2.

Таблица 1. Сопоставление элементов теорий [ 2 ]

Элемент теории

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

Исчисление высказываний

Константа "невыполнимость"

0

0

Константа "выполнимость"

М

1

Импликация

е

^

Отрицание

(. е 0 )

—1

Таблица 2. Выполнимость [ 2 ]

х

У

х е 0

х е у

((х е 0 ) е 0 )

0

0

М

М

0

0

М

М

М

0

М

0

0

0

М

М

М

0

М

М

Таким образом, наличие констант 0 и М, а также отношений импликации е и отрицания (... е 0 ) позволяет строить модели логических схем посредством теории множеств, причем по теореме 1 модели эти непротиворечивы.

2.    Построения моделей схем

Входы логических схем (см. рис. 1) обозначаются а;, выход - b. Запись модели инвертора такова:

Ь={х е М|(х е0 ) или х=(а е0 )}(а),       (1)

где а ; , b принимают значения 0 , М.

Модель элемента 2ИЛИ:

Ь={х е М|(х е0 ) или х=((а1 е0 ) е а2)}(а12).

Модель элемента 2И:

Ь={х е М|(х е0 ) или х=((а 1 ё 2 е0 )) е0 )}(аь а 2 ).

Модель элемента 2И-НЕ:

Ь={х е М|(х е0 ) или х=(а1 е 2 е0 ))}(а1, а2).

Эти логические элементы образуют базис, посредством которого строятся остальные более сложные логические схемы [5, с. 12].

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

а ) б)

в ) г )

Рис. 1. Элементы логических схем: а) инвертор НЕ, б) элемент 2ИЛИ, в) элемент 2И, г) элемент 2И-НЕ

Ь={х е М|(х е0 ) или L(x, y i ,. уп)}( y i ,. уп). (2)

По теореме 1 высказывание L(.) в схеме (2) задает некоторый объект, но не его дополнение. Это означает, что построенные модели логических схем - непротиворечивы.

Аналогично строятся модели более сложных схем, например модель RS-триггера (рис. 2), построенного из двух элементов 2ИЛИ-НЕ.

Рис. 2. RS-триггер

Модель RS-триггера состоит из двух взаимосвязанных выражений:

Ь={х е М|(х е0 ) или х=(((а1 е0 ) е d) е0 )}(a1, d) d={x е M|(x е0 ) или х=(((с2 е0 ) е Ь) е0 )}(с2, b).

Более сложные схемы строятся аналогично, набор основных логических функций, реализуемых в базисе, указанном в табл. 1, приведен в табл. 3.

3.    Замечание о модельной области

В модельной области лямбда-исчисления также строятся непротиворечивые модели, но иного вида, реализующие арифметику на подмножестве множества натуральных чисел, например модель сумматора двух чисел (b=a1+a2) такова:

b={x M|(x ∈∅ ) или х Pa 2 (a 1 )}(a 1 , a 2 ), (3) где a 1 , a 2 N, а Pa 2 (a 1 ) – простой последователь степени a 2 , взятый от a 1 .

Известна следующая теорема [4, 6]:

Теорема 2 (слабая непротиворечивость). Лямбда-исчисление над его модельной областью (конечные натуральные числа) в теории множеств с самопринад-лежностью непротиворечиво. □

Общий вид схемы свертывания с высказыванием, дополненной внешними переменными, принимающими значения в конечной области натурального ряда К, К N, b, у 1 ,… у n К N, таков:

b={x M|(x ∈∅ ) или L(x, у 1 ,… у n )}( у 1 ,… у n ). (4)

По теореме 2 высказывание L(.) в схеме (4) задает некоторый объект, но не его дополнение. Это означает, что построенные модели над областью K натуральных чисел непротиворечивы.

Заключение

Показано, что модели логических схем, строящиеся посредством теории множеств с самопринадлежностью, являются непротиворечивыми; приведены примеры построения базисных логических элементов и RS-триггера. Способ построения моделей логических схем использует модель двузначной логики, для которой ранее доказана теорема исключения третьего [2].

Таким образом, непротиворечивость получаемых моделей обоснована посредством

Таблица 3. Логические функции в базисе модели

Логич. функция

Выражение в базисе

Значения переменных

x

x

M

M

y

y

M

M

не x

(x ∈∅ )

M

M

не у

∈∅ )

М

М

x y

(x y)

M

M

M

х или у

((х ∈∅ ) у)

М

М

М

х и у

[(х ∈∅ )) ∈∅ ]

М

х = у

([(х у) ((у х) ∈∅ )] ∈∅ )

М

М

х у

[(х у) ((у х) ∈∅ )]

M

M

результатов теории множеств с самопринад-лежностью.

Список литературы Моделирование логических схем посредством теории множеств

  • Чечулин В.Л. Теория множеств с самопринадлежностью (основания и некоторые приложения): монография. Пермь, 2010. 100 с. URL: http://elibrary.ru/item.asp?id=15267103
  • Чечулин В.Л. О приложениях семантики самопринадлежности//Вестн. Перм. ун-та. Сер. Математика. Механика. Информатика. 2009. Вып. 3 (29). С.10-17.
  • Чечулин В.Л. Об одном варианте модельной области лямбда-исчисления//Синтаксис и семантика логических систем. Иркутск, 2010. С.112-114.
  • Чечулин В.Л. О непротиворечивости лямбда-исчисления//В мире научных открытий. Сер. Математика. Механика. Информатика. 2011. №1. С. 203-206.
  • Потемкин И.С. Функциональные узлы цифровой автоматики. М., 1988. 320 с. URL: http://www.nkras.ru/articles/2011/1/vypusk12011pdf
  • Chechulin V.L. About the selfconsidering semantic in the mathematical logic//Bull. Symbolic Logic. Vol.16, Is. 1(2010). P.111-112.
Статья научная