![\begin{mathpar}
\inferrule[T-VarA]{ }{x : T}
\par
\inferrule[T-AbsA]{t : T}{\lam...
...ar
\textrm{\ldots additional rules for booleans and \lq\lq if'' \ldots}
\end{mathpar}](homework6-img1.png)
Suppose we try to prove progress and preservation (for closed terms)
with this ``type system.''
Can we do it? Explain! Give concrete examples.
Please read Chapter 9 in the textbook.
In class, we discussed several dubious type rules. In particular, we
discussed something similar the following system:
Suppose we try to prove progress and preservation (for closed terms)
with this ``type system.''
Can we do it? Explain! Give concrete examples.
If we changed the rules to
![\begin{mathpar}
\inferrule[T-VarB]{ }{x : \texttt{Bool}}
\par
\inferrule[T-AbsB]...
...ar
\textrm{\ldots additional rules for booleans and \lq\lq if'' \ldots}
\end{mathpar}](homework6-img2.png)
Can we prove progress and preservation? Discuss!
Read Exercise 9.2.3 and prove that if
then we have a contradiction.
Do the proof of preservation (Theorem 9.3.9).
You will need to use the substitution lemma (Lemma 9.3.8).
In the skeleton file, two of the helper lemmas are marked as ``EXTRA.'' if you complete the rest of the homework, you are invited to do these proofs. A better grade on this part will replace a poorer grade for the SASyLF part of a previous homework.
In the substitution lemma, you will need to use ``weakening'' and ``exchange'' lemmas/properties. What flavor of type systems does not have weakening? Explain! When is exchange for some type systems problematic? Explain!