Repository files navigation

Following is the implementation of an abstract machine in OCaml namelykrivine machine which implementscall-by-name semantics. There exists another abstract machine namelysecd machine which implementscall-by-value semantics, whose code can be foundhere.

Abstract machines got the name abstract because they permit step-by-step execution of programs and also because they omit the many details of real(hardware) machines. They bridge the gap between the high level of a programming language and the low level of a real machine. The instructions of an abstract machine are tailored to the particular operations required to implement operations of a specific source language or class of source languages.

More about it can be foundhere.

The Krivine machine is a simple and natural implementation of the weak-head call-by-name reduction strategy for pure λ-terms. More specifically it aims to define rigorously head normal form reduction of a lambda term using call-by-name reduction. On the other hand Krivine machine implements call-by-name because it evaluates the body of a β-redex before it evaluates its parameter

Call by name is an evaluation strategy where the arguments to a function are not evaluated before the function is called—rather, they are substituted directly into the function body(using the closures) and then left to be evaluated whenever they appear in the function. If an argument is not used in the function body, the argument is never evaluated; if it is used several times, it is re-evaluated each time it appears, which can be optimized more to be evaluated just once and put it over some stack from which it can called everytime there is a need.More about it can be foundhere

For this implementation of krivine abstract machine, we consider a tiny language consisting of expressions, having the key operations of Lambda abstraction (lamba.x e), application of the abstraction (e1(e2)) and also some base operations on integer.

typeexp=Intofint |Varofstring |Absofstring*exp |Appofexp*exp;;

Which can be extended to include operations like addition, subtraction, multiplication, division, absolution of a number on integers, and and, or, not operation on boolean types, and also some comparsion operations like greater than, less than, equal, greater than or equal, less than or equal, and also some conditional statements like if-then-else. The OCaml representations of which on expressions can be defined as -

typeexp=Nil |Intofint |Boolofbool |Varofstring |Absofstring*exp |Appofexp*exp |Absoluteofexp|Notofexp|Addofexp*exp|Subofexp*exp|Divofexp*exp|Mulofexp*exp|Modofexp*exp|Expofexp*exp|Andofexp*exp|Orofexp*exp|Impofexp*exp|Equofexp*exp|GTEquofexp*exp|LTEquofexp*exp|Grtofexp*exp|Lstofexp*exp|Ifthenelseof (exp*exp*exp);;

Whenever we have a list of expressions (say program), we evaluate its each expression by defining it as an closure of the tuple of the expression and the environment closure. For the k-machine we also need an stack of closures.

The type of the above syntax can be defined in OCaml as

typestackCLOS=closurelistandclosure=CLtypeofexp*environmentCLOSandenvironmentCLOS= (exp*closure)list;;

On facing a base closure type, where the expression is a Integer, or boolean, or Nil; we return the some closure type. Whereas, when facing a closure type with a variable in it, we look up the variable in the attached enviornment and if found, we then insert that closure whose expression is the same as we looked up, into its environment and return the closure type. Implementation of suchlookup function can be defined as

letreclookup (e,env)=match (e, env)with| (e, (e1,cl)::c') ->if e1<>ethen lookup (e, c')else(match clwith|CLtype (Abs (x,x1),env) ->CLtype (Abs (x, x1), (e1,cl)::env)|_ -> cl)| (e,[]) -> raiseVariable_not_intialized;;

Now, for abstraction on lambda-calculi, we define this function as

(* val absApplied : closure * closure list -> closure * closure list = <fun>*)

Whenver we face a closure with the expression as an abstraction, we put the 'binding variable' with the closure on the top of the stack, meaning the closure of 'bounded variable', and we return this new closure type. ThisabsApplied function is performing the same functionality as stated above.

letabsApplied (cl,s)=match (cl, s)with| (CLtype(Abs(x ,e),env),c::c') -> (CLtype(e, (Var x ,c)::env), c')| (_,[]) -> raiseInvalidOperation|_ -> raiseInvalidOperation;;

The application of function i.e. e1(e2) can be easily defined as

CLtype (App(e1, e2), env) -> krivinemachine (CLtype(e1, env)) (CLtype(e2, env)::s)

where CLtype is the closure.

All the functionality stated above can be combined to this tiny krivine machine evaluation function.

letreckrivinemachinecl (s:stackCLOS)=match clwith|CLtype (Inti,env) ->CLtype (Int i, env)|CLtype (Varv,env) -> krivinemachine (lookup (Var(v), env)) s|CLtype (Abs(x,e),env) ->let (cl', s')= absApplied (cl, s)inkrivinemachine cl' s'|CLtype (App(e1,e2),env) -> krivinemachine (CLtype(e1, env)) (CLtype(e2, env)::s)

The OCaml code of the krivine machine which various features can be foundhere.

Found a bug or have a suggestion? Feel free to create an issue or make a pull request!

If this code is one of your assignments, I strongly recommend you to try it out first by yourself. Otherwise, feel free to use it if you want to expand the language or for any other purpose.

• This is the official research paper of call-by-name semantic implementing machine -A call-by-name lambda-calculus machine

• Extension of K-Machine and some new features -A Certified Extension of the Krivine Machine for aCall-by-Name Higher-Order Imperative Language