Unicity of Typing
- Unicity of typing holds for Expression:
- Case N. N:int holds. By single typing rule,
N:intexp holds.
- Case E1+E2. By inductive hypothesis,
E1:T1 and E2:T2 hold
for
unique T1 and T2. By single
typing
rule, E1:intexp and E2:intexp must hold. If
T1=T2=intexp, then
E1+E2:intexp. Otherwise, E1+E2 has no typing.
- ...
- Unicity of typing holds for Command:
- Case L := E. L:intloc holds. E:T1
holds for unique T1. By single typing rule,
T1 must be intexp to have L:=E:
comm. Otherwise, L:=E has no typing.
- ...
Unicity of typing holds for all four syntax domains.
Author: Wolfgang Schreiner
Last Modification: March 26, 1998