Moderator: Type Systems of Programming Languages
there is one thing that I do not understand in assignment 2 2.
when I have a expression like (<1> == <1>)+<2>
the new rule T-Eq' says that
<1> == <1> hast type Num
The contraction rule Eq-True
says us that:
<1> = <1> -> true
and by congruence rule Add1:
(<1> == <1>)+<2> -> true+<2>
when I remember
the contraction rule (AddNum) from the lectures a few weeks ago:
<m> + <n> -> <m + n>
this contraction rule cannot be applied to true + 2,
because true has not the form <m>
so I cannot show that progress stil holds because in this example it does not?
Or is the meaning of the exercise to assume that we have additional contraction rules for plus
which are also applyable for arguments that are not of the form <n> and <m>?
(in the sense that a computer saves data from different types in the same way, as 0s and 1s)?
It does. Consider the definition of progress /preservation in detail, for how many reduction steps progress is "guaranteed" and if you still satisfy the premise for e'.AlexanderF hat geschrieben:so I cannot show that progress stil holds because in this example it does not?