Go backward to Structural Induction Go up to Top Go forward to Unicity of Typing

Unicity of Typing

Can a syntax tree be typed in multiple ways?

• Unicity of typing property.
  • Every syntax tree has as most one assignment of typing attributes to its nodes.
  • If P:T holds, then T is unique.
• Unicity of Typing holds for Numeral.
  • By single typing rule, if N:T holds, then T = int (for all N in Numeral).
• Unicity of Typing holds for Location.
  • By single typing rule, if L:T holds, then T = intloc (for all L in Location).