Warning: preg_match() [function.preg-match]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 1384
Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700
Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707
Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700
Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707
It’s been a while now since the last post in my little series on Kalami, but I’ve finally polished the code for evaluating programmes as I wanted to. Overall, it’s not that different from the wellformed
code of the previous post; in fact, the most challenging aspect is how to enumerate all guesses.
As earlier, we’re dealing with statements, conditions, and expressions. The first one is the tricky one, so to start off simple I’ll first look at the other two. The full source code is available in the evalwoa branch on GitHub.
Assuming bindings in environment env
for all identifiers in an expression expr
, it may be evaluated straight-forwardly by the following recursive function eval_expr
:
let rec eval_expr env expr = match expr with ExprNumber(n) -> n | ExprVariable(id) -> List.assoc id env | ExprProduct(expr1, expr2) -> let val1 = eval_expr env expr1 in let val2 = eval_expr env expr2 in val1 * val2 | ExprDivision(expr1, expr2) -> let val1 = eval_expr env expr1 in let val2 = eval_expr env expr2 in val1 / val2 | ExprSum(expr1, expr2) -> let val1 = eval_expr env expr1 in let val2 = eval_expr env expr2 in val1 + val2 | ExprSubtraction(expr1, expr2) -> let val1 = eval_expr env expr1 in let val2 = eval_expr env expr2 in val1 - val2 | ExprPower(expr1, expr2) -> let val1 = eval_expr env expr1 in let val2 = eval_expr env expr2 in power val1 val2
Note first that since env
is just a list of pairs binding identifiers to integers
let env = [ (id1, n1); (id2, n2); ... (idk, nk) ];;
we may extract the latter using built-in function List.assoc
as in case ExprVariable
. Next, note that there’s no built-in function for integer exponentiation, hence the power
function used in case ExprPower
is implemented in evaluation.ml as a tail recursive repeated squaring (initially it was using the naive approach, but since I did do my PhD in crypto, this was one of the small changes needed; see separate file power.ml for the various implementations).
Evaluating condition cnd
is similar, with the small difference that for one reason or another (purist perhaps) I used the prefix notation for function invocation here:
let rec eval_cnd env cnd = match cnd with CndTrue -> true | CndFalse -> false | CndEqual(expr1, expr2) -> let val1 = eval_expr env expr1 in let val2 = eval_expr env expr2 in (=) val1 val2 | CndLessthan(expr1, expr2) -> let val1 = eval_expr env expr1 in let val2 = eval_expr env expr2 in (<) val1 val2 | CndNegation(cnd) -> let val1 = eval_cnd env cnd in (not) val1 | CndOr(cnd1, cnd2) -> let val1 = eval_cnd env cnd1 in let val2 = eval_cnd env cnd2 in (||) val1 val2 | CndAnd(cnd1, cnd2) -> let val1 = eval_cnd env cnd1 in let val2 = eval_cnd env cnd2 in (&&) val1 val2
For statement stmt
it finally gets a bit more interesting. Cases StmtLet
and StmtIf
are straight-forward, as are StmtAccept
and StmtReject
which respectively return the current environment and None
. However, for a guessing statement it’s a bit more involved. If the guess has an upper bound then we may just try all possibilities as in case StmtGuessLowerUpperBound
below. But this will of course not work when no upper bound is specified since an inner guess will prevent outer guesses from ever increasing. As an example, consider programme:
guess x in guess y in if x == y+1 then accept otherwise reject
which has solution [ ("x", 1); ("y", 0) ]
, yet if we first let x=0
and then use the strategy of enumerating all values for y
then we’ll never make it back to incrementing x
.
Instead, for a programme with n (unbounded) guesses, i.e. guesses without an upper bound, the simple strategy used here is to enumerate all n-arity integer tuples in an outer loop, and for each evaluate the main statement with a second environment guesses
linking the tuples with the identifiers of the (unbounded) guesses. Statements may then be evaluated as follows, using an initial empty environment env
for the main statement:
let rec eval_stmt env guesses stmt = match stmt with StmtLet(id, expr, stmt) -> let expr_value = eval_expr env expr in let env' = (id, expr_value) :: env in eval_stmt env' guesses stmt | StmtIf(cnd, stmt_true, stmt_false) -> let cnd_value = eval_cnd env cnd in if cnd_value then eval_stmt env guesses stmt_true else eval_stmt env guesses stmt_false | StmtGuess(id, stmt) -> let guess = List.assoc id guesses in let env' = (id, guess) :: env in eval_stmt env' guesses stmt | StmtGuessLowerBound(id, lower_bound_expr, stmt) -> let lower_bound = eval_expr env lower_bound_expr in let guess = List.assoc id guesses in if guess < lower_bound then None else let env' = (id, guess) :: env in eval_stmt env' guesses stmt | StmtGuessLowerUpperBound(id, lb_expr, ub_expr, stmt) -> let lower_bound = eval_expr env lb_expr in let upper_bound = eval_expr env ub_expr in let rec helper guess = let env' = (id, guess) :: env in let result = eval_stmt env' guesses stmt in match result with None -> if guess < upper_bound then helper (guess + 1) else None | Some(_) -> result in helper lower_bound | StmtAccept -> Some(env) | StmtReject -> None
where we see that in cases StmtGuess
and StmtGuessLowerBound
the guess performed in the outer enumeration is simply added to the environment.
The only thing missing is hence the outer enumeration. First we have a simple function collecting identifiers:
let rec get_unbounded_guesses stmt = match stmt with StmtLet(_, _, stmt) -> get_unbounded_guesses stmt | StmtIf(_, stmt_true, stmt_false) -> (get_unbounded_guesses stmt_true) @ (get_unbounded_guesses stmt_false) | StmtGuess(id, stmt) -> id :: (get_unbounded_guesses stmt) | StmtGuessLowerBound(id, _, stmt) -> id :: (get_unbounded_guesses stmt) | StmtGuessLowerUpperBound(_, _, _, stmt) -> get_unbounded_guesses stmt | StmtAccept -> [] | StmtReject -> []
Next is a projection function project arity number
performing a one-to-one mapping of an integer into a integer tuple with the given arity (see also projection.ml). The code for this gets a bit messy so I won’t give it here, yet the main principle is to partition the digits in number
such that for instance:
# project 3 123456;; - : (int * int) list = [(3, 14); (2, 25); (1, 36)]
It could definitely be done in other ways (as well as optimised), but I vaguely remember going with this simply because of it keeping the projected numbers slightly “balanced”.
Finally, we put this together to obtain:
let eval stmt = let unb_guess_ids = get_unbounded_guesses stmt in if (List.length unb_guess_ids) > 0 then let projector = project (List.length unb_guess_ids) in let rec helper number = let projection = projector number in let guesses = List.combine unb_guess_ids projection in let result = eval_stmt [] guesses stmt in match result with None -> helper (number + 1) | Some(_) -> result in helper 0 else eval_stmt [] [] stmt
that will indeed find a solution to the example programme from above!
While this is now a working interpreter, it does have its shortcomings when used without any kind of static analysis thrown in. For example, on programme:
guess x in reject
the interpreter will enter an infinite loop, despite the fact that the programme obviously doesn’t have any solutions. Fixing this will be the topic of the next post.