문제

As an exercise, I converted the following combinator to point-free notation:

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

with the usual convention of f, g, h as functions, and x, y, z as expressions. (This is not a homework problem, but just for fun and to see if I understand point-free conversions.)

After a lengthy manual rewriting process aided by ghci, I ended up with the following:

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

I noticed that h only consists of two combinators, "compose" (.) and "reverse compose" flip (.). With this, the original combinator can be written succinctly as:

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

The structure (number and order of) of "compose" and "reverse compose" operations seem to be somehow related to the structure of the original combinator.

I reckon this is directly related to combinatory logic and SKI calculus. My questions are thus:

  1. Can somebody with more insight explain what's going on here: How is the structure of "compose" and "reverse compose" in the point-free combinator related to the structure of functions and expressions in the pointful combinator?

  2. Can this be generalized to arbitrary combinators (i.e., number of functions, number of expressions, and their order is arbitrary)? More specifically, can every combinator be expression in terms of "compose" and "reverse compose", and is there a scheme to derive the combination of "compose" and "reverse compose" directly from the structure of the pointful combinator (i.e., without going through the complete rewrite process)? For instance, is it possible to directly derive the pointfree versions of \ f g x y z -> (f x y) g z just from looking at the function structure?

  3. What's the name in combinatory logic for c and r?

Update:

It seems that c is the B combinator and r is CB from the B, C, K, W system. But I'd still be happy to get more insight into my questions, especially questions 1 and 2.

도움이 되었습니까?

해결책

First, it's usually easier to derive the definitions by direct manipulation in combinatory form:

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

The types are the same, though my expression is shorter. Can this serve as a counterexample to whether the combinatory form should somehow follow the given definition? There is considerable freedom in how the rules are applied, so widely different forms can be derived. I don't think much insight can be arrived at from a given combinatory expression.

If anything, the combinators that appear in the final translation are more representative of the derivation steps taken, and those can be chosen freely among those that fit, at any given point.

For example, the following step is commonly taken in deriving your expression, evidently:

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)

But if you prioritize your rules application and make it deterministic, you should always arrive at the same result -- which will depend on the order in which you apply the rules.

라이센스 : CC-BY-SA ~와 함께 속성
제휴하지 않습니다 StackOverflow
scroll top