COMBILOG

COMBILOG offers basic tools for experimenting with Combinatory Logic. These tools include rewriting of given terms involving combinators, providing the definitions of common combinators as well as the possibility to define your own or redefine existing combinators, and searching for combinators with certain properties.

Installation

$ npm install combilog

Quick Run

The search for combinators using random search, genetic search (Genetic Programming), and a heuristic search based on equational reasoning can be executed from the command line using modules rnd, gp, and eqr located in directory tests. Run

$ node tests/rnd

for usage information regarding random search,

$ node tests/gp

for usage information regarding genetic programming, and

$ node tests/eqr

for usage information regarding search based on randomized equational reasoning.

Usage

var cl = require('combilog');

cl exposes the following functions:

defineCombinator (combiDef)

Defines a combinator. Such a definition must be a string representing an equation, e.g. 'Qxy = yy'. Any upper-case letter can be used as a combinator symbol. A combinator may be primed using the standard single quote character or the special character \u2032. Naturally, the primed and unprimed combinators are distinct (cp. pre-defined combinators B and B'). An upper-case letter may also be followed by a digit. Thus, W0 through W9, for instance, are valid combinators.

Any lower-case letter can be used as a variable. Note that the combinator symbol must occur as the first symbol of the left side of the equation and no place else. The remainder of the left side is a sequence of distinct variables. The right side must be an arbitrary term constructed with the variables introduced by the left side (and only those variables).

The value returned by this function is null if no prior definition existed. Otherwise the previous definition is returned.

See also: resetCombinators, listCombinatorDefs, listCombinators, isCombinatorDefined, getCombinatorDef

getCombinatorDef (combiSym)

Gets the definition of a given combinator symbol (a string). The definition returned is a string representing the equation that defines the given combinator symbol. E.g.,

cl.getCombinatorDef('K')

returns

'Kxy = x'

This function returns null if the given combinator symbol is undefined.

See also: isCombinatorDefined, listCombinators, listCombinatorDefs

isCombinatorDefined (combiSym)

Checks whether a given combinator symbol (a string) is defined. It returns true if a definition exists, false otherwise. This method is slightly more efficient for checking the mere existence of a definition than getCombinatorDef in that there is no conversion of the internal representation of a combinator definition into a string.

See also: listCombinators

isFixedPointCombinator (combi, maxTermsVisited)

Checks whether the given combinator combi is a fixed-point combinator. It returns true if combi can be proven to be a fixed-point combinator. It returns false if combi can be disproved to be a fixed-point combinator. Otherwise it returns null.

A combinator Y is a fixed point combinator if f(Yf) = Yf for all f. (Let us use Y instead of combi to facilitate notation.) isFixedPointCombinator attempts to prove or disprove the fixed-point property by computing all possible children of Yf obtained by rewriting Yf with applicable combinator definitions. The number of children or terms visited is limited by maxTermsVisited. If omitted it defaults to 500. The fixed-point property is proven if there are children T and f(T) , where T is some term. It can be disproved if the set of children is finite (and its cardinality is not greater than maxTermsVisited) and there are no two such children in that set. Otherwise it cannot be determined (at least not within the given resource restrictions dictated by maxTermsVisited) whether the given combinator is a fixed-point combinator.

listCombinatorDefs ()

Returns the list of all available combinator definitions. The value returned is an array of strings. Each string represents an equation that defines the respective combinator symbol.

See also: getCombinatorDef, listCombinators

listCombinators ()

Returns a list all available or defined combinator symbols. The value returned is an array of strings, each string representing a combinator symbol.

See also: listCombinatorDefs

resetCombinators()

Resets combinator definitions. As a result all combinator definitions created through defineCombinator (new or overriding existing ones) are undone.

See also: defineCombinator

rewrite (combiTerm, maxSteps)

Rewrites the given term (a string) using the currently available combinator definitions. It returns the term (the so-called Normal Form) obtained by exhaustively applying the available definitions. The rewriting strategy employed is leftmost/innermost.

Note that a normal form may not always exist since applying combinator definitions is not guaranteed to terminate. Therefore the number of rewrite steps can be limited through maxSteps. If the limit is exceeded this function returns null. The number of steps is unlimited if maxSteps is a number less than zero. The default is -1 (unlimited).

Examples:

cl.rewrite('SKKx')

returns

'x'

and

cl.rewrite('BWBxy')

returns

'x(yy)'

See also: rewriteSteps

rewriteSteps (combiTerm, maxSteps)

Rewrites the given term (a string) using the currently available combinator definitions and collects all intermediate rewrite steps. Those steps are returned as an array (of strings representing terms). The given term as well as the final term (the Normal Form) are included as the first and last entry, respectively. The rewriting strategy employed is leftmost/innermost.

The number of rewrite steps can be limited through maxSteps. If the limit is exceeded the final entry in the array returned is null. The number of steps is unlimited if maxSteps is a number less than zero. The default is -1 (unlimited). Hence, if maxSteps is supplied and is a number greater than or equal to zero the resulting array will have a length not greater than maxSteps + 2.

Examples:

cl.rewriteSteps('SKKx')

returns

['SKKx', 'Kx(Kx)', 'x']

and

cl.rewriteSteps('BWBxy')

returns

['BWBxy', 'W(Bx)y', 'Bxyy', 'x(yy)']

See also: rewrite

rndSearchBehavior (base, varList, out, options)

Performs a random search for a combinator that satisfies the input/output behavior specified through parameters varList and out. The combinator sought is assembled using the elementary and pre-defined combinators given by parameter base, an array of combinator symbols.

Example:

cl.rndSearchBehavior(['S','K'],'x','x')

searches for a combinator consisting of S and K such that when applied to x produces x (in other words the identity).

This function returns an object with the following properties:

• solution: the combinator (as a string) that satisfies the given input/output behavior if such a combinator was found; otherwise this property is undefined

• iterations: the number of iterations, or in other words the number of random combinators created and tested

• minLength: the minimal length of the random combinators created and tested

• maxLength: the maximal length of the random combinators created and tested

• timeElapsed: the time elapsed as a human-readable string

• hrtimeElapsed: the time elapsed in process.hrtime format

If supplied parameter options must be an object that may have one or more of the following properties:

• iterations: the maximal number of iterations or random combinators; default is 100

• maxSteps: the maximal number of rewrite steps when testing a random combinator; default is 20. Note that although random search is not prone to memory shortage per se, it is possible to create random combinators that when testing, i.e. performing rewrite steps, bloat up and produce term sizes that do nonetheless create memory issues. Therefore, choose the number of this property wisely.

• minLength: the minimal length of a random combinator; default is 0 (which just like 1 will permit the creation of random combinators consisting of a single combinator from base)

• maxLength: the maximal length of a random combinator; default is 20 (thus limiting the maximal number of combinators from base occurring in a random combinator to 20)

• applyProbability: the probability for creating an application node (recall that SK is short for apply(S,K) ); default is 0.5. Higher probabilities steer the random creation towards longer combinators (within the confines of minLength and maxLength).

rndSearchFixedPointCombinator (base, options)

Performs a random search for a combinator that satisfies the strong fixed-point property. Such a combinator is assembled using the combinators given by parameter base, an array of combinator symbols.

For a description of the return value and available options see rndSearchBehavior.

eqRndSearchBehavior(base,varList,out,options)

Performs a randomized search for a combinator that satisfies the input/output behavior specified through parameters varList and out. The combinator sought is assembled using the elementary and pre-defined combinators given by parameter base, an array of combinator symbols.

The search procedure is based on backward equational reasoning. Starting with out, the combinator equations are applied right to left. The inverse application of combinator equations continues until a given maximal depth has been reached (out being at depth 0). At each depth level only a specified maximal number of terms are randomly chosen to be retained while all others are discarded. This process is repeated (starting over with out) until a solution is found or the maximal number of repetitions (a.k.a. iterations) is exceeded.

Example:

cl.eqRndSearchBehavior(['S','K'],'x','x')

searches for a combinator consisting of S and K such that when applied to x produces x (in other words the identity).

This function returns an object with the following properties:

• solution: the combinator (as a string) that satisfies the given input/output behavior if such a combinator was found; otherwise this property is undefined

• iterations: the number of iterations (i.e., the number of times the process started from out)

• created: the number of terms created by applying combinator equations from right to left

• retained: the number of created terms that were retained (i.e., not discarded)

• timeElapsed: the time elapsed as a human-readable string

• hrtimeElapsed: the time elapsed in process.hrtime format

If supplied parameter options must be an object that may have one or more of the following properties:

• iterations: the maximal number of iterations; default is 100

• maxDepth: the maximal depth of the search; default is 10

• maxRetained: the maximal number of terms chosen at random to be retained (i.e., not discarded) at each depth level; default is 5

• logger: a function that accepts a string as a parameter and logs it in an appropriate way (the amount of data logged is determined by property logLevel); in the simplest case use logger: console.log; default is no logging (logger is undefined)

• logLevel: the log level (a number ranging from 0 to 4) that determines the degree of detail of logging activities (logging takes place only in the presence of a logger, of course); as usual a bigger number means more data logged; default is 0 (nothing will be logged)

Note that a solution found by this procedure may contain free variables. For instance,

cl.eqRndSearchBehavior(['S','K'],'x','x')

produces the solution SKx, which means that x can be replaced with anything and the resulting combinator still is solution. Hence SKK as well as SKS (as well as SK(KK) etc) represent the identity.

Similarly,

cl.eqRndSearchBehavior(['S','K'],'x','xx')

may produce S(SKx)(SKy) containing two free variables that may be replaced independently.

createGpSearchBehavior(base,varList,out)

Creates an object, let us call it gpSearch, that uses an evolutionary approach (Genetic Programming) to find a combinator that satisfies the input/output behavior specified through parameters varList and out. The combinator sought is assembled using the combinators given by parameter base, an array of combinator symbols.

Generation i+1 is produced by applying crossover to individuals selected from generation i via tournament selection. For further details, in particular a description of the fitness measure, consult the following publications:

• Solving Problems of Combinatory Logic with Genetic Programming, Second Annual Genetic Programming Conference (GP-97), July 13-16, 1997

• Evolving Combinators, Fourteenth International Conference on Automated Deduction (CADE-14), July 13-17, 1997

The following functions can be called on gpSearch to start, continue, or restart the search, as well as to obtain information on the current state of the proof search:

• rerun(options): starts or restarts a search, discarding previous runs (if any). Options for run and rerun may be supplied as an object where the following properties are recognized:

  • popSize: the number of individuals in each generation (population size); default is 100

  • maxGen: the maximal number of generations; note that the initial (random) generation is generation 0; default is 25

  • minLength: the minimal length (at least 2) of combinators in the inital (random) generation; default is 2

  • maxLength: the maximal length of combinators in the inital (random) generation; default is 20

  • tournamentK: parameter k of tournament selection (tournament size); default is 10

  • tournamentP: parameter p of tournament selection (probability); default is 0.5

  • maxSteps: the maximal number of rewrite steps taken during fitness evaluation; default is 20

  • minIndiLen: the minimal length of a combinator before it incurs a fitness penalty; default is 2

  • logger: a function that accepts a string as a parameter and logs it in an appropriate way (the amount of data logged is determined by property logLevel); in the simplest case use logger: console.log; default is no logging (logger is undefined)

  • logLevel: the log level (a number ranging from 0 to 2) that determines the degree of detail of logging activities (logging takes place only in the presence of a logger, of course); as usual a bigger number means more data logged; default is 0 (nothing will be logged)

• run(options): starts or resumes a search, continuing from where the previous run stopped (if any); run and rerun are identical if no run was executed before. Otherwise run ignores option popSize because it is not possible to modify the population size when resuming a search. Obviously options minLength and maxLength are also ignored as there is no need for a random generation of individuals when resuming a search.

• getState(): returns the current state of the search; it is undefined if neither run nor rerun was ever called. Otherwise it is either the string 'found' or 'failed'.

• getPopulation(maxSteps): returns the current population as an array of strings, each string representing an individual, i.e. a combinator; parameter maxSteps is optional. If it is given every individual is rewritten, but not with more than maxSteps rewrite steps. If parameter maxSteps is omitted no rewriting takes place. Note that any negative number for maxSteps imposes no limit on the length of the rewrite chains, which may produce inordinately long or possibly infinite rewrite chains that will crash your Nodejs application. Note also that the return value of this function is undefined if neither run nor rerun was ever called.

The return value of run and rerun is an object with the following properties:

• state: a string indicating the reason for termination, which can be either 'found' or 'failed'

• timeElapsed: the time elapsed as a human-readable string

• hrtimeElapsed: the time elapsed in process.hrtime format

• statistics: an object that provides statistical data regarding the search through its properties

  • generations: the number of the last generation

  • rndIndividuals: the number of randomly generated individuals (for generation 0)

  • individuals: the total number of individuals (including random ones)

  • crossovers: the number of crossover operations

  • fitnessEvals: the number of fitness evaluations (of individuals)

  • minIndiLenPenalties: the number of fitness penalties due to falling short of the minimal length requirement

• solution: the solution (a combinator as a string); this property is available only if a solution was found

Example:

var r = cl.createGpSearchBehavior(['S','K'],'xy','y(xxy)').run({popSize:1000});

searches for a combinator Q consisting of S and K so that Qxy = y(xxy). The result object r holds the information described above.