blob: 21f75e875d7191ba741e6028fccb785df0544d0e (
plain) (
tree)
|
|
/ Combinators /
/ Following Brent Kerby's 'The Theory of Concatenative Combinators' (TCC) /
/ Everything below doubles 3 /
3 ↑ + / Double 3 /
3 ⊂ ↑ + ⊃ ⍎ / Push execution token to stack, execute it /
3 ⊂ ↑ + ⊃ unit ⍎ ⍎ / Push execution token, wrap with unit, unwrap with ⍎, execute with ⍎ /
3 ⊂ ↑ ⊃ ⊂ + ⊃ cat ⍎ / Push separate execution tokens for ↑ and +, combine with cat, execute with ⍎ /
3 ⊂ + ⊃ ⊂ ↑ ⊃ ↕ cat ⍎ / Push executions for + and ↑, swap order with ↕, combine with cat, execute /
/ The examples above illustrate the definitions of the combinators /
/ The combinators also satisfy some interesting identities /
/ For example
unit ≡ ⊂⊃ cons
so this also doubles 3: /
3 ⊂ ↑ + ⊃ ⊂⊃ cons ⍎ ⍎
/ We can define a unit' which does this: /
∇ unit' ⊂⊃ cons ∇
3 ⊂ ↑ + ⊃ unit' ⍎ ⍎
/ The following also doubles three: /
3 ⊂ ↑ ⊃ ⊂ + ⊃ ⊂ ⍎ ⊃ ⊂ dip ⍎ ⊃ cons cons cons ⍎
/ This is because of the identity
cat ≡ ⊂ ⍎ ⊃ ⊂ dip ⍎ ⊃ cons cons cons
We can define a new cat' which does this:
/
⊂ dip ⍎ ⊃ ⊂ ⍎ ⊃ ∇ cat' LITERAL LITERAL cons cons cons ∇
/ The LITERALs just compile the execution tokens in the definition of cat' /
3 ⊂ ↑ ⊃ ⊂ + ⊃ cat' ⍎
/ Also cons can be written in terms of cat,
cons ≡ ⊂ unit ⊃ dip cat
giving /
⊂ unit ⊃ ∇ cons' LITERAL dip cat ∇
3 ⊂ ↑ + ⊃ ⊂⊃ cons' ⍎ ⍎
/ swap ≡ unit dip /
∇ swap' unit dip ∇
3 ⊂ + ⊃ ⊂ ↑ ⊃ swap' cat ⍎
∇ dip' ↕ unit cat ⍎ ∇
3 ⊂ + ⊃ ⊂ ↑ ⊃ unit dip' cat ⍎
/ ⍎ ≡ ↑ dip ↓ / ∇ ⍎' ↑ dip ↓ ∇
/ ⍎ ≡ ⊂⊃ unit dip dip ↓ / ∇ ⍎'' ⊂⊃ unit dip dip ↓ ∇
/ ⍎ ≡ ⊂⊃ unit dip dip dip / ∇ ⍎''' ⊂⊃ unit dip dip dip ∇
3 ⊂ ↑ + ⊃ ⍎'
3 ⊂ ↑ + ⊃ ⍎''
3 ⊂ ↑ + ⊃ ⍎'''
/ Lambdas /
/ λ (written \ in TCC) can be implemented as a Forth defining word /
∇ λ ◁ , ▷ @ ⍎ ∇
/ dip ≡ λ a λ b a ⊂ b ⊃ /
3 ⊂ + ⊃ ⊂ ↑ ⊃ unit λ a λ b a ⊂ b ⊃ cat ⍎
/ End of scope ($ in TCC) can be done with HIDE a /
∇ $ HIDE ∇
/ An Abstraction Algorithm /
/ TCC gives an algorithm to eliminate λ's from combinators. Applying it /
/ gives the equivalence of /
/ λ a b a ⊂ c a ⊃ ≡ ⊂ b ⊃ dip ↑ ⊂ ⍎ ⊃ dip ⊂ c ⊃ ⊂ dip ⍎ ⊃ cons cons /
/ ( lambda ) ( no lambda ) /
/ For example, letting b be ↑ and c be + and trying each of the above /
/ combinators on a stack with 2 ⊂ 1+ ⊃ on ( adding an ⍎ at the end of /
/ both to test the effect of the ⊂ c a ⊃ left on top of the stack) /
⊂ ↑ ⊃ ⊂ + ⊃ λ c λ b
2 ⊂ 1+ ⊃ λ a b a ⊂ c a ⊃ ⍎
2 ⊂ 1+ ⊃ ⊂ b ⊃ dip ↑ ⊂ ⍎ ⊃ dip ⊂ c ⊃ ⊂ dip ⍎ ⊃ cons cons ⍎
/ Both give 6 since in this case both lines are equivalent to 2 ↑ 1+ + 1+ /
/ The sip Combinator /
/ ⊂ b ⊃ ⊂ a ⊃ sip ≡ ⊂ b ⊃ a ⊂ b ⊃ /
/ ↑ ≡ ⊂⊃ sip /
3 ⊂⊃ sip +
/ dip ≡ λ a ⊂ ↓ a ⊃ sip /
3 ⊂ + ⊃ ⊂ ↑ ⊃ unit λ a ⊂ ↓ a ⊃ sip cat ⍎
/ dip ≡ ⊂ ↓ ↓ ⊃ ⊂ sip ⍎ ⊃ cons cons sip /
3 ⊂ + ⊃ ⊂ ↑ ⊃ unit ⊂ ↓ ↓ ⊃ ⊂ sip ⍎ ⊃ cons cons sip cat ⍎
/ Applicative Combinators /
∇ w ['] ↑ dip ⍎ ∇
∇ k ['] ↓ dip ⍎ ∇
∇ b ['] cons dip ⍎ ∇
∇ c ['] ↕ dip ⍎ ∇
∇ s >R ⊤ ↕ cons ↕ R> ⍎ ∇
/ ↑ ≡ ⊂⊃ w /
/ ↓ ≡ ⊂⊃ k /
/ cons ≡ ⊂⊃ b /
/ ↕ ≡ ⊂⊃ c /
3 ⊂⊃ w +
3 ↑ ↑ ⊂⊃ k +
3 ⊂ ↑ + ⊃ ⊂⊃ ⊂⊃ b ⍎ ⍎
3 ⊂ + ⊃ ⊂ ↑ ⊃ ⊂⊃ c cat ⍎
/ b ≡ ⊂ k ⊃ ⊂ s ⊃ ⊂ k ⊃ cons s /
⊂ k ⊃ ⊂ s ⊃ ⊂ k ⊃ ∇ b' LITERAL LITERAL LITERAL cons s ∇
3 ⊂ ↑ + ⊃ ⊂⊃ ⊂⊃ b' ⍎ ⍎
|