421 lines
15 KiB
TeX
421 lines
15 KiB
TeX
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
%
|
|
% I N F O R M A T I C S
|
|
% Honours Exam LaTeX Template for Exam Authors
|
|
%
|
|
% Created: 12-Oct-2009 by G.O.Passmore.
|
|
% Last Updated: 10-Sep-2018 by I. Murray
|
|
%
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
%%% The following define the status of the exam papers in the order
|
|
%%% required. Simply remove the comment (i.e., the % symbol) just
|
|
%%% before the appropriate one and comment the others out.
|
|
|
|
%\newcommand\status{\internal}
|
|
%\newcommand\status{\external}
|
|
\newcommand\status{\final}
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
%%% The following three lines are always required. You may add
|
|
%%% custom packages to the one already defined if necessary.
|
|
|
|
\documentclass{examhons2018}
|
|
\usepackage{amssymb}
|
|
\usepackage{amsmath}
|
|
\usepackage{semantic}
|
|
\usepackage{stix}
|
|
|
|
%%% Uncomment the \checkmarksfalse line if the macros that check the
|
|
%%% mark totals cause problems. However, please do not make your
|
|
%%% questions add up to a non-standard number of marks without
|
|
%%% permission of the convenor.
|
|
%\checkmarksfalse
|
|
|
|
\begin{document}
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
%
|
|
% Replace {ad} below with the ITO code for your course. This will
|
|
% be used by the ITO LaTeX installation to install course-specific
|
|
% data into the exam versions it produces from this document.
|
|
%
|
|
% Your choices are (in course title order):
|
|
%
|
|
% {anlp} - Acc. Natural Language Processing (MSc)
|
|
% {aleone} - Adaptive Learning Environments 1 (Inf4)
|
|
% {adbs} - Advanced Databases (Inf4)
|
|
% {av} - Advanced Vision (Inf4)
|
|
% {av-dl} - Advanced Vision - distance learning (MSc)
|
|
% {apl} - Advances in Programming Languages (Inf4)
|
|
% {abs} - Agent Based Systems [L10] (Inf3)
|
|
% {afds} - Algorithmic Foundations of Data Science (MSc)
|
|
% {agta} - Algorithmic Game Theory and its Apps. (MSc)
|
|
% {ads} - Algorithms and Data Structures (Inf3)
|
|
% {ad} - Applied Databases (MSc)
|
|
% {aipf} - Artificial Intelligence Present and Future (MSc)
|
|
% {ar} - Automated Reasoning (Inf3)
|
|
% {asr} - Automatic Speech Recognition (Inf4)
|
|
% {bioone} - Bioinformatics 1 (MSc)
|
|
% {biotwo} - Bioinformatics 2 (MSc)
|
|
% {bdl} - Blockchains and Distributed Ledgers (Inf4)
|
|
% {cqi} - Categories and Quantum Informatics (MSc)
|
|
% {copt} - Compiler Opimisation [L11] (Inf4)
|
|
% {ct} - Compiling Techniques (Inf3)
|
|
% {ccs} - Computational Cognitive Science (Inf3)
|
|
% {cmc} - Computational Complexity (Inf4)
|
|
% {ca} - Computer Algebra (Inf4)
|
|
% {cav} - Computer Animation and Visualisation (Inf4)
|
|
% {car} - Computer Architecture (Inf3)
|
|
% {comn} - Computer Comms. and Networks (Inf3)
|
|
% {cd} - Computer Design (Inf3)
|
|
% {cg} - Computer Graphics [L11] (Inf4)
|
|
% {cn} - Computer Networking [L11] (Inf4)
|
|
% {cp} - Computer Prog. Skills and Concepts (nonhons)
|
|
% {cs} - Computer Security (Inf3)
|
|
% {dds} - Data, Design and Society (nonhons)
|
|
% {dme} - Data Mining and Exploration (Msc)
|
|
% {dbs} - Database Systems (Inf3)
|
|
% {dmr} - Decision Making in Robots and Autonomous Agents(MSc)
|
|
% {dmmr} - Discrete Maths. and Math. Reasoning (nonhons)
|
|
% {ds} - Distributed Systems [L11] (Inf4)
|
|
% {epl} - Elements of Programming Languages (Inf3)
|
|
% {es} - Embedded Software (Inf4)
|
|
% {exc} - Extreme Computing (Inf4)
|
|
% {fv} - Formal Verification (Inf4)
|
|
% {fnlp} - Foundations of Natural Language Processing (Inf3)
|
|
% {hci} - Human-Computer Interaction [L11] (Inf4)
|
|
% {infonea} - Informatics 1 - Introduction to Computation(nonhons)
|
|
% different sittings for INF1A programming exams
|
|
% {infoneapone} - Informatics 1 - Introduction to Computation(nonhons)
|
|
% {infoneaptwo} - Informatics 1 - Introduction to Computation(nonhons)
|
|
% {infoneapthree} - Informatics 1 - Introduction to Computation(nonhons)
|
|
% {infonecg} - Informatics 1 - Cognitive Science (nonhons)
|
|
% {infonecl} - Informatics 1 - Computation and Logic (nonhons)
|
|
% {infoneda} - Informatics 1 - Data and Analysis (nonhons)
|
|
% {infonefp} - Informatics 1 - Functional Programming (nonhons)
|
|
% If there are two sittings of FP, use infonefpam for the first
|
|
% paper and infonefppm for the second sitting.
|
|
% {infoneop} - Informatics 1 - Object-Oriented Programming(nonhons)
|
|
% If there are two sittings of OOP, use infoneopam for the first
|
|
% paper and infoneoppm for the second sitting.
|
|
% {inftwoa} - Informatics 2A: Proc. F&N Languages (nonhons)
|
|
% {inftwob} - Informatics 2B: Algs., D.Structs., Learning(nonhons)
|
|
% {inftwoccs}- Informatics 2C-CS: Computer Systems (nonhons)
|
|
% {inftwocse}- Informatics 2C: Software Engineering (nonhons)
|
|
% {inftwod} - Informatics 2D: Reasoning and Agents (nonhons)
|
|
% {iar} - Intelligent Autonomous Robotics (Inf4)
|
|
% {it} - Information Theory (MSc)
|
|
% {imc} - Introduction to Modern Cryptography (Inf4)
|
|
% {iotssc} - Internet of Things, Systems, Security and the Cloud (Inf4)
|
|
% (iqc) - Introduction to Quantum Computing (Inf4)
|
|
% (itcs) - Introduction to Theoretical Computer Science (Inf3)
|
|
% {ivc} - Image and Vision Computing (MSc)
|
|
% {ivr} - Introduction to Vision and Robotics (Inf3)
|
|
% {ivr-dl} - Introduction to Vision and Robotics - distance learning (Msc)
|
|
% {iaml} - Introductory Applied Machine Learning (MSc)
|
|
% {iaml-dl} - Introductory Applied Machine Learning - distance learning (MSc)
|
|
% {lpt} - Logic Programming - Theory (Inf3)
|
|
% {lpp} - Logic Programming - Programming (Inf3)
|
|
% {mlpr} - Machine Learning & Pattern Recognition (Inf4)
|
|
% {mt} - Machine Translation (Inf4)
|
|
% {mi} - Music Informatics (MSc)
|
|
% {nlu} - Natural Language Understanding [L11] (Inf4)
|
|
% {nc} - Neural Computation (MSc)
|
|
% {nat} - Natural Computing (MSc)
|
|
% {nluplus} - Natural Language Understanding, Generation, and Machine Translation(MSc)
|
|
% {nip} - Neural Information Processing (MSc)
|
|
% {os} - Operating Systems (Inf3)
|
|
% {pa} - Parallel Architectures [L11] (Inf4)
|
|
% {pdiot} - Principles and Design of IoT Systems (Inf4)
|
|
% {ppls} - Parallel Prog. Langs. and Sys. [L11] (Inf4)
|
|
% {pm} - Performance Modelling (Inf4)
|
|
% {pmr} - Probabilistic Modelling and Reasoning (MSc)
|
|
% {pi} - Professional Issues (Inf3)
|
|
% {rc} - Randomness and Computation (Inf4)
|
|
% {rl} - Reinforcement Learning (MSc)
|
|
% {rlsc} - Robot Learning and Sensorimotor Control (MSc)
|
|
% {rss} - Robotics: Science and Systems (MSc)
|
|
% {sp} - Secure Programming (Inf4)
|
|
% {sws} - Semantic Web Systems (Inf4)
|
|
% {stn} - Social and Technological Networks (Inf4)
|
|
% {sapm} - Software Arch., Proc. and Mgmt. [L11] (Inf4)
|
|
% {sdm} - Software Design and Modelling (Inf3)
|
|
% {st} - Software Testing (Inf3)
|
|
% {ttds} - Text Technologies for Data Science (Inf4)
|
|
% {tspl} - Types and Semantics for Programming Langs. (Inf4)
|
|
% {usec} - Usable Security and Privacy (Inf4)
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
\setcourse{tspl}
|
|
\initcoursedata
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
%
|
|
% Set your exam rubric type.
|
|
%
|
|
% Most courses in the School have exams that add up to 50 marks,
|
|
% and your choices are:
|
|
% {qu1_and_either_qu2_or_qu3, any_two_of_three, do_exam}
|
|
% (which include the "CALCULATORS MAY NOT BE USED..." text), or
|
|
% {qu1_and_either_qu2_or_qu3_calc, any_two_of_three_calc, do_exam_calc}
|
|
% (which DO NOT include the "CALCULATORS MAY NOT BE USED..." text), or
|
|
% {custom}.
|
|
%
|
|
% Note, if you opt to create a custom rubric, you must:
|
|
%
|
|
% (i) **have permission** from the appropriate authority, and
|
|
% (ii) execute:
|
|
%
|
|
% \setrubrictype{} to specify the custom rubric information.
|
|
%
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
\setrubric{qu1_and_either_qu2_or_qu3}
|
|
|
|
\examtitlepage
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
%
|
|
% Manual override for total page number computation.
|
|
%
|
|
% As long as you run latex upon this document three times in a row,
|
|
% the right number of `total pages' should be computed and placed
|
|
% in the footer of all pages except the title page.
|
|
%
|
|
% But, if this fails, you can set that number yourself with the
|
|
% following command:
|
|
%
|
|
% \settotalpages{n} with n a natural number.
|
|
%
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
%
|
|
% Beginning of your exam text.
|
|
%
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
\begin{enumerate}
|
|
|
|
\item \rubricqA
|
|
|
|
\newcommand{\Tree}{\texttt{Tree}}
|
|
\newcommand{\AllT}{\texttt{AllT}}
|
|
\newcommand{\AnyT}{\texttt{AnyT}}
|
|
\newcommand{\leaf}{\texttt{leaf}}
|
|
\newcommand{\branch}{\texttt{branch}}
|
|
\newcommand{\here}{\texttt{here}}
|
|
\renewcommand{\left}{\texttt{left}}
|
|
\renewcommand{\right}{\texttt{right}}
|
|
\newcommand{\ubar}{\texttt{\underline{~}}}
|
|
|
|
Consider a type of trees defined as follows.
|
|
\begin{gather*}
|
|
%
|
|
\inference[\leaf]
|
|
{A}
|
|
{Tree~A}
|
|
%
|
|
\quad
|
|
%
|
|
\inference[\ubar\branch\ubar]
|
|
{Tree~A \\
|
|
Tree~A}
|
|
{Tree~A}
|
|
%
|
|
\end{gather*}
|
|
|
|
Given a predicate $P$ over $A$, we define predicates $\AllT$ and
|
|
$\AnyT$ which hold when $P$ holds for \emph{every} leaf in the tree
|
|
and when $P$ holds for \emph{some} leaf in the tree, respectively.
|
|
\begin{gather*}
|
|
%
|
|
\inference[\leaf]
|
|
{P~x}
|
|
{\AllT~P~(\leaf~x)}
|
|
%
|
|
\quad
|
|
%
|
|
\inference[\ubar\branch\ubar]
|
|
{\AllT~P~xt \\
|
|
\AllT~P~yt}
|
|
{\AllT~P~(xt~\branch~yt)}
|
|
%
|
|
\\~\\
|
|
%
|
|
\inference[\leaf]
|
|
{P~x}
|
|
{\AnyT~P~(\leaf~x)}
|
|
%
|
|
\quad
|
|
%
|
|
\inference[\left]
|
|
{\AnyT~P~xt}
|
|
{\AnyT~P~(xt~\branch~yt)}
|
|
%
|
|
\quad
|
|
%
|
|
\inference[\right]
|
|
{\AnyT~P~yt}
|
|
{\AnyT~P~(xt~\branch~yt)}
|
|
%
|
|
\end{gather*}
|
|
|
|
\begin{itemize}
|
|
|
|
\item[(a)] Formalise the definitions above.
|
|
|
|
\marks{12}
|
|
|
|
\item[(b)] Prove $\AllT~({\neg\ubar}~\circ~P)~xt$
|
|
implies $\neg~(\AnyT~P~xt)$, for all trees $xt$.
|
|
|
|
\marks{13}
|
|
|
|
\end{itemize}
|
|
|
|
\newpage
|
|
|
|
\item \rubricqB
|
|
|
|
\newcommand{\COMP}{\texttt{Comp}}
|
|
\newcommand{\OK}{\texttt{ok}}
|
|
\newcommand{\ERROR}{\texttt{error}}
|
|
\newcommand{\LETC}{\texttt{letc}}
|
|
\newcommand{\IN}{\texttt{in}}
|
|
|
|
\newcommand{\Comp}[1]{\COMP~#1}
|
|
\newcommand{\error}[1]{\ERROR~#1}
|
|
\newcommand{\ok}[1]{\OK~#1}
|
|
\newcommand{\letc}[3]{\LETC~#1\leftarrow#2~\IN~#3}
|
|
|
|
\newcommand{\comma}{\,,\,}
|
|
\newcommand{\V}{\texttt{V}}
|
|
\newcommand{\dash}{\texttt{-}}
|
|
\newcommand{\Value}{\texttt{Value}}
|
|
\newcommand{\becomes}{\longrightarrow}
|
|
\newcommand{\subst}[3]{#1~\texttt{[}~#2~\texttt{:=}~#3~\texttt{]}}
|
|
|
|
You will be provided with a definition of intrinsically-typed lambda
|
|
calculus in Agda. Consider constructs satisfying the following rules,
|
|
written in extrinsically-typed style.
|
|
|
|
A computation of type $\Comp{A}$ returns either an error with a
|
|
message $msg$ which is a string, or an ok value of a term $M$ of type $A$.
|
|
Consider constructs satisfying the following rules:
|
|
|
|
Typing:
|
|
\begin{gather*}
|
|
\inference[$\ERROR$]
|
|
{}
|
|
{\Gamma \vdash \error{msg} \typecolon \Comp{A}}
|
|
\qquad
|
|
\inference[$\OK$]
|
|
{\Gamma \vdash M \typecolon A}
|
|
{\Gamma \vdash \ok{M} \typecolon \Comp{A}}
|
|
\\~\\
|
|
\inference[$\LETC$]
|
|
{\Gamma \vdash M \typecolon \Comp{A} \\
|
|
\Gamma \comma x \typecolon A \vdash N \typecolon \Comp{B}}
|
|
{\Gamma \vdash \letc{x}{M}{N} \typecolon \Comp{B}}
|
|
\end{gather*}
|
|
|
|
Values:
|
|
\begin{gather*}
|
|
\inference[\V\dash\ERROR]
|
|
{}
|
|
{\Value~(\error{msg})}
|
|
\qquad
|
|
\inference[\V\dash\OK]
|
|
{\Value~V}
|
|
{\Value~(\ok{V})}
|
|
\end{gather*}
|
|
|
|
Reduction:
|
|
\begin{gather*}
|
|
\inference[$\xi\dash\OK$]
|
|
{M \becomes M'}
|
|
{\ok{M} \becomes \ok{M'}}
|
|
\qquad
|
|
\inference[$\xi\dash\LETC$]
|
|
{M \becomes M'}
|
|
{\letc{x}{M}{N} \becomes \letc{x}{M'}{N}}
|
|
\\~\\
|
|
\inference[$\beta\dash\ERROR$]
|
|
{}
|
|
{\letc{x}{(\error{msg})}{t} \becomes \error{msg}}
|
|
\\~\\
|
|
\inference[$\beta\dash\OK$]
|
|
{\Value{V}}
|
|
{\letc{x}{(\ok{V})}{N} \becomes \subst{N}{x}{V}}
|
|
\end{gather*}
|
|
|
|
\begin{enumerate}
|
|
\item[(a)] Extend the given definition to formalise the evaluation
|
|
and typing rules, including any other required definitions.
|
|
\marks{12}
|
|
|
|
\item[(b)] Prove progress. You will be provided with a proof of progress for
|
|
the simply-typed lambda calculus that you may extend.
|
|
\marks{13}
|
|
\end{enumerate}
|
|
|
|
Please delimit any code you add as follows.
|
|
\begin{verbatim}
|
|
-- begin
|
|
-- end
|
|
\end{verbatim}
|
|
|
|
\newpage
|
|
|
|
\item \rubricqC
|
|
|
|
\newcommand{\TT}{\texttt{tt}}
|
|
\newcommand{\CASETOP}{{\texttt{case}\top}}
|
|
\newcommand{\casetop}[2]{\CASETOP~#1~{\texttt{[tt}\!\Rightarrow}~#2~\texttt{]}}
|
|
\newcommand{\up}{\uparrow}
|
|
\newcommand{\dn}{\downarrow}
|
|
|
|
You will be provided with a definition of inference for extrinsically-typed lambda
|
|
calculus in Agda. Consider constructs satisfying the following rules,
|
|
written in extrinsically-typed style that support bidirectional inference.
|
|
|
|
Typing:
|
|
\begin{gather*}
|
|
\inference[$\TT$]
|
|
{}
|
|
{\Gamma \vdash \TT \dn \top}
|
|
\\~\\
|
|
\inference[$\CASETOP$]
|
|
{\Gamma \vdash L \up \top \\
|
|
\Gamma \vdash M \dn A}
|
|
{\Gamma \vdash \casetop{L}{M} \dn A}
|
|
\end{gather*}
|
|
|
|
\begin{enumerate}
|
|
\item[(a)] Extend the given definition to formalise the typing rules,
|
|
and update the definition of equality on types.
|
|
\marks{10}
|
|
|
|
\item[(b)] Extend the code to support type inference for the new features.
|
|
\marks{15}
|
|
\end{enumerate}
|
|
|
|
Please delimit any code you add as follows.
|
|
\begin{verbatim}
|
|
-- begin
|
|
-- end
|
|
\end{verbatim}
|
|
|
|
\end{enumerate}
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
%
|
|
% End of your exam text.
|
|
%
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
\end{document}
|