Exporting premises for the environment

With the introduction of the environment, we will want to export a second trigger proposition. The original trigger proposition allows us to evaluate a tree in an initially empty environment. However, we also want to export a proposition to allow us to evalute a tree in an existing environment. From scratch then, we can prove the first proposition given a tree and an empty initial environment (which spares us the effort of constructing an environment tree by hand). Then, we may use the resulting environment as the initial environment in a subsequent proof of the second proposition, and so on.

The first exported premise thus requires only the initial tree for the computation:

export env[] |- exp : I, env as init_eval_exp(exp) = env;

Note that the function init_eval_exp takes one argument, a tree, and returns the calculated environment.

We may go one step further. Rather than starting with an empty environment, we initialize it so that it contains the variable RESULT whose value is zero. After the computation, we update this variable with the result. We modify the export clause accordingly:

export 
   env[pair(variable "RESULT", integer 0)] |- exp : I, env  &
   UPDATE(env |- variable "RESULT", I : env')
  as init_eval_exp(exp) = env';

The second exported premise handles the non-empty environment:

export env |- exp : I, env' as full_eval_exp(exp, env) = env' ;

Note that in this case, the function full_eval_exp takes two arguments and returns the modified environment. This premise does not guarantee that the result of the evaluation will appear in the environment. For this, we explicitly assign the result to the variable RESULT as before:

export  
   env |- exp : I, env' &
   UPDATE(env' |- variable "RESULT", I : env'')
  as full_eval_exp(exp, env) = env'';

N.B. We added an environment to some Typol rules without updating the judgement that allows Typol to type check them. We do so below.