pathterminuspages/projects/aboutcontactabout me

Evaluation

Untyped Lambda Calculus #4 :: 17-03-2019

Contents
 -Untyped Lambda Calculus in JavaScript
 -Parser
 -Semantics
 @Evaluation
 -Testing
 -Usage

Evaluation Strategies

As mentioned in Types and Programming Languages we can evaluate using either the call-by-value strategy or the call-by-name. For now only the call-by-value strategy is implemented. It might be an idea to implement both later on so one can see the different outcomes of the two. Evaluation strategies are further described here.

Scopes and Closures

Another thing to take into consideration is scopes and especially closures. The latter can be difficult to deal with. The idea of closures is as follows. Say we have some function in which we define another function. Now this inner function captures the current scope in its closure. In JavaScript it can be illustrated as follows:

var fun1 = function(){ var a = "1"; var b = "2"; return function(c){ return a + c; }; }; alert(fun1()("3")); // will alert 13

So as soon as fun1 is evaluated it will return a function that has both var a and var b in its closure. This might not seem useful, but I assure you that it is. Functions in functional languages, like the λ-calculus, have closures. Therefore we include this feature.

The code example above exploits one more feature, namely partial evaluation. In the λ-calculus a function can be partial evaluated, this is called Currying. The idea is as follows: each function takes exactly one argument. So in order to have more-than-one-argument-functions we let the first function return a new function that takes yet another argument. Each function that returns another function has to capture its argument within its closure. In JavaScript we can express this idea as follows

var fun = function(a){ return function(b){ return function(c){ return a + b + c; }; }; }; //partial call fun var part1 = fun(1); //part1 evaulates to a function with [a -> 1] in its scope var part2 = part1(2); var part3 = part2(3); //part3 evaluates to 1 + 2 + 3 = 6

Closures are a clone of the current scope added whenever some term is reduced to an abstraction. That is when we bind an abstraction to some value during let-bindings or when substituting. Or if the final term returned is an abstraction.

There are two different kinds of scope strategies:

  1. Static Scoping: What most languages posses. When searching for a substitution of a variable the inner scope in which the variable is defined are searched. Then the next and so on until the global scope are reached, or until a substitution is found. This can be done quite simple: create a global dictionary (often called a store). Whenever some function body is entered save whatever value (if any) that is stored with the same name as the parameter of this function. Now overwrite that value in the store (this is called shadowing). When the current function returns, reinsert the saved value and discard the one inserted when the function was entered.
  2. Dynamic Scoping: This differs from static ditto in that variables within abstractions are substituted according to the scope of the calling function.

For now this version of λ-calculus only deals with static scoping. Dynamic scoping might be implemented as future work.

Evaluation Strategies Revisited

The call-by-value and call-by-name strategies was mentioned first in this chapter. Both strategies do not reduce within abstractions when the abstraction is not applied. We can list the two

  • call-by-value: We only reduce the outermost redexes. Every time we perform a reduction, we first evaluate the arguments given. That is we reduce the arguments until they are either a free variable or an abstraction. call-by-value is the standard strategy for most programming languages.
  • call-by-name: This is a more exotic way of evaluating. In its purest form arguments are not evaluated during reductions. That is in for example: $$ (\lambda x . x\ a)\ (id\ b) $$ the full tree rooted in application of $b$ to $id$ is substituted into the scope of the abstraction. So every time $x$ is evaluated, it is done so on the whole sub tree.

Optimizations

Look for any under usage.

CommentsGuest Name:Comment: