Конструктивное понятие истинности.




Конструктивная семантика для СКИП.

Произвольнуюформулу F конструктивного исчисления предикатов мы будем рассматривать как спецификацию (точное описание) некоторой задачи Z. Формулу F будем считать истинной, если мы сможем предъявить решение задачи Z.

 

Формула F&G истинна, когда мы можем построить терм вида

<tF, tG>, где tF -решение F, tG -решение G.

Формула F G истинна, когда мы можем построить терм вида

<0, tF> или <1, tG>, где tF -решение F, tG -решение G..

Формула F G истинна, когда имеется решение задачи G с некоторым параметром типа F (т.е. по любому решению задачи F можно построить решение задачи G):

xF. tG (xF ).

Формула x0 F(x0)истинна, когда существуют конкретный объект a0 и решение tF(a), т.е мы можем построить терм вида < a0, tF(a)>.

Формула x0 F(x0) истинна, когда для любого объекта x0 можно построить решение задачи F(x0), т.е мы можем построить терм вида x0 . tF().

Конструктивное понятие отрицания:

 

Константа ложь f или 0=1.

Идея построения правильных программ:

 

Цель следующего определения ввести синтаксическое понятие «замкнутый - терм типа F», таким образом, чтобы конструктивная истинность определялась следующим образом: формула F - истинна тогда и только тогда, когда существует замкнутый - терм типа F.

6.2. Определение замкнутого -терма.

0). Пусть tf произвольный -терм типа f. Тогда для любой формулы А терм tf также будем считать термом типа А.

1).ПустьA- произвольная формула конструктивного исчисления предикатов, тогда xA является -термом типа А, при этом переменная xA в -терм xA входит свободно.

2). Пусть tA произвольный -терм типа А,Sb – произвольный -терм типа В, тогда

< tA, Sb >=r A&B

является -термом типа А&В, при этом все свободные переменные термов tA, Sbявляются свободными переменнымии в -терме r A&B типа А&В.

3). Пусть tA произвольный -терм типа А,Sb – произвольный -терм типа В, тогда

= r A B

является -термом типа А В, при этом все свободные переменные термов tA, Sbявляются свободными переменнымии в -терме r A B типа А В.

4). Пусть tB (xA)- терм, в который входит свободно переменная xA типа А, тогда

xА. tВ (xА )= r A B

является -термом типа А В, при этом все свободные переменные терма tB, за исключением переменной xA, являются свободными переменнымии в -терме r A B типа А В.

5). Пусть t0- объектный терм, SA() -терм, тогда

<t0, SA( ) >= r

является -термом типа , при этом все свободные переменные терма SA() являются свободными переменнымии в -терме r типа .

6). Пусть tA() -терм, x0-объектная переменная, тогда

x0. tA( ) = r

является -термом типа , при этом все свободные переменные терма tA(), за исключением переменной x0, являются свободными переменнымии в -терме r типа .

7а). Пусть t A&B - терм типа А&B, тогда

(t A&B)0 = rA,

является термом типа A, при этом все свободные переменные терма t A&Bявляются свободными переменными и в терме rA.

7б). Пусть tA&B терм типа A&B, тогда

(t A&B)1 =rВ,

является термом типа B, при этом все свободные переменные терма tA&B являются свободными переменными и в терме rВ.

8а). Пусть t - терм типа x A(x), тогда

(t )0 = r0,

является объектным термом, при этом все свободные переменные терма t являются свободными переменными и в терме r0.

8б). Пусть t - терм типа x A(x), тогда

(t )1 = rA( ), где S0= (t )0,

является термом типа A(S0), при этом все свободные переменные терма t являются свободными переменными и в терме rA().

9а). Пустьt A B - терм типа A B, SA - терм типа A, тогда

t A B[SA] = rB,

является термом типа B, при этом все свободные переменные термов t A B и SA являются свободными переменными в терме rB.

9б). Пусть t - терм типа x A(x), S0 - объектный терм, тогда

t [S0] = rA( ),

является термом типа A(S0), при этом все свободные переменные терм t являются свободными переменными и в терме rA().

10). ПустьtA, SA – термы типа A, u0, v0 – объектные термы, тогда

(if u0 = v0 then tA else SA) =rA,

является термом типа A, при этом все свободные переменные термов tA, SA, u0, v0 являются свободными переменными в терме rA.

 

 

-терм называется замкнутым, если он не содержит свободных переменных.



Поделиться:




Поиск по сайту

©2015-2024 poisk-ru.ru
Все права принадлежать их авторам. Данный сайт не претендует на авторства, а предоставляет бесплатное использование.
Дата создания страницы: 2020-03-12 Нарушение авторских прав и Нарушение персональных данных


Поиск по сайту: