All about control.
May start at a lower level. An applicative system is simply a system in which objects can be applied to other objects. A simple example of an applicative system is bash. ls | More It can be assumed that they are in some kind of environment, and that the above means ls in the environment, and then do more. In applicative notation, this is more @ (ls @environment) However, more complex things could be done, such as ls | grep template | More So, now in applicative notation it is more @ ((grep @pattern) @ (ls @environment)). Check out the grep @ pattern. Grep is applied to a pattern that returns the program to match that pattern as a result of ls. This is the point of application, the application of the program to the arguments, the creation of new programs from "atomic" (so-called built-in) programs. However, we cannot do too much programming with just a primitive application or built-in ones. We need a way to structure our input and apply our primitives to our input.
Here is the lambda. Using lambda, you can generalize (grep @ pattern) To apply grep to any input, (grep @X) However, we must have a way to get grep input. So we usually use functions. f (X) = grep @X The above process is called abstracting the argument. But there is no reason to think that the name f is special, so we have the syntax: lambda X. grep @X Then the lambda X. grep @X can be applied to the input and the input will be replaced in the body and evaluated. However, the replacement may become erratic, the associated variables can be difficult to implement on the machine. SKI (or B, C, K, W) makes it possible to create lambda material without substitution and instead simply replaces the application.
Recall, the application is what everything is about. It is very convenient to reason at the level of application of the program to something (perhaps to another program). Lambda calculus makes it possible to structure the input and application of programs to arguments. SKI makes it possible to make lambda without explicit substitution.
It should be noted that the abbreviation SKI is inherently lazy, so you may need some consideration in the actual use of SKI to structure your application. Indeed, the arguments can now be fully evaluated and can also be a partial application. You can get around this with type theory and only evaluate the program at its input if the program is in the main position of the application. Ie, if you write with closed lambda terms translated into SKI, then p @ arg1 @ .... It must be if p is a primitive program, then the rewriting is complete, and therefore all arguments 1) are available, 2) are fully appreciated. However, I have not proved this, and this may not be true with a sufficiently strong type theory ...
Haskeller
source share