л-выражения true, false и not наделены такими свойствами:
not true = false
not false = true
Для того, чтобы представить булевскую функцию ∧ (“и”) , л-выражения and наделены такими свойствами:
and true true = true
and true false = false
and false true = false
and false false = false
Для того, чтобы представить булевскую функцию ∨ (“или”) , л-выражения or наделены такими свойствами:
or true true = true
or true false = true
or false true = true
or false false = true
л-выражения, используемые для представления вещей могут показаться на первый взгляд абсолютно немотивированными. Но определения выбираются таким образом, чтобы они работали согласованно. Мы будем писать
LET ~ = л-выражение
для того, чтобы ввести ~ как новую нотацию. Обычно ~ будет просто именем, как true или and. Такие имена написаны жирным шрифтом или подчёркнуты, чтобы отличать их от переменных. Так, например,
true – переменная, а true это л-выражение лx. лy. x (см. 2.1), а 2 – число, в то время как 2 это л-выражение лf x. f (f x) ( см. 2.3).
Иногда ~ будет использована как более сложная форма, как условная нотация ( Е → E1 | E2 ).
2.1 Значения истинности и условные высказывания.
В этом параграфе л-выражения true, false, not и ( E → E1 | E2 ) наделены такими свойствами:
not true = false
not false = true
(true → E1| E2 ) = E1
(false → E1 | E2 ) = E2
л-выражения true и false представляют значения истинности true и false, not представляет функцию ¬ “не”, а ( E → E1 | E2 ) представляют условное высказывание, “Если Е, тогда Е1, иначе Е2”.
Существует бесконечное множество работающих способов представления значений истинности и отрицания; те, которые мы приведем являются традиционными и выработаны логиками за длительное время.
LET true = лx. лy. x
LET false = лx. лy. y
LET not = лt. t false true
Легко использовать правила л-конверсии для того, чтобы показать что эти определения обладают нужными свойствами. Например:
not true = (лt. t false true ) true (по определению not)
= true false true ( β-конверсия)
= (лx. лy. x) false true ( по определению true)
= (лy. false) true ( β-конверсия )
= false ( β-конверсия )
Подобным образом, not false = true.
Условные выражения ( E → E1 | E2 ) можно определить следующим образом:
LET ( E → E1 | E2 ) = ( E E1 E2 )
Это означает, что для любого л-выражения Е, Е1 и Е2 , ( E → E1 | E2 ) означает ( E E1 E2 ).
Условные высказывания работают корректно:
( true → E1 | E2 ) = true E1 E2
= (лx y. x) E1 E2
= E1
и
( false → E1 | E2 ) = false E1 E2
= (лx y. y) E1 E2
= E2
Упражнение 13
Предположим, and – л-выражение лx y. ( x → y | false ). Показать что:
and true true = true
and true false = false
and false true = false
and false false = false
Упражнение 14
Придумайте такое л-выражение or что:
Or true true = true
Or true false = true
Or false true = true
Or false false = false
2.2 Пары и кортежи
Следующие аббревиатуры представляют пары и n-кортежи в
л-исчислении.
LET fst = лp. p true
LET snd = лp. p false
LET ( E1 E2 ) = лf. f E1 E2
(E1 E2 ) – л-выражения представляющие упорядоченную пару, чей первый компонент ( т. е. Е1 ) доступен из функции fst, а второй из snd. Следующие вычисления показывают, как взаимодействуют различные описания для получения правильного ответа.
fst ( E1, E2 ) = (лp. p true ) (E1 E2)
= (E1, E2 ) true
= (лf. f E1 E2 ) true
= true E1 E2
= (лx y. x ) E1 E2
= E1
Упражнение 15
Показать, что snd ( E1, E2 ) = E2
Пара представляет собой структуру данных из двух компонент. Обобщение на n компонент называется n-кортежом и легко определяется с помощью пар.
LET ( E1, E2 , … , En ) = ( E1, ( E2, ( … ( En-1, En) … )))
(E1, … , En) – n-кортеж с компонентами E1, … ,En и длиной n. Пары – это 2-кортежи. Аббревиатуры определенные ниже, предоставляют способ извлечения компонент из n-кортежей.
n
LET E ↓ 1 = fst E
n
LET E ↓ 2 = fst ( snd E)
.
.
. n
LET E ↓ i = fst ( snd(snd( … ( snd E) … ))) (если i < n )
------------------------
i-1 snds
.
.
. n
LET E ↓ snd(snd( … (snd E) … )))
--------------------
i-1 snds
Легко показать, что эти определения работают, например:
n n
(E1,E2, … , En)↓ = (E1,(E2,(…)))↓1
= fst (E1,(E2,(…)))
= E1
n n
(E1,E2, … En)↓2 = (E1,(E2,(…)))↓2
= fst (snd ( E1,(E2,(…))))
= fst (E2,(…))
= E2
n
В общем случае (E1, E2, … ,En)↓i =Ei для любого i такого, что 1 ≤ i ≤ n.
Соглашение
n
Обычно мы будем писать просто Е ↓ i вместо E ↓ i, когда очевидно что n необходимо. Например:
(E, … , En) ↓ i = Ei ( где 1 ≤ i ≤ n).
2.3 Числа
Есть множество способов представления чисел с помощью л-выражений, каждый со своими достоинствами и недостатками [38,22]. Задача состоит в том, чтобы определить л-выражение n для представления каждого числа n. Нам также необходимо определить л-выражения для представления простейших арифметических операций. Например, нам понадобятся функции suc, pre, add и iszero, которые соответственно представляют функцию наследования ( n → n + 1 ), предшествования ( n → n – 1 ), сложения и проверки равенства нулю. Эти л-выражения будут правильно представлять числа, если они будут обладать следующими свойствами:
suc n = n+1 (для всех чисел n)
pre n = n-1 (для всех чисел n)
add m n = m+n (для всех чисел m и n)
iszero 0 = true
iszero ( suc n) = false
Здесь описано классическое представление чисел по Черчу. Для того чтобы объяснить его, удобно определить f n x как n аппликаций f к x. Например,
f 5 x = f (f (f (f (f x ))))
По соглашению, f 0 x означает x. В общем случае:
LET E0 E′ = E′
LET En E′ = E(E( … (E E′)…))
------------
n штук Е
Обратите внимание, что En (EE′) = En+1 E′ = E(En E′) … )) ; этот факт мы будем использовать в дальнейшем.
Пример:
f4x = f (f (f (f x))) = f (f3x) = f3(f x)
Используя введенные обозначения, мы теперь можем определить числа Черча. Заметьте, как следующее л-выражение n кодирует унарное представление n.
LET 0 = лf x. x
LET 1 = лf x. fx
LET 2 = лf x. f(f x)
.
.
.
LET n = лf x. fn x
.
.
Теперь могут быть получены представления suc, add и iszero. Чтобы понять как они работают, лучше всего представлять, что они работают с унарными представлениями чисел. Упражнения, следующие ниже, должны помочь.
LET suc = лn f x. n f (f x)
LET add = лm n f x. m f (n f x)
LET iszero = лn. n (лx. false) true
Упражнение 16
Показать, что
(i) suc 0 = 1
(ii) suc 5 = 6
(iii) iszero 0 = true
(iv) iszero 5 = false
(v) add 0 1 = 1
(vi) add 2 3 = 5
Упражнение 17
Для любого m и n показать, что:
(i) suc n = n+1
(ii) iszero ( suc n) = false
(iii) add 0 n = n
(iv) add m 0 = m
(v) add m n = m+n
Функцию предшествования определить труднее, чем другие простейшие функции. Идея состоит в том, что предшественник n определяется используя лf x. fn x (т. е. n), для получения функции, которая применяется только n-1 раз. “Выбросим” первое f в fn. Для того, чтобы это сделать, нужно сперва определить функцию prefn которая оперирует с парами и имеет свойства:
(i) prefn f (true, x) = (false, x)
prefn f (false, x) = (false, f x)
Из этого следует :
(iii) (prefn f)n (false, x) = (false, fn x)
(iv) (prefn f)n (true, x) = (false, fn-1 x) (если n > 0)
Таким образом, n применений prefn к (true, x) дают n-1 применений f к x. Используя эту идею, определение функции предшествования pre очевидно. Но, прежде чем дать его, дадим определение prefn
LET prefn = лf p. (false, (fst p → snd p | (f(snd p))))
Упражнение 18
Показать, что prefn f (b, x) = (false,(b → x | f x )) , и, следовательно,
prefn f (true, x) = false, x)
prefn f (false, x) = (false, f x)
(prefn f)n (false, x) = (false, fn x)
(prefn f)n (true, x) = (false, fn-1 x) (если n>0)
Теперь можно определить функцию предшествования pre:
LET pre = лn f x. snd (n ( prefn f) (true, x))
Из этого следует, что если n>0 тогда
pre n f x = snd (n (prefn f)( true x)) (по определению pre)
= snd ((prefn f)n (true, x)) (по определению n)
= snd((false, fn-1 x) (по (v) описанному выше)
= fn-1 x
Следовательно, из экстенсиональности ( см. 1.7) :
pre n = лf x. fn-1 x
|
Из за большого объема этот материал размещен на нескольких страницах:
1 2 3 4 5 6 7 8 9 10 11 |
