Lambdas abstractions Types, Term building

Posted on March 1, 2020
Tags: typetheory

In programming types we are restricted to function or in logic implication.
Therefore it would be beneficial to learn about the different arrangements of function types and how to build terms for them.

(A1 -> (A2 -> (A3 -> B)))
A1 ∧ A2 ∧ A3 -> B
λa1 a2 a3, b

The above is trivial to understand

((A1 -> A2) -> A3) -> B is far more difficult to understand

For the rest of this notebook we assume type parenthesis are binded to the left (A -> B) -> C

1 Rules to building lambda terms

2 rules to building terms

2 Weak Peirce problem

def weak_peirce : ((((A → B) → A) → A) → B) → B :=
λX, X (λ Y, Y (λ a, (X (λ z, a)) ))
goal :: ((((A -> B) -> A) -> A) -> B) -> B
 
X :: (A -> B -> A -> A) -> B
Y :: A -> B -> A
a :: A
z :: A -> B -> A

(λ z, a) :: (A -> B -> A) -> A
(X (λ z, a)) :: B --apply X to (λ z, a)

3 Canonical patterns

(A1 -> (A2 -> (A3 -> B))) has its own pattern λ a1 a2 a3. b pushing everything as evidence in lambda abstraction
((A1 -> A2) -> B) -> B also has its own pattern

When all we have is ((A1 -> A2) -> B) -> B all we can do is extract function λf::((A1 -> A2) -> B)
and apply it to a placeholder λf::((A1 -> A2) -> B). (f _ ) meaning (f _ ) :: B

λf. (f _)
(...->B) -> B
notice the canonical patterns 
λX.(X _) :: (...->B)->B
λY.(Y _) :: (...->A)->A

\[\overbrace{\overbrace{\lambda X}^{(...) → B}. \overbrace{(X \square)}^{B}}^{((...) → B)→B)} \qquad \qquad \overbrace{\overbrace{\lambda Y}^{(A→ B) → A}. \overbrace{(Y \square)}^{A}}^{((A→ B) → A)→A)} \tag{canonical pattern}\]

\[\begin{align} {\color{purple}\lambda X. \overbrace{(X {\color{green}\square})}^{B}} \qquad \qquad & \tag{X::(A → B → A → A) → B}\\ {\color{green}\lambda Y. \overbrace{(Y {\color{blue}\square})}^{A}} \qquad & \tag{Y::(A → B) → A}\\ {\color{blue}\lambda a. \overbrace{({\color{red}\square})}^{B}} & \tag{a::A}\\ \end{align}\]

In the above 3 lambdas, if we keep plugging each one in to the next respective \(\square\) we get:

\[\lambda X. X (\lambda Y. Y( \lambda a. {\overbrace{\color{red}\square}^{B}}))\]

We need to fill in the placeholder with type \(B\)

3.1 Attempt Solution

  • First attempt, I had thought this looked like some recursion
    • \(\delta = (X (\lambda Y. \lambda a. {\color{red}\square})) :: B\)
    • \({\color{red}\square} = \delta\)
    • \(\delta = (X (\lambda Y. \lambda a. \delta))\) clearly wouldnt work but looks interesting maybe another Y combinator.
      The subterm of \(\delta\) depends on \({\color{red}\square}\).
      The subterm of \({\color{red}\square}\) depends on \(\delta\).

3.2 Proper solution

Scoping nested lambdas means we have access to binded lambda terms in the outer scope.

  • Solution, focus on \(\overbrace{(X \square)}^{B}\) to build a term for \({\overbrace{\color{red}\square}^{B}}\)
    • X :: (A -> B -> A -> A) -> B
    • So we need to build (A -> B -> A -> A)
      • Red herring: looks like Y but pointless since Y is already bounded
    • All we have to do is focus on the last type A of (A -> B -> A -> A)
    • We just need the superpower of lambda abstraction (λ z, a):: (...)->A

\[{\color{red}\square} = (\overset{((..)\rightarrow A) \rightarrow B}{X}(\underbrace{\lambda z. a}_{(..)\rightarrow A}))\]

This means the full solution is:

\[\lambda X. X (\lambda Y. Y(\lambda a. \overbrace{\overset{((..)\rightarrow A) \rightarrow B}{X}(\underbrace{\lambda z. a}_{(..)\rightarrow A})}^{B}))\]

λX, X (λ Y, Y (λ a, (X (λ z, a)) )) :: ((((A → B) → A) → A) → B) → B

4 Lesson learned