lomeo: (лямбда)
[personal profile] lomeo
Вот после долгих попыток перевести K в IBCS базис, понял, что этот базис не является полным, т.е, через него нельзя выразить любые лямбда-термы без свободных переменных.

Date: 2006-06-12 10:35 am (UTC)
From: [identity profile] timlendus.livejournal.com
Для перевода l-термов в базис I,B,C,S есть 2 правила:
1) lx.x = I
2) lx.PQ = BP(lx.Q) x не принадлежит P, x принадлежит Q
= C(lx.P)Q x принадлежит P, x не принадлежит Q
= S(lx.P)(lx.Q) x принадлежит P, x принадлежит Q
Отсюда видно что правила для ситуации, когда x не принадлежит ни P ни Q нет. Для того, чтобы проверить возможность разложения l-терма в базис I,B,C,S необходимо проверить наличие вхождения всех переменных левой части l-выражения в правую часть l-выражения. Например, lxy.x
нельзя разложить в этом базисе, т.к. нет вхождения переменной y в правую часть.
P.S. По данной тематике есть хорошие книги профессора Вольфенгагена, советую почитать.

Date: 2006-06-13 06:50 am (UTC)
From: [identity profile] lomeo.livejournal.com
Да, я собственно уже посмотрел.
Спасибо!

Profile

lomeo: (Default)
Dmitry Antonyuk

April 2024

S M T W T F S
 123456
7891011 1213
14151617181920
21222324252627
282930    

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 29th, 2025 10:03 am
Powered by Dreamwidth Studios