Combinator
definition a combinator is a closed lambda-calculus term --- https://youtu.be/seVSlKazsNk and https://youtu.be/VrRVqHvy4PQ?t=422
properties
combinators can be manipulated through combinatory logic
proceduce big B, due to Ethan Sue
any parenthesization of free variables can be achieved using solely the b ‹combinator. for example, \(a\ (b\ c)\ (d\ e\ (f\ g)) = B\ B\ (B\ (B\ (B\ B\ (B\ B))\ B))\ a\ b\ c\ d\ e\ f\ g\)
let terms \(R, S, T\) and free variable \(x\). repeatedly rewrite \(R\ (S\ T) \mapsto \mathrm B\ R\ S\ T\) and \(R\ x \mapsto R\) at the top level until all free variables have been consumed. the resulting combinator can be shortened by rewriting \(\mathrm B\ R\ S\ T \mapsto R\ (S\ T)\) recursively. the rewrites are carried out on the abstract ‹syntax, not on the concrete ‹syntax. --- birb.pl --- https://github.com/uocsclub/to-mock-a-mockingbird/blob/main/code/birb.pl
combinators
I Combinator
identity
aka identity, id in Haskell
definition I = x -> x = (*) #todo id
definition I = S K K
definition I = ii ii
notation (*) x #todo id
K Combinator
discards the second argument
aka constant, const in Haskell
definition K = x. y. x
definition K = ii (ii (ii ii))
notation .x y
S Combinator
aka substitution, <*> and ap in Haskell
definition S = f. g. x. f x (g x)
definition S = ii (ii (ii (ii ii)))
notation (f g) x or equivalently (* f g) x #todo id
B Combinator
the composition of its arguments
aka compose, (.) and fmap in Haskell, "bluebird"
definition B = f. g. x. f (g x)
definition B = S (K S) K
definition in the lambda-calculus \(B = \lambda fgx.\ f\ (g\ x)\)
notation f`g x
--- https://youtu.be/SmXB2K_5lcA?t=612
B1 Combinator
aka "blackbird", .: in Haskell
definition B_1 = f. g. x. y. f (g x y)
definition B_1 = B B B
definition .: = (.) . (.)
C Combinator
swaps the arguments to a function
aka flip, flip in Haskell
equiv matrix › transpose
definition C = f. x. y. f y x
definition C = S (B B S) (K K)
notation rr f x y
W Combinator
duplicates the second argument
aka duplication, 'commute' or 'self' in APL, join in Haskell
definition W = f. x. f x x
definition W = C S K
notation (f *) x or equivalently (* f *) x #todo id
M Combinator
applies a function to itself
aka mockingbird, ω combinator
definition M = f. f f
definition M = S I I
notation (* *) f #todo id
KI Combinator
discards the first argument
aka kite, const id in Haskell
definition K I = f. x. y. f y
notation .(*) #todo id
T Combinator
applies the first argument to the second argument
aka thrush, & in Haskell
definition T = x. f. f x
definition T = C I
SBI Combinator
applies a function twice
definition S B I = f. x. f (f x)
Sigma Combinator
aka chain, =<< in Haskell, S' combinator
definition SS = f. g. x. f (g x) x
notation (g f *) x #todo id
Psi Combinator
aka on in Haskell
definition YY = f. g. x. y. f (g x) (g y)
notation g {x f y}
Phi Combinator
aka converge, liftA2 and liftM2 and phoenix and starling' in Haskell, S2 combinator, S' combinator, 'fork' in APL
definition FF = f. g. h. x. f (g x) (h x)
notation (g f h) x
Phi1 Combinator
definition FF_1 = f. g. h. x. y. f (g x y) (h x y)
notation x (g f h) y
Y Combinator
aka fixed-point combinator, fix in Haskell
see fixed point
the y ‹combinator lets us use recursion in programming languages that don't support it, which includes the lambda-calculus
definition Y = f. (x. f (x x)) (x. f (x x))
definition using recursion Y = f. f (Y f)
definition in the lambda-calculus \(Y = \lambda f.\ (\lambda x.\ f\ (x\ x)) (\lambda x.\ f\ (x\ x))\)
example \(\mathrm{fact} = Y\ (\lambda f\ n.\ (\mathrm{is0}\ n)\ 1\ (\mathrm{mul}\ n\ (f\ (\mathrm{pred}\ n))))\) --- https://crypto.stanford.edu/~blynn/lambda/ and https://youtu.be/VrRVqHvy4PQ
--- https://en.wikipedia.org/wiki/Fixed-point_combinator#Y_combinator
Theta Combinator
aka Turing combinator
see fixed point
definition QQ = (x. y. y (x x y)) (x. y. y (x x y))
the advantage of the theta ‹combinator over the y ‹combinator is that QQ f β-reduces to f (QQ f) while Y f and f (Y f) only β-reduce to a common term
--- https://en.wikipedia.org/wiki/Fixed-point_combinator#Other_fixed-point_combinators
--- https://crypto.stanford.edu/~blynn/lambda/quine.html#_curry
Iota Combinator
definition ii = x. x S K
we have ii ii = I /\ ii (ii ii) = S K /\ ii (ii (ii ii)) = K /\ ii (ii (ii (ii ii))) = S; the iota ‹combinator can be used to define the s ‹combinator and k ‹combinator, and can therefore be composed to produce combinators that are extensionally equal to any term in the lambda-calculus. consequently, ii combinatory logic is turing complete
---
--- https://en.wikipedia.org/wiki/Combinatory_logic#One-point_basis
--- https://en.wikipedia.org/wiki/SKI_combinator_calculus#Informal_description
--- https://youtu.be/gnrSedVucXs?t=1678
--- https://en.wikipedia.org/wiki/Iota_and_Jot#Universal_iota
---
--- https://en.wikipedia.org/wiki/B,_C,_K,_W_system
--- https://en.wikipedia.org/wiki/SKI_combinator_calculus
--- https://www.uiua.org/docs/combinators
--- https://youtu.be/gnrSedVucXs
--- https://youtu.be/Y0KKPYkeOTA
--- Combinator Table - Combinatory Logic.html --- https://combinatorylogic.com/table.html --- https://youtu.be/Y0KKPYkeOTA
--- Combinator Birds.html --- https://www.angelfire.com/tx4/cus/combinator/birds.html --- https://combinatorylogic.com/table.html --- https://youtu.be/Y0KKPYkeOTA
--- https://gist.github.com/Avaq/1f0636ec5c8d6aed2e45#file-combinators-md --- https://combinatorylogic.com/table.html --- https://youtu.be/Y0KKPYkeOTA
--- https://codegolf.stackexchange.com/questions/53250/optimizing-ski-compiler
--- https://cs.stackexchange.com/questions/13901/what-is-the-name-of-this-combinator
--- https://youtu.be/i1K_kUKJnE4?t=525