Seite 1 von 1

Assignment 2

Verfasst: 9. Nov 2013 16:29
von AlexanderF
hello,

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)?

regards,
Alexander

Re: Assignment 2

Verfasst: 9. Nov 2013 17:09
von cofi
AlexanderF hat geschrieben:so I cannot show that progress stil holds because in this example it does not?
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'.

Re: Assignment 2

Verfasst: 10. Nov 2013 16:31
von AlexanderF
Ok,

yes, your right.

Thanks!