A lambda calculus that is close to both supercombinators and combinators in style. Lambda terms are defined so that all the arguments must be provided for substitution to take place. A Self variable provides the ability to define combinators recursively.
Step defines how a Term can be reduced in one step, the different options. Terms are variant lambda expressions. This 'combinatory lambda calculus' is halfway between the lambda calculus proper and a combinatory logic and is a kind of supercombinator logic. Lambda terms are given by a big lambda instead of the usual small lambda. This big lambda defines base combinators in terms of a lambda calculus, as per supercombinators, in such a way that all its arguments must be passed at once for the combinatory logic to apply. This is a calculus with no limit to the number of base combinators. As a consequence of the construction, and the combinatory flavour of the big lambdas, there are no complicated De Bruijn index manipulations. The indices whih are used are references to the arguments of the base combinator (ie a big lambda term), such that the largest index is the first argument. However, it only applies at the top level as any subterms comnsisting of further big lambdas do not have access to the arguments of any other lambda expression including that in which it is a sub-Term. Whilst this adds a little to the length of terms it also brings big lambda calculus into closer correspondence with combinatory logic and the advantages thereof.
'Variables' are used only within lambda caclulus terms to define the behaviour of base combinators. 'Constants' are the 'variables' of the combinatory calculus fragment (ie Terms which have no variables), acting as constants when within lambda terms - there are no substitutions into these constants within the calculus internally, though this may be implemented externally.
A 'Self' Term provides an additional means of defining recursion that should enable streams of arguments to be applied.
In ComboLambd2.agda a working version is given along with a proof of the Church-Rosser property. This now needs to be coded in a form that is more easily tested, experimented with and used.