COMP3161/9164 20T3 Assignment 0 Proofs
Version 1.0
Marks : 15% of overall marks for the course
Due date: Wednesday, 7th of October 2020, 12 noon (Sydney Time)
History
September 15th Initial spec drafted
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 (although figures may be drawn). 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
Consider the language of boolean expressions P containing just literals (True, False), parentheses, implication (⇒) 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.
1
2. The operator ¬ has the highest precedence, and implication is right-associative. Define a set of simultaneous judgements to define the language without any ambi- guity.
3. Here is an abstract syntax B for the same language:
B ::= Not B | Imp B B | True | False
Write an inductive definition for the parsing relation connecting your unambiguous judgements to this abstract syntax.
4. Here is a big-step semantics for the language B
x⇓True x⇓False Not x ⇓ False Not x ⇓ True
True ⇓ True
x⇓False x⇓True y⇓v Imp x y ⇓ True Imp x y ⇓ v
False ⇓ False
a) What is the set of evaluable expressions? What is the set of values?
b) Show the evaluation of Imp (Not (Imp True False)) False with a derivation tree.
c) Define an equivalent small-step semantics for B. Part B
Here is a small-step semantics for a language L with True, False and if expressions: c → c′
(Ifcte)→(Ifc′ te)(1) (IfTruete)→t(2) (IfFalsete)→e(3)
1. What are the initial states for this semantics? What are the final states?
2. Show the full evaluation of the term (If (If True False True) True False).
3. Define an equivalent big-step semantics for L.
Part C
1. Define a compilation function c : B → L which converts expressions in B to expressions in L.
2. Prove for all e B where e ⇓ v that c(e) ⇓ v by rule induction on the assumption that e ⇓ v.
2
Part D
1. Here is a term in λ-calculus:
(λn. λf. λx. f (n f x)) (λf. λx. f x)
a) Fully β-reduce the above λ-term. Show all intermediate beta reduction steps. b) Identify an η-reducible expression in the above (unreduced) term.
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.
3. Prove for all e B where e ⇓ v that d(e) ≡αβη v′ where v′ is the λ-calculus encoding of v.
4. Suppose we wished to add let bindings to our language B. The abstract syntax is given in higher-order form as Let B (x. B).
a) Here is an example of an expression in our extended B:
(Let True (x. Let (Imp x False) (x. (Imp x (Let (Imp a x) (a. Imp a x))))))
Give an α-equivalent expression that does not shadow x.
b) Apply the substitution [a := False] to the (original) expression.
c) What is the scope of the bound variable a in this expression?
d) How would you extend the λ-calculus encoding function d to include Let
expressions?
2 Late Penalty
Unless otherwise stated if you wish to submit an assignment late, you may do so, but a late penalty reducing the maximum available mark applies to every late assignment. The maximum available mark is reduced by 10% if the assignment is one day late, by 25% if it is 2 days late and by 50% if it is 3 days late. Assignments that are late 4 days or more will be awarded zero marks. So if your assignment is worth 88% and you submit it one day late you still get 88%, but if you submit it two days late you get 75%, three days late 50%, and four days late zero.
Assignment extensions are only awarded for serious and unforeseeable events. Having the flu for a few days, deleting your assignment by mistake, going on holiday, work commitments, etc do not qualify. Therefore aim to complete your assignments well before the due date in case of last minute illness, and make regular backups of your work.
3
3 Plagiarism
Many students do not appear to understand what is regarded as plagiarism. This is no defense. Before submitting any work you should read and understand the UNSW plagiarism policy https://student.unsw.edu.au/plagiarism.
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!
4