Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: THEend8_
COMP3161/9164 Assignment
Proofs
Marks : 15% of overall marks for the course.
A mark of x (out of 100) on this assignment will
translate to .15x course marks.
Due date: Thursday, 5th of October 2023, 23:59:59 PM (Sydney Time)
1 Task
In this assignment you will formally model a language of boolean computations using a
variety of semantic techniques, including its syntax and sematics, and its compilation to
various target languages.
Prepare your answers in one PDF file, preferably using LATEX, where all prose is
typeset. Figures may be drawn, but make sure they are legible. Please ensure all
mathematics is formatted correctly. Some guidance will be posted on the course website.
Submit your PDF using the CSE give system, by typing the command
give cs3161 Proofs Proofs.pdf
or by using the CSE give web interface.
Part A (25 marks)
Consider the language of boolean expressions P containing just literals (True, False),
parentheses, exclusive or (⊕) and negation (¬):
P = {True, False,¬True,¬False, True⊕ False,¬(True⊕ False), . . . }
1. Write down a set of inference rules that define the set P. The rules may be
ambiguous. (5 marks)
2. The operator ¬ has the highest precedence, and conjunction is right-associative.
Define a set of simultaneous judgements to define the language without any ambi-
guity. (5 marks)
1
3. Here is an abstract syntax B for the same language:
B ::= Not B | Xor B B | True | False
Write an inductive definition for the parsing relation connecting your unambiguous
judgements to this abstract syntax. (5 marks)
4. Here is a big-step semantics for the language B
x ⇓ True
Not x ⇓ False(N1)
x ⇓ False
Not x ⇓ True(N2) True ⇓ True(N3) False ⇓ False(N4)
x ⇓ v y ⇓ v
Xor x y ⇓ False(N5)
x ⇓ v y ⇓ v ′ v 6= v ′
Xor x y ⇓ True (N6)
a) Show the evaluation of Xor (Not (Xor True False)) True with a derivation tree.
(5 marks)
b) Consider the following inference rule:
x ⇓ v
Not x ⇓ v−1
where we understand v−1 to be defined by the following equations:
True−1 = False
False−1 = True
Is this rule derivable? Is it admissible? Justify your answers. (5 marks)
Part B (20 marks)
Here is a small-step semantics for a language L with True, False and if expressions:
c 7→ c ′
(If c t e) 7→ (If c ′ t e)(1) (If True t e) 7→ t(2) (If False t e) 7→ e(3)
1. Show the full evaluation of the term (If True (If True False True) False). (5
marks)
2. Define an equivalent big-step semantics for L. (5 marks)
3. Prove that if e ⇓ v then e ?7→ v, where ⇓ is the big-step semantics you defined in
the previous question, and
?7→ is the reflexive and transitive closure of 7→. Use rule
induction on e ⇓ v. (10 marks)
2
Part C (15 marks)
1. Define a recursive compilation function c : B → L which converts expressions in
B to expressions in L. (5 marks)
2. Prove that for all e, e ⇓ v implies c(e) ⇓ v, by rule induction on the assumption
that e ⇓ v. (10 marks)
Part D (40 marks)
1. Here is a term in λ-calculus:
(λn. λf. λx. (n f (f x))) (λf. λx. f x)
a) Fully β-reduce the above λ-term. Show all intermediate beta reduction steps.
(5 marks)
b) Identify an η-reducible expression in the above (unreduced) term. (5 marks)
2. Recall that in λ-calculus, booleans can be encoded as binary functions that return
one of their arguments:
T ≡ (λx. λy. x)
F ≡ (λx. λy. y)
Either via L or directly, define a function d : B→ λ which converts expressions in
B to λ-calculus. (5 marks)
3. Prove that for all e such that e ⇓ v it holds that d(e) ≡αβη v ′, where v ′ is the
λ-calculus encoding of v. (10 marks)
4. Suppose we added unary local function definitions to our language P. Here’s an
example in concrete syntax:
let
g(x ) = ¬x
in
g(True)
end
We limit ourselves to non-recursive bindings (meaning functions can’t call them-
selves), and first-order functions (meaning functions accept exactly one boolean
argument).
a) Extend the abstract syntax for B from question A.3 so that it supports the
features used in the above example. Use first-order abstract syntax with
explicit strings. You don’t have to extend the parsing relation. (5 marks)
3
b) Define a scope-checking judgement, similar to the ok judgement from the
lectures. It should check (a) that all names of variables and functions are used
only within their scopes; and (b) that names used in variable (or function)
position are indeed the names of variables (or functions). Hence, the following
expressions should both be rejected:
let
f (x ) = ¬x
in
f (x )
end
let
f (x ) = ¬x
in
f (f )
end
let
f (x ) = x (True)
in
f (False)
end
The following are examples of things that should be accepted: nested defini-
tions, and shadowed definitions.
let
f (x ) =
let
g(y) = ¬x ⊕ y
in
g(x )⊕ ¬g(x )
end
in
f (False)
end
let
f (x ) = x
in
let
f (x ) = f (x )
in
f (True)
end
end
Note that the latter example is not a recursive call.
This question is a bit more open-ended than the previous ones, and will require
you to make some design choices. Here’s one: if the same string is used to
denote both a function name and a variable in the same scope, should that be
rejected or accepted by your judgement? Explicitly state (in English) which
choice you made, and define things accordingly. (10 marks)
2 Late Penalty
You may submit up to five days (120 hours) late. Each day of lateness corresponds to
a 5% reduction of your total mark. For example, if your assignment is worth 88% and
you submit it two days late, you get 78%. If you submit it more than five days late, you
get 0%.
Course staff cannot grant assignment extensions—if you need an extension, you have
to apply for special consideration through the standard procedure.
4
3 Plagiarism
Many students do not appear to understand what is regarded as plagiarism. This is
no defense.
All work submitted for assessment must be entirely your own work. We regard un-
acknowledged copying of material, in whole or part, as an extremely serious offence. In
this course submission of any work derived from another person, or solely or jointly writ-
ten by and or with someone else, without clear and explicit acknowledgement, will be
severely punished and may result in automatic failure for the course and a mark of zero
for the course. Note this includes including unreferenced work from books, the internet,
etc.
Do not provide or show your assessable work to any other person. Allowing another
student to copy from you will, at the very least, result in zero for that assessment. If
you knowingly provide or show your assessment work to another person for any reason,
and work derived from it is subsequently submitted, you will be penalized, even if the
work was submitted without your knowledge or consent. This will apply even if your
work is submitted by a third party unknown to you. You should keep your work private
until submissions have closed.
If you are unsure about whether certain activities would constitute plagiarism ask us
before engaging in them!