Assignment 2

Moderator: Type Systems of Programming Languages

AlexanderF
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 140
Registriert: 2. Mai 2010 17:55

Assignment 2

Beitrag 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

Benutzeravatar
cofi
Mausschubser
Mausschubser
Beiträge: 86
Registriert: 22. Sep 2009 12:07

Re: Assignment 2

Beitrag 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'.

AlexanderF
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 140
Registriert: 2. Mai 2010 17:55

Re: Assignment 2

Beitrag von AlexanderF »

Ok,

yes, your right.

Thanks!

Antworten

Zurück zu „Type Systems of Programming Languages“