Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- (((λ x : Bool . (λ y : Bool . (x , y))) true) false) . 2
- --------------------------------------------------------
- ----- S-x-23 -------- S-T-2 ----- S-Γ-0 ----- S-Γ-0 ----- S-x-23 -------- S-T-2 ----- S-Γ-0 ----- S-x-23 -------- S-T-2 ----- S-Γ-0 ----- S-x-23 -------- S-T-2 ----- S-Γ-0 ----- S-x-23 -------- S-T-2
- x ← x Bool ← T ∅ ← Γ ∅ ← Γ x ← x Bool ← T ∅ ← Γ x ← x Bool ← T ∅ ← Γ x ← x Bool ← T ∅ ← Γ x ← x Bool ← T
- ------------------------------------- T-Ctx1 ----- S-x-23 -------- S-T-2 ------------------------------------- S-Γ-1 ----- S-x-24 -------- S-T-2 ------------------------------------- S-Γ-1 ----- S-x-24 -------- S-T-2 ----- S-x-24 -------- S-T-2 ------------------------------------- S-Γ-1 ------------------------------------- S-Γ-1 ----- S-x-24 -------- S-T-2 ----- S-Γ-0 ----- S-x-23 -------- S-T-2
- (x : Bool) ∈ (∅ , x : Bool) x ← x Bool ← T (∅ , x : Bool) ← Γ y ← x Bool ← T (∅ , x : Bool) ← Γ y ← x Bool ← T y ← x Bool ← T (∅ , x : Bool) ← Γ (∅ , x : Bool) ← Γ y ← x Bool ← T ∅ ← Γ x ← x Bool ← T
- ----------------------------------------------------------------------------------------------------------------------------------------------- T-Ctx2 ------------------------------------------------------------ S-Γ-1 ----- S-x-23 -------- S-T-2 ----------------------------------------------------------- T-Ctx1 ------------------------------------------------------------ S-Γ-1 ----- S-x-24 -------- S-T-2 ------------------------------------- S-Γ-1 ----- S-x-24 -------- S-T-2 ----- S-x-23 ----- S-x-24 ----- S-x-23 ----- S-x-24 ----- S-x-23 ----- S-x-24 ----- S-x-23 ----- S-x-24 ----- S-x-23 ----- S-x-24 ----- S-x-23 ----- S-x-24
- (x : Bool) ∈ ((∅ , x : Bool) , y : Bool) ((∅ , x : Bool) , y : Bool) ← Γ x ← x Bool ← T (y : Bool) ∈ ((∅ , x : Bool) , y : Bool) ((∅ , x : Bool) , y : Bool) ← Γ y ← x Bool ← T (∅ , x : Bool) ← Γ y ← x Bool ← T x ← x y ← x x ← x y ← x x ← x y ← x x ← x y ← x x ← x y ← x x ← x y ← x
- ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- T-Var -------------------------------------------------------------------------------------------------------------------------------------------------------------------------- T-Var ------------------------------------------------------------ S-Γ-1 ----- S-t-0 ----- S-t-0 -------- S-T-2 -------- S-T-2 ----- S-Γ-0 ----- S-x-23 -------- S-T-2 ----- S-t-0 ----- S-t-0 -------- S-T-2 -------- S-T-2 ----- S-t-0 ----- S-t-0 -------- S-T-2 -------- S-T-2 ----- S-t-0 ----- S-t-0 ----- S-t-0 ----- S-t-0 ----- S-t-0 ----- S-t-0
- ((∅ , x : Bool) , y : Bool) ⊢ x : Bool ((∅ , x : Bool) , y : Bool) ⊢ y : Bool ((∅ , x : Bool) , y : Bool) ← Γ x ← t y ← t Bool ← T Bool ← T ∅ ← Γ x ← x Bool ← T x ← t y ← t Bool ← T Bool ← T x ← t y ← t Bool ← T Bool ← T x ← t y ← t x ← t y ← t x ← t y ← t
- ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- T-Pair ------------------------------------- S-Γ-1 ----- S-x-24 -------- S-T-2 -------------------- S-t-3 ------------------------- S-T-1 ----- S-x-24 -------- S-T-2 -------------------- S-t-3 -------- S-T-2 ------------------------- S-T-1 ----- S-x-24 -------- S-T-2 -------------------- S-t-3 -------- S-T-2 -------- S-T-2 ----- S-x-24 -------- S-T-2 -------------------- S-t-3 ----- S-x-24 -------- S-T-2 -------------------- S-t-3
- ((∅ , x : Bool) , y : Bool) ⊢ (x , y) : (Bool × Bool) (∅ , x : Bool) ← Γ y ← x Bool ← T (x , y) ← t (Bool × Bool) ← T y ← x Bool ← T (x , y) ← t Bool ← T (Bool × Bool) ← T y ← x Bool ← T (x , y) ← t Bool ← T Bool ← T y ← x Bool ← T (x , y) ← t y ← x Bool ← T (x , y) ← t
- ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- T-Abs ----- S-Γ-0 ----- S-x-23 -------- S-T-2 ----------------------------------------------- S-t-1 -------------------------------------- S-T-0 ----- S-Γ-0 ----- S-x-23 -------- S-T-2 ----------------------------------------------- S-t-1 -------- S-T-2 ------------------------- S-T-1 ----- S-x-23 -------- S-T-2 ----------------------------------------------- S-t-1 ----- S-x-23 -------- S-T-2 ----------------------------------------------- S-t-1
- (∅ , x : Bool) ⊢ (λ y : Bool . (x , y)) : (Bool → (Bool × Bool)) ∅ ← Γ x ← x Bool ← T (λ y : Bool . (x , y)) ← t (Bool → (Bool × Bool)) ← T ∅ ← Γ x ← x Bool ← T (λ y : Bool . (x , y)) ← t Bool ← T (Bool × Bool) ← T x ← x Bool ← T (λ y : Bool . (x , y)) ← t x ← x Bool ← T (λ y : Bool . (x , y)) ← t
- --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- T-Abs --------------- T-True ----- S-Γ-0 -------------------------------------------------------------------- S-t-1 -------- S-t-6 -------------------------------------- S-T-0 ----- S-Γ-0 -------------------------------------------------------------------- S-t-1 -------- S-t-6 -------- S-T-2 -------- S-T-2 -------------------------------------------------------------------- S-t-1 -------- S-t-6
- ∅ ⊢ (λ x : Bool . (λ y : Bool . (x , y))) : (Bool → (Bool → (Bool × Bool))) ∅ ⊢ true : Bool ∅ ← Γ (λ x : Bool . (λ y : Bool . (x , y))) ← t true ← t (Bool → (Bool × Bool)) ← T ∅ ← Γ (λ x : Bool . (λ y : Bool . (x , y))) ← t true ← t Bool ← T Bool ← T (λ x : Bool . (λ y : Bool . (x , y))) ← t true ← t
- --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- T-App ---------------- T-False ----- S-Γ-0 ----------------------------------------------------------------------------------------- S-t-2 --------- S-t-7 ------------------------- S-T-1 ----------------------------------------------------------------------------------------- S-t-2 --------- S-t-7
- ∅ ⊢ ((λ x : Bool . (λ y : Bool . (x , y))) true) : (Bool → (Bool × Bool)) ∅ ⊢ false : Bool ∅ ← Γ ((λ x : Bool . (λ y : Bool . (x , y))) true) ← t false ← t (Bool × Bool) ← T ((λ x : Bool . (λ y : Bool . (x , y))) true) ← t false ← t
- ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- T-App ----- S-Γ-0 --------------------------------------------------------------------------------------- S-t-2 -------- S-T-2
- ∅ ⊢ (((λ x : Bool . (λ y : Bool . (x , y))) true) false) : (Bool × Bool) ∅ ← Γ (((λ x : Bool . (λ y : Bool . (x , y))) true) false) ← t Bool ← T
- ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- T-Proj2
- ∅ ⊢ ((((λ x : Bool . (λ y : Bool . (x , y))) true) false) . 2) : Bool
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
