COMP3161/9164 21T3 Assignment 0 Proofs
15% of overall marks for the course.
A mark of x (out of 100) on this assignment will translate to .15x course marks.
Wednesday, 6th of October 2021, 12 noon ( )
Copyright By PowCoder代写 加微信 powcoder
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 (30 marks)
Consider the language of boolean expressions P containing just literals (True, False), parentheses, disjunction (∨) 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 disjunction is right-associative. Define a set of simultaneous judgements to define the language without any ambi- guity. (5 marks)
3. Here is an abstract syntax B for the same language:
B ::= Not B | Or 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 x⇓False Not x ⇓ False Not x ⇓ True
True ⇓ True
a) Show the evaluation of Or (Not (Or True False)) False with a derivation tree.
b) ProvethatforallesuchthateB,thereexistsavsuchthate⇓v. Userule induction on the assumption e B. (10 marks)
Part B (15 marks)
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? (5 marks)
2. Show the full evaluation of the term (If (If True False True) True False). (5 marks)
3. Define an equivalent big-step semantics for L. (5 marks)
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. f (n f x)) (λf. λx. f x)
x⇓True x⇓False y⇓v Or x y ⇓ True Or x y ⇓ v
False ⇓ False
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 n-ary local function definitions to our language P. Here’s an example in concrete syntax:
nand (x , y ) = ¬x ∨ ¬y in
nand (true, false) end
We limit ourselves to non-recursive bindings (meaning functions can’t call them- selves), and first-order functions (meaning functions require boolean arguments).
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)
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:
(10 marks)
f (x ) = ¬x in
f (x ) = x (True)
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 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!