Go backward to Unicity of Typing
Go up to Top
Go forward to Typing Rules Define a Language
Unicity of Typing
- Unicity of typing holds for Expression:
- Case N. N:int holds. By single typing rule,
N:intexp holds.
- Case E_1+E_2. By inductive hypothesis,
E_1:T_1 and E_2:T_2 hold
for
unique T_1 and T_2. By single
typing
rule, E_1:intexp and E_2:intexp must hold. If
T_1=T_2=intexp, then
E_1+E_2:intexp. Otherwise, E_1+E_2 has no typing.
- ...
- Unicity of typing holds for Command:
- Case L := E. L:intloc holds. E:T_1
holds for unique T_1. By single typing rule,
T_1 must be intexp to have L:=E:
comm. Otherwise, L:=E has no typing.
- ...
Unicity of typing holds for all four syntax domains.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: core.tex,v 1.3 1996/02/05 10:34:52 schreine Exp schreine