COMP3161/9164 23T3 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.
Thursday, 5th of October 2023, 23:59:59 PM ( )
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 (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 exclusive or 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 | 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 x ⇓ False
Not x ⇓ False(N1) Not x ⇓ True(N2) True ⇓ True(N3)
x⇓v y⇓v x⇓v y⇓v′ v̸=v′ Xor x y ⇓ False(N5) Xor x y ⇓ True
False ⇓ False(N4) (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′
(Ifcte)7→(Ifc′ te)(1) (IfTruete)7→t(2) (IfFalsete)7→e(3)
1. Show the full evaluation of the term (If True (If True False True) False). (5
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)
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:
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)
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 let let
f(x) = ¬x f(x) = ¬x f(x) = x(True)
f(x) f(f) f(False)
end end end
The following are examples of things that should be accepted: nested defini- tions, and shadowed definitions.
f (x ) = let
g(y) = ¬x ⊕ y in
g(x) ⊕ ¬g(x) end
f (x ) = x in
f (x ) = f (x ) in
f (True) 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. More information here: https://www.student.unsw.edu.au/special-consideration
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!
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com