![\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).