Type Systems : Sample Typing Proof

Show:

? |- (?f: int?int . (?g: int?int . (?x:int . (f (g x))))): (int?int) ? ((int?int) ? (int?int))

Tree1: f :int?int, g :int?int, x:int |- g :int?int, f :int?int, g :int?int, x:int |- x :int

f :int?int, g :int?int, x:int |- (g x): int

Tree2: f :int?int, g :int?int, x:int |- f :int?int, Tree1

f :int?int, g :int?int, x:int |- (f (g x)): int

f :int?int, g :int?int |- (? x:int . (f (g x))): int?int

f :int?int |- ((? g :int?int . (? x:int . (f (g x)))) : (int?int) ? (int?int)

? |- (? f :int?int . (? g :int?int . (? x:int . (f (g x))))) : (int?int) ? ((int?int) ? (int?int))

Previous slide

Next slide

Back to first slide

View graphic version