Exercises

I doubt I'll ever get around to doing all the exercises in any of the books I like, but I want a way to remember the the solutions that I could figure out.

TAPL - Benjamin Pierce

5.2.1

{- logical or -}
or = λa. λb. a tru b

{-
| a   | b   | or a b            |
|-----+-----+-------------------|
| tru | tru | tru tru tru = tru |
| tru | fls | tru tru fls = tru |
| fls | tru | fls tru tru = tru |
| fls | fls | fls tru fls = fls |
-}

{- logical and -}
and = λa. λb. a b fls

{-
| a   | b   | and a b           |
|-----+-----+-------------------|
| tru | tru | tru tru fls = tru |
| tru | fls | tru fls fls = fls |
| fls | tru | fls tru fls = fls |
| fls | fls | fls fls fls = fls |
-}

{- logical not -}
and = λa. a fls tru

{-
| a   | not a             |
|-----+-------------------|
| tru | tru fls tru = fls |
| fls | fls fls tru = tru |
-}

6.1.1

Named term (question) de-Bruijn index term (answer)
λs. λz. z; λ.λ. 0;
λs. λz. s (s z); λ.λ. 1 (1 0);
λm. λn. λs. λz. m s (n z s); λ.λ.λ.λ. 3 1 (2 0 1);
λf. (λx. f (λy. (x x) y)) (λx. f (λy. (x x) y)); λ. (λ. 1 (λ. (1 1) 0)) (λ. 1 (λ. (1 1) 0));
(λx. (λx. x)) (λx. x); (λ. (λ. 0)) (λ. 0);

6.2.2

-- Exercise: 6.2.2
-- Part 1
shift(2) (λ.λ. 1 (0 2))
= λ. shift(2, 1) (λ. 1 (0 2))
= λ. λ. shift(2, 2) (1 (0 2))
= λ. λ. 1 (0 4)

-- Part 2
shift(2) (λ. 0 1 (λ. 0 1 2))
= λ. shift(2,1) (0 1 (λ. 0 1 2))
= λ. 0 3 (λ. shift(2,2) (0 1 2))
= λ. 0 3 (λ. 0 1 4)

1. ↑² (λ.λ. 1 (0 2))
   - ↑²₀ (λ.λ. 1 (0 2))
   - λ. ↑²₁(λ. 1 (0 2))
   - λ. λ. ↑²₂(1 (0 2))
   - λ. λ. (↑²₂ 1) (↑²₂ (0 2))
   - λ. λ. 1 (↑²₂ (0 2))
   - λ. λ. 1 ((↑²₂ 0) (↑²₂ 2))
   - λ. λ. 1 (0 4)

2. ↑² (λ. 0 1 (λ. 0 1 2))
   - ↑²₀ (λ. 0 1 (λ. 0 1 2))
   - λ. ↑²₁ (0 1 (λ. 0 1 2))
   - λ. [↑²₁ (0 1)] [↑²₁ ((λ. 0 1 2))]
   - λ. (0 3) [↑²₁ ((λ. 0 1 2))]
   - λ. (0 3) (λ. [↑²₂ (0 1 2)])
   - λ. (0 3) (λ. (0 1 4))

6.2.5

1. [b ↦ a] (b (λx. λy. b))

Γ = {a, b}

Nameless form: Γ = {1, 0}

[0 ↦ 1] 0 (λ. λ. 1

13.1.1

Question

Draw a similar diagram showing the effects of evaluating the expressions a = {ref 0, ref 0} and b = (λx: Ref Nat. {x, x}) (ref 0).

Answer

a = {ref 0, ref 0}


a = { _, _}
      |  |
      ↓  ↓
    +---+---+
    |   |   |
    +---+---+

where the two elements of the record point to different memory locations.

And

b = (λx: Ref Nat. {x, x}) (ref 0)


b = { _, _}
      |  |
      ↓  ↓
      ↘  ↙
        ↓ 
      +---+
      |   |
      +---+

where both elements of the record point to the same memory location.

15.2.1

Question

Draw a derivation showing that {x:Nat, y:Nat, z:Nat} is a subtype of {y:Nat}.

Answer

{x:Nat, y:Nat, z:Nat} <: {x:Nat, y:Nat, z:Nat} (S-Refl)
{x:Nat, y:Nat, z:Nat} <: {x:Nat, y:Nat} (S-RcdWidth, k=1)
{x:Nat, y:Nat, z:Nat} <: {y:Nat, x:Nat} (S-RcdPerm)
{x:Nat, y:Nat, z:Nat} <: {y:Nat} (S-RcdWidth, k=1)

22.2.3

DONE 22.2.3

λx:X. λy:Y. λz:Z. (x z) (y z)

Type of bound variables are like:

x:_ -> _ -> _
y:_ -> _
z:_

y has to return something which x z can accept

x:A -> X -> _
y:A -> X
z:A

Rest can be anything.

x:A -> X -> B
y:A -> X
z:A

Some possible type unifiers:

DONE 22.4.3

String diagrams - Ralf Hinze, Dan Marsden

DONE 1.3

Category whose objects ∈ ℕ, and morphisms are nxm matrices.

(c * b) * a = c * (b * a)
id * a = a = a * id

Principles of abstract interpretation - Cousot

DONE 11.2 Galois connection for n ≤⌊x⌋⇔ n ≤ x

Let

∀ x y ∈ ℕ,
  ⌊x⌋ ≼ y   ↔   x ⊑ y

So,

  ⌊x⌋ ≼ y
=>  x ≤ y

   x ⊑ y
=> x ≤ y

LHS ↔ RHS
∎

∴ The Galois connection is (⌊x⌋, x).