Модел в комбинатор без точки, как е свързан със SKI смятането

Като упражнение преобразувах следния комбинатор в нотация без точки:

h f g x y z = f x (g y z)

с обичайната конвенция за f, g, h като функции и x, y, z като изрази. (Това не е проблем за домашна работа, а просто за забавление и за да видя дали разбирам преобразувания без точки.)

След дълъг процес на ръчно пренаписване, подпомаган от ghci, стигнах до следното:

h = ((flip (.)) (flip (.)) . (flip (.))) . ((.)(.))

Забелязах, че h се състои само от два комбинатора, "compose" (.) и "reverse compose" flip (.). С това оригиналният комбинатор може да бъде написан накратко като:

c = (.) -- compose
r = flip c -- "reverse compose"
h = ((r r) . r) . (c c)
   = c(c(r r)r)(c c)

Структурата (броят и редът на) на операциите "съставяне" и "обратно композиране" изглежда по някакъв начин е свързана със структурата на оригиналния комбинатор.

Смятам, че това е пряко свързано с комбинаторната логика и SKI смятането. Въпросите ми са така:

  1. Може ли някой с по-добра представа да обясни какво се случва тук: как структурата на „съставяне“ и „обратно композиране“ в комбинатора без точки е свързана със структурата на функциите и изразите в точковия комбинатор?

  2. Може ли това да се обобщи до произволни комбинатори (т.е. брой функции, брой изрази и техният ред е произволен)? По-конкретно, може ли всеки комбинатор да бъде израз по отношение на „съставяне“ и „обратно композиране“ и има ли схема за извличане на комбинацията от „съставяне“ и „обратно композиране“ директно от структурата на точковият комбинатор (т.е. без преминаване през целия процес на пренаписване)? Например, възможно ли е директно да се извлекат безточковите версии на \ f g x y z -> (f x y) g z само от разглеждане на функционалната структура?

  3. Какво е името в комбинаторната логика за c и r?

Актуализация:

Изглежда, че c е B комбинаторът, а r е CB от B, C, K , система W. Но все пак ще се радвам да получа повече информация за въпросите си, особено за въпроси 1 и 2.


haskell combinatory-logic lambda-calculus pointfree
person Powerfool    schedule 16.03.2014    source източник
comment
Ако дадена променлива се появи повече от веднъж в RH, тогава B и CB вече не са достатъчни (нужни са напр. S). Ако дадена променлива изобщо не се среща, те също не са достатъчни (нужни са напр. K)   -  person augustss    schedule 16.03.2014
comment
По отношение на 2, абстракцията от скоби е прост алгоритъм за SKI.   -  person augustss    schedule 16.03.2014
comment
тук можете да намерите трансформацията на скоби, която augustss споменава (мисля).   -  person Will Ness    schedule 16.03.2014
comment
augustss: Много интересно, благодаря. Какъв би бил добър уводен текст, който да научите за комбинаторното смятане? Уил: Благодаря за справката.   -  person Powerfool    schedule 16.03.2014

Отговори (1)


arrow_upward
2
arrow_downward

Първо, обикновено е по-лесно да се извлекат дефинициите чрез директна манипулация в комбинирана форма:

h f g x y z = f x (g y z)
            = B(fx)(gy)z     -- B rule
            = B(B(fx))gyz    -- B rule
h f g x = B(B(fx))g          -- eta-contraction
        = BBB(fx)g           -- B rule
        = B(BBB)fxg          -- B rule
        = C(B(BBB)f)gx       -- C rule
h f = C(B(BBB)f)             -- eta-contraction
    = BC(B(BBB))f            -- B rule
h   = BC(B(BBB))             -- eta-contraction
 -- = B(B(CB(CB))(CB))(BB)   -- your expression

Типовете са същите, но моят израз е по-кратък. Може ли това да служи като контрапример за това дали комбинираната форма трябва по някакъв начин да следва дадената дефиниция? Съществува значителна свобода в начина на прилагане на правилата, така че могат да бъдат изведени много различни форми. Не мисля, че може да се стигне до много прозрение от даден комбинативен израз.

Ако не друго, комбинаторите, които се появяват в окончателния превод, са по-представителни за предприетите стъпки за извличане и те могат да бъдат избрани свободно измежду тези, които отговарят във всеки даден момент.

Например, следната стъпка обикновено се предприема при извличането на вашия израз, очевидно:

g(fx) = Bgfx = CBfgx 

B (B (CB(CB)) (CB)) (BB) f g x y z
   = B (CB(CB)) (CB) (BB f) g x y z
   = CB (CB) (CB (BB f)) g x y z     --   and here
   = CB (BB f) (CB g) x y z          --  here
   = CB g (BB f x) y z               -- here
   = BB f x (g y) z
   = B (f x) (g y) z
   = f x (g y z)

Но ако приоритизирате приложението на правилата си и го направите детерминистично, винаги трябва да достигате до един и същ резултат -- което ще зависи от реда, в който прилагате правилата.

person Will Ness    schedule 16.03.2014
comment
Манипулирането на комбинаторната форма наистина е много по-просто от моя процес на преобразуване от точка към точка без (имах около три пъти повече междинни стъпки.) Жалко обаче, че явното преобразуване все още изглежда необходимо. Надявах се, че структурата на комбинаторната форма е в пряка връзка с точковата форма. Ако не като цяло, то поне за специални случаи като f_{0,n_0} f_{1,n_1} ... f_{K-1, n_{K-1}}, където f_{i,n} := f_i xi_0 xi_1 ... xi_{n-1} (т.е. K функции f_0, ..., f_K, всяка с променливо число [xi_0, ..., xi_{n-1}] от взаимно несъответстващи изрази). - person Powerfool; 16.03.2014
comment
изглежда, че е в пряка връзка с предприетите стъпки за трансформация. - person Will Ness; 17.03.2014