Logics without Contraction II
Martin Bunder · 1997
Abstract BCI and BCK logics are named after the combinators B, C, I, and K. Combinators are simple operators which apply to arbitrary terms X, Y, ... as follows: BXYZ = X(YZ)CXYZ= XZYIX=XKXY=XWXY= XYY. These terms can all be regarded as functions. For every X and Y, BXY is a unary function which maps Z to X( YZ), BX is a function that maps Y into the function BXY, etc.