Alternative application semantics¶
Note
This section takes a different approach compared to the original PLAI second edition. Reasons – Lazy application is dealt with well in PLAI already, so please refer to that. I don’t think students gain much by working through the “reactive” application semantics from a PL perspective. Visual tools such as Excel, Max/MSP or PureData are better models of this mode than any textual programming language or sub language. If students are to learn it, it would probably be to learn that it isn’t a great idea to pursue in a textual PL, despite possible conceptual elegance of the original Fran. I’m choosing to do searching a little differently due to doing type systems afterwards. I had not intended to do type systems due to time constraints but am trying to see if this change of approach can help with the constraint of a trimester system.
Solving for goals¶
One paradigm for program execution (function application) is to consider “variables” to be first class entities you can pass to your functions. Variables start off with low information content and as your function progresses, more information is added to them. By “information” here, we’re not talking about adding bits of data, but in the sense that a variable may initially be defined to take one of several values in a given set and as the program progresses, the size of this set is progressively reduced, thereby making the variable more precise about its values.
The simplest version of that process of adding information is to have variables be initially in an “Unknown” state and later on as the program progresses, they may transition to a “Known” state getting bound to some value, after which the value cannot be changed.
The purpose of a program in this paradigm is to start off with a set of variables (at least some of them) in an “unknown state” and when the program finishes, at least some of them become known – or “bound” to values. Furthermore, we consider the program to produce one or more such possible set of bindings of the program’s variables. We’ll look at how we can compute this.
Let’s define a value type that represents this idea of a “variable”. We’ll further give our variables some string name that we can recognize them by.
(struct Var (name) #:transparent)
; That gives us Var, Var? and Var-name
We’ll represent the idea of a set of bindings for our variables using our usual “association list”, with variables as keys and values which can be either variables themselves or ordinary values.
Question
Our “bindings as an association list” representation permits the occurrence of mutiple bindings for a single variable. Reflect on whether that is desirable. What do you think?
We’ll constrain our bindings list such that a particular variable can only
occur in the key position in one of the entries. i.e. We’re not permitted to
indicate different bindings for a variable in the same bindings set. Given that
we’re making variables using Var
, we can lookup our variables in the
bindings list using assv
.
(define v1 (Var "one"))
(define v2 (Var "one"))
(display (eqv? v1 v2)) ; Shows #f, which is what we want. We want each of our
; Var values to be distinguishable irrespective of their
; names.
Given that a set of bindings may indicate that a variable A
(we’ll use
the convention of referring to variables using capitalized names) is is bound
to another variable B
, we need a procedure to determine the value at the
end of such a chain of “bindings”. We’ll call this procedure walk
.
(define (walk var bindings)
(let ([m (assv var bindings)])
(if m
(if (Var? (second m))
(walk (second m) bindings)
(second m))
; We let a var be itself if it isn't found in bindings.
; This also lets us deal with the case where A is bound
; to B but B does not appear as a key in the bindings.
var)))
Now let’s consider what kinds of assertions we can make about two “things” in
our system. A “thing” being a variable or a value. If we assert that
<thing1> = <thing2>
, what effect would we expect such an assertion to
have on our current set of bindings?
A = A
– i.e two variables are declared to be equal and they are the same. This also has no impact on our bindings set and we stay happy.A = 32
– i.e. first thing is a variable and the second thing is a value. In this case, we’d like to make note of this additional information in our bindings set. We’ll therefore add an entry for it there.A = B
– i.e. two different variables are declared to be equal to each other. We can add a binding to this effect to our set. Question: Should we addA
bound toB
orB
bound toA
?32 = A
– same as the previous case, we add a bindings forA
to our bindings set.32 = 32
– i.e. both things are values that are equal to each other. In this case, we’re happy. No contradictions. And our bindings doesn’t change one bit.
In any other case (such as 2 = 3
), the assertion will fail. Let’s capture all
of these in a function – unify
. This process we described above, that
takes an assertion and augments a set of bindings with new information that reflects
the facts being asserted is called “unification” in the case where the assertion is
made via equality.
; unify tries to assert A = B in the context of the given
; bindings. It produces an augmented set of bindings if the
; assertion provided new information about variables involved.
(define (unify A B bset)
(let ([av (walk A bset)]
[bv (walk B bset)])
; By taking the walked end values for both LHS and RHS
; of the unification, we're guaranteed that both never
; appear as the key in our bindings set.
(cond
[(and (Var? av) (Var? bv) (equal? av bv))
bset] ; Handles 1
[(Var? av) ; Handles 2 & 3
(extend av bv bset)]
[(Var? bv) ; Handles 4
(extend bv av bset)]
[(eq? av bv) ; Handles 5
bset]
; Produce #f in all other cases.
[else #f])))
(define empty-bset empty)
(define (extend key val bset)
(cons (list key val) bset))
Goals¶
We earlier stated that our “program” in this model has the task of figuring out
which possible assignments to variables makes sense – i.e. is consistent with
a set of declarations about their properties. Since we’re talking about
“possible assignments to variables”, we’ll model the result of our program
as a list of bindings. i.e. if we call our set of bindings a BSet
,
our program is expected to produce a (listof BSet)
.
This is giving our program a uniform interface of BSet -> (listof BSet)
.
We’ll call such a program a “goal”, since it is faced with the goal of finding
one or more possible sets of assignments to variables that is consistent with
some logic. In this case, if our goal cannot be met, the result is expected to
be an empty list indicating that there is no possible set of bindings that is
consistent with the goal.
Let’s now consider the simplest of such programs – a declaration of equality
between two things … which is unify
in a different clothing.
(define (eq A B)
(λ (bset)
(let ([b (unify A B bset)])
(if b
(list b) ; Singleton list of bindings.
empty))))
It is useful to look at possible ways to combine (listof BSet)
values.
If we concatenate two such lists, we’re saying that the BSet
values
belonging to either of the two lists are permitted as outcomes. This is like an
“or” (a.k.a. “disjunction”) and we can exploit that.
(define (disj goalA goalB)
(λ (bset)
(append (goalA bset) (goalB bset))))
So we have “or”. How do we get an “and” (a.k.a. “conjunction”) of two goals? Calling the first goal on bindings can produce a list of possible bindings, but we then need to use the second goal to examine whether it is consistent with any of them at all. To do that, we can call the second goal on each of the result bindings, each of which will produce a list of bindings that are consistent with goalB and the result bindings we applied it to. Then we concatenate all those lists to get the result. That way, if the second goal fails on all of them, it will indicate that by returning an empty list in each case and when we concatenate them all, we’ll get an empty list as the result. If even one of them succeeded, the we’ll get a non-empty list and can go home happy.
(define (conj goalA goalB)
(λ (bset)
(apply append (map goalB (goalA bset)))))
Exercise
Go off now and study how the above definition of conj
satisfies our
descripion of “and” in the preceding paragraph. What properties do we
expect such a conj
to satisfy, logically? Does it satisfy them? In
particular, why should we expect (conj goalA goalB)
to produce the
same set of possibilities produced by (conj goalB goalA)
?
Note that eq
produces a goal based on a statement about variables and
values, and disj
and conj
take goals as arguments and produce
a goal as their result. So we can call them “combinators”.
We can now describe some simple interesting searches.
(define a (Var "a"))
(define b (Var "b"))
(define goal (conj (eq a 1)
(disj (eq b 2)
(eq b 3))))
(writeln (goal empty-bindings))
Exercise
Go off and run the above code to see what you get as the result.
This task of introducing new variables can perhaps be automated a bit.
We define a new primitive called fresh
which creates new variables
and makes a goal of them.
(define (fresh varnames goal-proc)
(if (equal? (procedure-arity goal-proc) (length varnames))
(let ([vars (map Var varnames)])
(apply goal-proc vars))
(raise-argument-error 'fresh
"varnames should provide a name for each argument of the goal procedure"
(list varnames goal-proc))))
Now, we can code our simple example as –
(define goal (fresh '(a b)
(λ (a b)
(conj (eq a 1)
(disj (eq b 2)
(eq b 3))))))
(writeln (goal empty-bindings))
Structural unification¶
So far, our “unification” procedure only dealt with simple values and variables. We can extend this mechanism to also consider matching, say two cons pairs. In that case though, we’d expect the corresponding parts of the cons pairs to unify and hence unify becomes a recursive procedure.
Note
What are possible problems when we try to do this? Think through
possible cases one might encounter when calling unify
with such
cons pairs to be unified and what we’re supposed to do to them. Below
are spoilers, so do that now!
What is supposed to happen when we ask for a variable to be unified with a cons pair which itself contains this variable? If we wish to be strict about it, we can declare failure when we encounter such a case. If we decide on this, we need to add an “occurs check” to our unify cases. Otherwise we need to consider the possibility that the unification request is intended to produce an infinite circular data structure as the variable’s resultant binding and tip toe around that possibility without catching ourselves doing an infinte loop.
We’ll chicken out and do the simple “don’t let that happen” approach. You can try the other option as an exercise (heheh!).
(define (occurs? var expr)
(if (pair? expr)
(or (occurs? var (car expr))
(occurs? var (cdr expr)))
(eq? var expr)))
We now use this to modify our unification procedure to support pairs.
(define (unify A B bset)
(let ([av (walk A bset)]
[bv (walk B bset)])
; By taking the walked end values for both LHS and RHS
; of the unification, we're guaranteed that both never
; appear as the key in our bindings set.
(cond
[(and (Var? av) (Var? bv) (equal? av bv))
bset] ; Handles 1
[(and (Var? av) (not (occurs? av bv))) ; Handles 2 & 3
(extend av bv bset)]
[(and (Var? bv) (not (occurs? bv av))) ; Handles 4
(extend bv av bset)]
[(and (pair? av) (pair? bv) (not (empty? av)) (not (empty? bv)))
; We have to use car and cdr here instead of first
; and rest because the latter two require the
; pair to be a non-empty list ... which is not a
; constraint we require to be met by the two pairs.
(let ([b2 (unify (car av) (car bv) bset)])
(unify (cdr av) (cdr bv) b2))]
[(eq? av bv) ; Handles 5
bset]
; Produce #f in all other cases.
[else #f])))
Such a structural unification is way more powerful than the ordinary atomic value unification we did earlier. Check out the simple example below and make more of your own –
(define goal
(fresh '(a b)
(λ (a b)
(eq (cons a b) (list 1 2 3 4 5)))))
(writeln (goal empty-bindings))
Exercise
Thoroughly thrash out various possible usages of such structural unification. What sets of arguments will you try it with and what would you expect? How might you extend it even further?
Question
Why didn’t we consider implementing a not
since we implemented “and”
and “or” as conj
and disj
respectively?
Reference: The approach above specifies a small goal language called microKanren. You may also want to go through A Gentle Introduction to microKanren.
Generalizing “pair”s¶
In the latest version of unify
above, we supported unification of two
“pair” structures. What if we want to generalize that and support arbitrary
struct
-like … structures?
To do that, see what is special about a struct
that we define ourselves.
The main component of the definition that identifies a structure is its name,
and the fields are a list of values. We could model the structure’s name as a
constant symbol and the fields as … a list of values! While Racket’s
structures have fixed arity, there is no real need to restrict ourselves to
fixed arity structures for the purpose of unification because we’ve already
implemented unification between lists!
So, let’s model such an arbitrary structure as a Racket struct
. We
borrow a term used in Prolog – “functor” – for this purpose. In Prolog, in an
expression of the form word(arg1,arg2,...)
the word
is referred
to as a “functor”.
(struct FExpr (functor args))
; functor is a symbol
; args is a list of values.
When our new unify
tries to match two functors, we’re going to demand
that their name
parts match exactly and both be symbols (and,
in particular, not variables). For the fields themselves, we can bank on our
support for matching two lists.
Design question
Should we permit matching a variable against an entire sublist of fields of
a particular functor? i.e. Should our unify support unification between
(FExpr 'f (cons (Var "one") (Var "two")))
and (FExpr 'f
(list 1 2 3 4))
? What are the consequences of permitting versus not permitting
such a unification?
We’re going to assume that we cannot do “partial list of fields” matching between
two functors. We want the fields to match in count. i.e. We’re going to demand that
fields
actually be a list and not merely be a sequence of nested conses.
(define (valid-fexpr? f)
(and (FExpr? f)
(symbol? (FExpr-functor f))
(list? (FExpr-args f))))
(define (occurs? var expr)
(cond
[(pair? expr)
(or (occurs? var (car expr))
(occurs? var (cdr expr)))]
[(valid-fexpr? expr)
(ormap (λ (e) (occurs? var e)) (FExpr-args expr))]
[else (eq? var expr)]))
(define (unify A B bset)
(let ([av (walk A bset)]
[bv (walk B bset)])
; By taking the walked end values for both LHS and RHS
; of the unification, we're guaranteed that both never
; appear as the key in our bindings set.
(cond
[(and (Var? av) (Var? bv) (equal? av bv))
bset]
[(and (Var? av) (not (occurs? av bv)))
(extend av bv bset)]
[(and (Var? bv) (not (occurs? bv av)))
(extend bv av bset)]
[(and (pair? av) (pair? bv) (not (empty? av)) (not (empty? bv)))
; We have to use car and cdr here instead of first
; and rest because the latter two require the
; pair to be a non-empty list ... which is not a
; constraint we require to be met by the two pairs.
(let ([b2 (unify (car av) (car bv) bset)])
(unify (cdr av) (cdr bv) b2))]
[(and (valid-fexpr? av)
(valid-fexpr? bv)
(equal? (FExpr-functor av) (FExpr-functor bv))
(equal? (length (FExpr-args av)) (length (FExpr-args bv))))
; We already know how to unify lists!
; Here we're relying on the previous cond case, which
; works with general nested pairs and hence also works with lists
; ... which is what we're limiting ourselves to in this case.
(unify (FExpr-args av) (FExpr-args bv) bset)]
[(eq? av bv)
bset]
; Produce #f in all other cases.
[else #f])))
Questions
What can you imagine using the above extension for? After all, programming languages are there to wish our imaginations into existence. So what wizard powers did the above extensions to unify (relative to the first cut) give you? What kinds of goals would you try it on?
Hint: For one thing, you can model pair
itself using
(FExpr 'cons (list <head> <tail>))
.
Prolog¶
Prolog is a language in which key ideas we discussed above – unify
, the
notion of “goals”, and disj
/ conj
as “goal combinators” – are
available as language level primitives.
Note
This is a bit of a lie. While logically Prolog tries to do what we presented in this section, it doesn’t do it using the same mechanism. The mechanism employed is “backtracking depth-first search”, similar to what we did in the last section on generators. The choice of mechanism has some interesting conseqences for the language design, with Prolog getting some not-quite-logical behaviours as a consequence of turning this into a practical language (which it certainly is) and our implementation being that much purer, but far less efficient than Prolog for large problems … can you see why it can be inefficient?
unify
is simply=
in Prologdisj
between goals is represented as an infix operator;
conj
between goals is represented as an infix operator,
(FExpr 'functor (list Arg1 Arg2 ...))
is represented asfunctor(Arg1,Arg2,...)
in Prolog.Prolog has “predicates” which express a goal in terms of subgoals using combinators like
disj
andconj
– i.e.,
and;
operators. These predicates are declared in a function-like manner where formal parameters first get unified with actual parameters before the subgoals are solved. (We’ll see examples below) Predicates have only two results – either they succeed and produce a set of bindings required for them to succeed, or they fail.
As a notational convenience, identifiers that start with a capitalized letter
– like Result
, Any
– are variables and identifiers that start
with a lower case letter – like some
, disj
– are ordinary
symbols, much like Scheme symbols.
Note
SWI Prolog is a free and rich+powerful Prolog engine you can play with. You can write web services with it too if you want to, write solvers for some kinds of optimization problems, use it as a sophisticated search engine on a database of facts and so on.
Examples¶
Consider the following block of code. Place it in a file named presence.pl
.
Then run swipl
and on the REPL type [presence].
(including the period
at the end), followed by return key. Now the module is loaded for you to play with.
:- module(presence, [is_in/2]). % A standard module declaration. Ignore this for now.
% Declare some facts. Facts are simply predicates that are declared to be true.
is_in(srikumar, chennai).
is_in(chennai, tamilnadu).
is_in(tamilnadu, india).
% This predicate depends on other subgoals being met.
% Here we're saying that is A is in C and C is in B, then A is in B.
is_in(A, B) :-
is_in(A, C), % NOTE: comma here means "conjunction" -- i.e. "and".
is_in(C, B).
After loading the module, try the following in the REPL -
?- is_in(tamilnadu, chennai).
false
?- is_in(chennai, X).
X = tamilnadu <hit ; for other possible answers>
X = india <hit ; now>
?- is_in(X, tamilnadu).
X = chennai;
X = srikumar
So you can see it can provide all permissible answers to the questions you ask,
and much of this is based on unify
, disj
and conj
as
language primitives!
You can play with Prolog’s unification right on the REPL -
?- A = 5.
?- 5 = A.
?- some(X) = some(other).
?- [1,2,B] = [A,2,C]. % We have Prolog lists on both sides here.
?- A + B = 2 + 3. % Surprise! Why? Find out through experiments.
?- A + B = 5 - 3. % Surprise! Why? Find out through experiments.
?- plus(num(5), minus(num(10),num(1))) = plus(A, minus(num(10),B))
Our interpreter expressed in Prolog¶
We can actually build our calculator language in Prolog like below –
:- module(interp, [interp/2]).
interp(num(X), Result) :-
Result = X.
interp(add(A, B), Result) :-
interp(A, RA),
interp(B, RB),
Result is RA + RB. % Note "is" instead of "=" actually does calculation.
interp(sub(A, B), Result) :-
interp(A, RA),
interp(B, RB),
Result is RA - RB.
interp(mul(A, B), Result) :-
interp(A, RA),
interp(B, RB),
Result is RA * RB.
Exercise
Study the above Prolog module source and compare it with our Scheme based interpreter
for the arithmetic language. How is the recursive evaluation handled in both places?
See how we use unification here where we used match
in Racket?
Now try the following after loading the above module.
?- interp(add(num(10), mul(num(3), num(4))), Result).
Adding functions to our interpreter¶
To add functions to our language, we’ve seen that we need three things -
A term to represent an “identifier”
A term to represent “function application”
A term to represent a “function expression”
We also need to introduce the idea of a “evaluation environment” that keeps track of bindings between identifiers and values that we should substitute for them in calculation. We also have to extend our interpreter to support more than just “number” as a value type.
So we need to add the following -
:- module(interp, [interp/3]).
interp(_, num(X), num(Result)) :-
Result = X.
interp(Env, add(A, B), num(Result)) :-
interp(Env, A, num(RA)),
interp(Env, B, num(RB)),
Result is RA + RB. % Note "is" instead of "=" actually does calculation.
interp(Env, sub(A, B), num(Result)) :-
interp(Env, A, num(RA)),
interp(Env, B, num(RB)),
Result is RA - RB.
interp(Env, mul(A, B), num(Result)) :-
interp(Env, A, num(RA)),
interp(Env, B, num(RB)),
Result is RA * RB.
interp(Env, id(X), Result) :-
atom(X),
member(X = Result, Env).
interp(DefnEnv, fun(ArgSym, Body), fun(DefnEnv, ArgSym, Body)).
interp(Env, apply(Fun, Arg), Result) :-
interp(Env, Fun, fun(DefEnv, ArgSym, Body)),
interp(Env, Arg, ArgVal),
interp([ArgSym = ArgVal|DefEnv], Body, Result).
The expression [ArgSym = ArgVal|DefEnv]
adds a term ArgSym = ArgVal
which is a pair of values along with the functor =
, to the head of the
environment list DefEnv
.
Using =
as the functor helps readability but could be confusing about
whether any binding is happening in prolog. To clarify that, you could’ve
used any functor name, for example, you can use bind
like this too –
[bind(ArgSym,ArgVal)|DefEnv]
– as long as you also modify the
interpretation of id(X)
to use member(bind(X,Result), Env)
instead of member(X = Result, Env)
.
Exercise
Add booleans and conditional expressions to this interpreter.