15312: Principles of Programming Languages

Practice Examination
May 7, 2013

There are 16 pages in this examination, comprising 5 questions worth a total of 135 points.
You may refer to your personal notes and to the textbook (Practical Foundations of Programming LanguagesPFPL), but to no other person or source, during the examination.
You have 180 minutes to complete this examination.
Please read each question completely before attempting to solve any part.
Please answer all questions in the space provided with the question.
There are two scratch sheets at the end for your use.

Full Name:
Andrew ID:

Question:
Points:
Score:

Conversions

Monads

Dynamic

Parallelism

Concurrency

Total

25

30

30

25

25

135

Question 1 [25]: Conversions

You may have used Google calculator. Like any calculator, it will do arithmetic calculations for
you. Unlike your typical calculator, it gives you a convenient way to do unit conversions. For
example, you can ask it to compute 12 feet 2 inches + 3.6 meters and it will return 7.3084
meters. You can also ask fancier questions like 12 feet 2 inches + 3.6 meters in fathoms
(the result is 3.996 fathoms the fathom is a British unit of water depth), or to convert mass
values, and even currencies. One thing it will not do is mix incompatible quantities, for example
2 inches + 3 grams. In this exercise, we will study the programming language concepts that
underlie this tool, and then extend it.
We start with a simple language that supports a fixed choice of quantities (here length, mass
and currency), a fixed selection of units for those quantities, and a few useful operations to form
expressions (a measurement in a unit, the sum of two expressions, and the explicit conversion
into a compatible unit). Such expressions are classified by the type float(q) for an appropriate
quantity q; the type scalar classifies the scalar coefficients of units (e.g., 3.6 in 3.6 meter).
Quantities

q ::= length | mass | currency

Types

Units

u ::= meter | inch | fathom | oz | gram | USD | QAR | EUR

Expressions

e ::= n | eu | e1 + e2 | e into u

::= scalar | float(q)

The straightforward static semantics commits all measurements in an expressions to a single

quantity. These rules rely on the judgment u is a q which states that unit u refers to the quantity
q, for example we would have meter is a length.
n : scalar
e : scalar u is a q
eu : float(q)

tp n

tp sc

e1 : float(q) e2 : float(q)
e1 + e2 : float(q)

e : float(q) u is a q
e into u : float(q)

tp pl

tp in

The dynamic semantics extends the standard step evaluation judgment e 7 e0 with a conversion
table X, obtaining e 7X e0 . Actual conversions are performed by the auxiliary conversion
judgment X |= 1 u = k u0 which uses the conversion table X to determine that k units of u0
correspond to one unit of u for example we have X |= 1 fathom = 1.8288 meter. The value
judgment is similarly written e valX and holds for expressions of the form n u.
n u valX
e1
7 X e01
e1 + e2
7 X e01 + e2

val n

e1 valX e2 7X e02
e1 + e2 7X e1 + e02

ev pl1

X |= 1 u1 = k u2

ev pl2

ev pl3

n1 u1 + n2 u2 7X (kn1 + n2 )u2
e 7X e0
e into u 7X e0 into u

X |= 1 u0 = k u
ev in1

n u0 into u 7X (kn)u

ev in2

Given this setup, the language so obtained admits the obvious safety properties, which are
omitted.

Page 2

You will now extend this language with a mechanism to add units and conversion factors
(e.g., the Swedish aln, which is equal to 0.5937 meter), with another mechanism to add
new quantities (e.g., time or temperature), and with scalar functions. The resulting language
extension is as follows:
Quantities

q ::= . . . |

Types

Units

u ::= . . . |

Expressions

e ::= . . . | letq(..e) | letu 1 = e1 in e2 | x | x : scalar. e | e1 e2

::= . . . | some(. ) | 1 2

Here, is a quantity variable and is a unit variable. These operators have the following
meaning: letq(..e) creates a new quantity and a measurement unit for for use inside
expression e; letu 1 = e1 in e2 creates a new measurement unit equal to the value of e1 for
use inside expression e2 ; functions have the usual behavior but their argument is restricted to
scalar values. The creation of a new quantity is witnessed by the type some(. ). (If this
works better for you, feel free to do the later parts of this question to gain practice.)
(a) (8 points) Define the static semantics of this language extension by giving typing rules for
letq and letu. Your typing judgment is now ; ` e : , where the context has the form
1 is a q1 , . . . , n is a qn for distinct unit variables i (note that some qj may be a quantity
variable) and the context contains standard typing assumptions of the form x : scalar.
Solution:

(, is a ); ` e :
; ` letq(..e) : some(. )

tp letq

; ` e1 : float(q) (, is a q); ` e2 :
; ` letu 1 = e1 in e2 :

tp letu

(b) (9 points) Define the dynamic semantics of this language extension by giving evaluation
rules for letq and letu. The evaluation judgment is upgraded to hX, ei 7 hX 0 , e0 i, where
X and X 0 are the conversion tables before and after the evaluation step, respectively. You
may extend a conversion table with entries such as 1aln = 0.5937 meter. The rule for
values shall remain unchanged.
Solution:

(#X)
hX, letq(..e)i 7 h(X, 1 = 1), ei

ev letq

hX, e1 i 7 hX 0 , e01 i
hX, letu 1 = e1 in e2 i 7 hX 0 , letu 1 = e01 in e2 i
(#X)
hX, letu 1 = n u in e2 i 7 h(X, 1 = n u), e2 i

Page 3

ev letu1

ev letu2

(c) (4 points) If you were to implement the language so obtained and you wanted to know
how many Swedish alns correspond to 2.3 fathoms using the expression
letu 1aln = 0.5937 meter in 2.3 fathom into aln
you may get the following answer: 3.874 var7062. The scalar part is correct, but what does
the reported unit, var7062, has to do with alns?? Explain what has happened. Recall that
units are stored in the conversion tables at run-time. (If you have time, suggest a way to
fix the problem.)
Solution: Because aln is a bound variable in this expression, it can be -renamed as
needed. The implementation has simply freshened it into some internal identifier,
here var7062.
Optional answer: There is no perfect solution to this problem. One way is to
extend letu with a third argument, a string, that specifies how the unit should be
printed. This brings up a new problem: what if the user mistakenly redefines the
string corresponding to an existing unit (and possibly get some really weird-looking
results)? How do deal with this? Simply turning a blind eye is a recipe for disaster
given that to this day not everybody agrees on how much a gallon holds, and that
there are over a dozen interpretations of what a league is. Given this confusing reality,
the safest solution may be for an implementation to raise a warning (or an error) if
unit names get redefined.
(d) (4 points) Define an expression of type some(.float() float()) that converts any Fahrenheit temperature into Celsius. The conversion formula is C = 5/9 F 32. Note that it
is not as simple as it looks and that you are likely to use every construct you have just
introduced in the grammar. (Feel free to write scalars as fractions, e.g., 5/9 for the scalar
corresponding to 5/9.)
Solution:
letq(temp.F.letu 1C = 5/9 F in x : scalar. xF + 32 C)

Page 4

Question 2 [30]: Confidentiality

Modernized Algol is based on a monadic type system, which distinguishes expressions from
commands. The meaning of a command depends on the contents of the active assignables,
whereas the meaning of an expression is independent of the assignables. More generally, a
monadic type system may be seen as isolating a notion of a sensitive computation from a
robust computation in such a way that (a) any robust computation may be seen as pro forma
sensitive, and (b) any computation that depends on a sensitive computation is itself deemed
sensitive. In the context of Modernized Algol a sensitive computation is a command, which
may use assignables, and a robust computation is an expression, which does not.
In this question we explore another application of a monadic type system to the problem of
ensuring confidentiality. We postulate that a program has two sorts of input ports and two
sorts of output ports, the public and the private, and we wish to protect the confidentiality of
data arising from the private port. This amounts to ensuring that any data dependent on input
from the private port may not be written to the public port. This can be guaranteed using a
monadic type system that generalizes the one used in Modernized Algol.
We first need two security levels, pub and priv, representing the sensitivity of an operation.
The typing judgement for expressions, ` e : is as usual, but the typing judgement for
commands now has the form
` m @ (r, w)
where r represents the read level, and w represents the write level, of the command m. The
read level is to be thought of as an upper bound on the security level of the reads within m, and
the write level is to be thought of as a lower bound on the security level of the writes within
m. Therefore a public read can be at read level pub or priv, but a private read can only be at
read level priv. Similarly, a private write can occur at write level pub or priv, but a private
read can occur only at write level priv.
(pub, priv) represents the base level of access - only reading from the public channel and
only writing to the private channel.
(pub, pub) is the security level of a program that reads only from the public channel, but
can write to either the public or the private channel.
(priv, priv) is the security level of a program that reads from either the public or the
private channel, but can only write to the private channel.
(priv, pub) would be the security of a program that reads from and writes to any channel
it wants. Such a command may violate confidentiality because it admits commands that
do private reads and public writes.
We introduce an ordering among security levels in which we regard priv as being more sensitive than pub:
pub v pub
priv v priv
pub v priv
This relation is reflexive (l v l), transitive (if l v l0 and l0 v l00 , then l v l00 ), and anti-symmetric
(if l v l0 and l0 v l, then l = l0 ).
It does not violate confidentiality to regard a command that reads the public port as being one
that (vacuously) reads the private port. Similarly, it does not violate confidentiality to regard

Page 5

a command that writes the private port as being one that (vacuously) writes the public port.
This leads to the following inclusion rule for commands:
` m @ (r, w) r v r0 w0 v w
` m @ (r0 , w0 )
That is, a command that reads at a level may be regarded as reading at any higher level, and
a command that writes at a level may be regarded as writing at any lower level.
Corresponding to the assignment of security levels to commands, we must enrich the type of
suspended commands to record the security level of the encapsulated command. That is, the
type cmd[(r, w)]( ) is the type of suspended commands that yield a value of type and that
have security level (r, w).
` m @ (r, w)
` cmd(m) : cmd[(r, w)]( )
The static semantics is organized so that each command has a principal security level in which
the read level is as small as possible and the write level is as large as possible.
(a) (5 points) State the principal typing rule for the return command, ret(e).
`e:
Solution: ` ret(e) @ (pub, priv)
(b) (5 points) State the most general possible typing rule for the bind command, seq(e; x.m).
Hint: the security level of e may differ from the security level of m. You will need two
premises relating the read and write levels of e to the read and write levels of m.
` e : cmd[(r, w)]( ) , x: ` m 0 @ (r0 , w0 ) r v r0
Solution:
` seq(e; x.m) 0 @ (r0 , w0 )

w0 v w

There are four commands for performing input and output: rdPriv, rdPub, wrPub(e),
and wrPriv(e). The read commands yield a string, and the write commands take a string
as argument and yield type unit.
Here are the principal typing rules for two of these commands:
` rdPub string @ (pub, priv)

` e : string
` wrPriv(e) unit @ (pub, priv)

By the inclusion rule given above these commands may also be given any security level
(r, w)! This corresponds to the idea that there are no confidentiality restrictions on public
reads or private writes.
(c) (5 points) Give the principal typing rule for private reads and public writes. This means
to give the smallest read level and the largest write level possible consistent with the
intended meaning of the security level of each command.
Solution:
` rdPriv string @ (priv, priv)

Page 6

` e : string
` wrPub(e) unit @ (pub, pub)

The essential reason why this language guarantees confidentiality comes down to the following assertion:
The command seq(cmd(rdPriv); x.wrPub(x)) is ill-typed at level (pub, priv).
That is, we cannot perform a private read followed by a public write in a program that is
well-typed at the most general security level (that is, with the least read level and greatest
write level).
Prove the critical case of this assertion by assuming that ` seq(cmd(rdPriv); x.wrPub(x))
@ (pub, priv) is derivable by the typing rule for sequencing, and deriving a contradiction.
(d) (5 points) By inversion of the typing rule for sequencing, these are all of the typing judgements that may be derived from the assumption.
Solution:
1. ` cmd(rdPriv) : cmd[(r, w)](string);
2. ` rdPriv string @ (r, w);
3. , x:string ` wrPub(x) @ (pub, priv), where = unit.
(e) (5 points) Give all of the ordering judgements among security levels that are derivable
from these facts. You will need to invert the sequencing rule, and you will need to take
account of the inclusion rule!
Solution:
1. r v pub and priv v w (from the sequencing rule).
2. priv v r (from the read private rule)
(f) (5 points) Draw a contradiction from the ordering judgements just derived.
Solution: If priv v r, then r = priv, but then r 6v pub.

Page 7

Question 3 [30]: Dynamic Typing

Let us extend Dynamic PCF (PFPL Chapter 22) with the following additional constructs
inspired by those found in dynamic languages such as Lisp or Scheme:
d ::= . . . | cons(d1 ; d2 ) | nil | car(d) | cdr(d) | ifcons(d; d1 ; d2 )
The expression cons(d1 ; d2 ) forms a pair of dynamic values as a dynamic value, and the expression nil may be thought of as the null pair. The operations car and cdr extract the
first and second components, respectively, of a pair created with cons(d1 ; d2 ). The expression
ifcons(d; d1 ; d2 ) evaluates d, and evaluates either d1 or d2 according to whether the value of d
is nil.
It is common in dynamic languages with these constructs to represent lists as compositions of
cons cells ending with nil, so that the list [1, 2, 3] would be represented by the expression
cons(1; cons(2; cons(3; nil))).
Using this representation the app function to append lists may be written in Dynamic PCF as
follows:
fix app is
x.
y.
ifcons x then cons(car(x),app(cdr(x))(y)) else y
First, each call to the function incurs two dynamic checks (because it is curried). Second, the
expressions car(x) and cdr(x) incur dynamic checks to ensure that x is a dynamic pair, but
only one such check is really necessary. We will explore the sources of these redundancies, and
how they may be remedied in a hybrid typed language.
(a) (10 points) Give the dynamic semantics rules for these constructs, bearing in mind that
this is a dynamic language. You must define the judgement d 7 d0 and d err. You will
require four auxiliary judgements, d is cons (d1 , d2 ), d isnt cons, d is nil, and d isnt nil,
which you are to define. To get you started, here are the congruence rules for transition
and error propagation; you are to give the other rules.
d1 7 d01
cons(d1 ; d2 ) 7 cons(d01 ; d2 )
d1 err
cons(d1 ; d2 ) err
d 7 d0
car(d) 7 car(d0 )

d err
car(d) err

d1 value d2 7 d02
cons(d1 ; d2 ) 7 cons(d1 ; d02 )
d1 value d2 err
cons(d1 ; d2 ) err
d 7 d0
cdr(d) 7 cdr(d0 )

d 7 d0
ifcons(d; d1 ; d2 ) 7 ifcons(d0 ; d1 ; d2 )

d err
cdr(d) err

d err
ifcons(d; d1 ; d2 ) err

Concentrate only on the extensions described above; do not bother with rules governing
the other constructs of Dynamic PCF.

Page 8

Solution:
d is cons (d1 , d2 )
car(d) 7 d1

d is cons (d1 , d2 )
cdr(d) 7 d2

d isnt cons
car(d) err

d value d is cons ( , )
ifcons(d; d1 ; d2 ) 7 d1
cons(d1 ; d2 ) is cons (d1 , d2 )

d isnt cons
cdr(d) err

d value d isnt cons

ifcons(d; d1 ; d2 ) 7 d2

cons(d1 ; d2 ) isnt nil

nil is nil

nil isnt cons

Recall that Hybrid PCF is an extension of statically typed PCF with a type dyn of dynamic
values. For the purposes of this question, we will further assume that Hybrid PCF has
product and option types. Now we extend Hybrid PCF with two classes, Cons and Nil, of
values of type dyn. The new and cast operations for these classes have the following typing
rules:
` e : dyn
` e : unit
` new[Nil](e) : dyn
` cast[Nil](e) : unit
` e : dyn dyn
` e : dyn
` new[Cons](e) : dyn
` cast[Cons](e) : dyn dyn
The dynamics for these constructs is as in Hybrid PCF:
e value c 6= c0
cast[c](new[c0 ](e)) err

e value
cast[c](new[c](e)) 7 e

(b) (5 points) Give definitions of nil, cons(e1 ; e2 ), car(e) and cdr(e) in Hybrid PCF so that
they implement the dynamics given above and they obey the following typing rules:
` nil : dyn

` e1 : dyn ` e2 : dyn
` cons(e1 ; e2 ) : dyn

` e : dyn
` car(e) : dyn

` e : dyn
` cdr(e) : dyn

Solution:
nil
cons(e1 ; e2 )
car(e)
cdr(e)

:=
:=
:=
:=

new[Nil](hi)
new[Cons](he1 , e2 i)
fst(cast[Cons](e))
snd(cast[Cons](e))

To define the conditional branch ifcons(e; e1 ; e2 ) in Hybrid PCF it is sufficient to enrich it

with a new expression, as[c](e), that returns null if its argument is not of class c, and that
returns just(e0 ) if it is of class c and its instance data is e0 .
` e : dyn
` as[Nil](e) : opt(unit)

` e : dyn
` as[Cons](e) : opt(dyn dyn)

The dynamics of as[c](e) is given by the following rules (omitting the obvious congruence
rules):
c 6= c0 e value
e value
as[c](new[c](e)) 7 just(e)
as[c](new[c0 ](e)) 7 null

Page 9

(c) (5 points) Give a definition of ifcons(e; e1 ; e2 ), which evaluates to e1 is the value of e is of

class Cons and to e2 otherwise.
Solution:
ifcons(e; e1 ; e2 ) ::= ifnull(as[Cons](e); e2 ; .e1 )
(d) (5 points) Translate the function app given above into an expression of Hybrid PCF of
type dyn
dyn
dyn by expanding the definitions of car(e), cdr(e), and ifcons(e; e1 ; e2 )
given above.
Solution:
fix app : dyn
dyn
dyn is
x : dyn.
y : dyn.
ifnull(as[Cons](x); y;
.new[Cons](hfst(cast[Cons](x)),
app(snd(cast[Cons](x)))(y)i))

(e) (5 points) The solution to the preceding question reveals two redundant dynamic class
checks arising from the casts of values that are known to be of class Cons. Rewrite the
answer to the preceding question to eliminate the redundant checks by taking advantage
of the bound variable of the ifnull elimination form for option types.
Solution:
fix app : dyn
dyn
dyn is
x : dyn.
y : dyn.
ifnull(as[Cons](x); y;
u.new[Cons](hfst(u), app(snd(u))(y)i))

Page 10

Question 4 [25]: Parallelism

In this problem, we will analyze the cost of a parallel algorithm to select the k th smallest
element from an unordered sequence of numbers. To do this, we will first extend the dataparallel language described in Chapter 43 of PFPL with a filter construct, which applies a
given function to every element of the sequence, and selects those elements for which the
function evaluates to true. The typing judgement and cost dynamics are given by the following
rules.
` e1 : seq , x : ` e2 : bool
(T F ilter)
` filter(e1 ; x.e2 ) : seq
e1 c1 seq(v0 , ..., vn1 ) map(seq(v0 , ..., vn1 ); x.e2 ) c2 seq(b0 , ..., bn1 )
n1

filter(e1 ; x.e2 ) c1 c2 (j=0 1) seq(vi | bi = true)

(EF ilter)

The algorithm, written below, works as follows: we first pick a pivot element in this case,
we simply pick the first element in the sequence. In parallel, we then filter the sequence twice,
selecting those elements less than the pivot into the sequence less, and selecting those elements
greater than the pivot into the sequence more. We then compare k to the size of the two
sequences. There are three cases to consider:
the less sequence contains the element we are looking for. In this case we recurse on less.
the pivot is the element we are looking for.
the more sequence contains the element we are looking for. In this case, we recurse on
more, adjusting k appropriately.
Below is the algorithm described above, with snippets of code missing for you to implement
fix selectk : nat seq nat nat is
x : nat seq. k:nat.
let pivot = x[0] in
letpar less = ... and
more = ... in
if k < len(less) then
selectk less k
else
if k < len(x) - len(more) then
pivot
else
selectk more (k - (len(x) - len(more))
(a) (5 points) Give the first piece of missing code, that computes the value of less by selecting
the elements of the sequence less than the pivot.
Solution: f ilter(x; y.y < pivot)
For this problem, assume that the cost of the arithmetic operations (subtraction, comparison) are computed in constant time. We are concerned with the size of the input as related

Page 11

to the length of the sequence of numbers, not of the size of the numbers themselves. Also
consider the input to be a value, that is, a fully computed sequence of numbers.
The running time of this algorithm is dependent on the input.
(b) (5 points) Give an input to selectk that exhibits the worst case running time. Assume
that the filter operation returns the list of filtered elements in the same order as they
appear in the input.
Solution: selectk(seq(0, 1, 2, ..., n 1), n 1)
Let us now consider the expected running time for this algorithm. Let us now assume that
the filter operation returns the list of filtered elements in random order. This, in effect,
will allow us to assume that the expected size of less is equal to the expected size of more.
(c) (5 points) What is the asymptotic work of this algorithm? This is the time needed to
run this algorithm on a single processor. Write, and solve, the recurrence function as a
function of the length of the sequence.
Solution: For some constants k0 , k1 ,
W (0) = k0
W (2n) = k0 + 4nk1 + W (n)
W (n) = O(n)
(d) (5 points) What is the asymptotic depth of this algorithm? This is the time needed to run
this algorithm on an unbounded number of processors. Write, and solve, the recurrence
function as a function of the length of the sequence.
Solution: For some constants k0 , k1 ,
D(0) = k0
D(2n) = k0 + 4k1 + D(n)
D(n) = O(lg(n))
(e) (5 points) What is the parallelizability ratio of this algorithm? What does this imply
about the ability to make use of multiple processors when executing this algorithm?
Solution: The parallelizability ratio is n/lg(n). For a fixed number of processors, p,
this means that we can make efficient use of them for sufficiently large problems, where
n/lg(n) >= p. For a given input size n, this is the maximum number of processors
that can be used to solve this problem efficiently; any extra processors would be forced
to sit idle.

Page 12

Question 5 [25]: The Spi-Calculus

Suppose Alice and Bob wish to securely communicate on a well-known channel. To do so, they
use the following protocol. First, Alice and Bob must exchange their public keys.
Second, if Alice wants to contact Bob, she sends him a message consisting of a nonce, a freshly
generated unguessable secret that identifies the message, encrypted by Bobs public key. When
Bob receives this message, he decrypts it using his private key.
Third and finally, he responds to Alice with another (freshly generated) nonce encrypted by
Alices public key. When Alice receives this message, Alice and Bob now have the two nonces
as a shared secret. This sort of protocol is useful in real-world situations when worrying about
the threat of being compromised by a malicious third party who also knows about the open
channel on which Alice and Bob are communicating.
In this question we formulate this protocol in an extension of the synchronous -calculus with
support for encryption, called the spi-calculus. It has the ability to generate key pairs consisting
of a public and corresponding private key and is able to encrypt communication on a channel
with a given key.
P ::= $(E) | 1 | c.P | (K, K).P | P1 || P2
E ::= !K c(a1 , ..., an ); P | ?K c(a1 , ..., an .P ) | 0 | E1 + E2
The operation (K, K).P allocates a private and public key pair. The send event is parameterized by a public key, K and the receive event is parameterized by the corresponding private
key, K. This corresponds to the idea that messages sent on a channel are encrypted using the
public key of the intended recipient, and are decrypted by the recipient using that principals
private key. (Each principal is responsible to protect its private key!) The send and receive
events generate the obvious actions, which are synchronized as specified by the following rule:
!K c(a1 ,...,an )

? c(a1 ,...,an )

K
P1 7 P10 P2 7
P20
P1 || P2 7 P10 || P20

In other words synchronization is possible only when the receiver has the private key corresponding to the public key used by the sender.
Now that we have encryption in the spi-calculus, we can define Alice and Bobs handshake
protocol as a process P of the form (K, K).c.(PA || PB ), where PA represents Alice, PB
represents Bob. The key pair K, K and channel c are keys and channels well-known to Alice
and Bob over which they may exchange their public keys. While not made explicit in the
question, it is assumed that other principals also know about c and K, and also that after
exchanging public keys, Alice and Bob have some way to verify that those keys actually belong
to each other (such as meeting in person). You are to write the two process calculus expressions,
PA and PB representing Alice and Bob in the protocol described above.
As shown in the protocol description, PA and PB can each be broken down into three phases;
PAi represents what Alice does in phase i, and PBi represents what Bob does in phase i. In
general, each phase for both Alice and Bob consist of a series of name generations (both keys
and channels), synchronous sends, and synchronous receives, though not all of these have to
occur in each phase. For nonces, they can use channel names, though only because channel
names act as fresh, unguessable secrets.

Page 13

(a) (11 points) Give the definitions of PA1 and PB1 .

Solution:
PA1 := (KA , KA ).$(?K c(KB .$(!KB c(KA ); PA2 )))
PB1 := (KB , KB ).$(!K c(KB ); $(?KB c(KA .PB2 )))
(b) (14 points) Give the definitions of PA2 , PB2 , PA3 , and PB3 .
Solution:
PA2 := a.$(!KB c(a); PA3 )
PB2 := $(?KB c(a.PB3 ))
PA3 := $(?KA c(b.PA0 ))
PB3 := b.$(!KA c(b); PB0 )

Page 14

Scratch Work:

Page 15

Scratch Work:

Page 16