Чтение дерева вывода типов

Как выглядит «доказательство, что выражение типизируется», и как читать его сверху вниз.

Дерево вывода (derivation) — построение суждения Γ |- e : T применением правил: листья — аксиомы (Var), узлы — правила (Abs, App), корень — доказанное суждение.

Что такое дерево вывода

Когда чекер говорит «терм имеет тип T», за этим стоит формальный объект — дерево вывода. Это доказательство в чистом виде: чтобы заключить суждение под чертой, мы предъявляем доказательства посылок над чертой, и так рекурсивно до аксиом. Читать дерево можно двояко: снизу вверх («чтобы доказать это, мне нужно доказать вот это») — так работает проверка; сверху вниз («из этих фактов следует вот это») — так читается готовое доказательство.

Пример: тип функции тождества

Построим вывод для |- (\x:Int. x) : Int -> Int. Внизу — то, что доказываем; вверх растут посылки.

         x : Int принадлежит (x : Int)
        ------------------------------- (Var)
              x : Int |- x : Int
        ------------------------------- (Abs)
          |- (\x:Int. x) : Int -> Int

Читаем снизу вверх: чтобы по (Abs) получить тип Int -> Int для функции, надо показать, что тело x имеет тип Int в контексте x : Int. Это даёт правило (Var), потому что пара x : Int есть в контексте. Дерево замкнулось аксиомой — доказательство построено.

Пример посложнее: аппликация

Вывод для f : Int -> Bool, y : Int |- f y : Bool. У правила (App) две посылки, поэтому дерево ветвится.

  f:Int->Bool принадлежит Г        y:Int принадлежит Г
 ----------------------- (Var)    ----------------- (Var)
  Г |- f : Int -> Bool             Г |- y : Int
 ------------------------------------------------- (App)
                 Г |- f y : Bool

где Г = f : Int -> Bool, y : Int

Две ветви над чертой (App) — это две посылки правила: «слева функция-стрелка» и «справа аргумент нужного типа». Обе доказываются через (Var). Корень — искомый тип Bool.

Демонстрация: чекер, печатающий шаги вывода

Добавим к чекеру трассировку: пусть он печатает применённое правило и полученное суждение. Так мы увидим дерево вывода как последовательность шагов (в порядке завершения, то есть от листьев к корню).

def arrow(a,b): return ("->",a,b)
def show(t):
    if isinstance(t,str): return t
    l=show(t[1])
    if isinstance(t[1],tuple): l="("+l+")"
    return l+" -> "+show(t[2])
def var(n): return ("var",n)
def lam(p,ty,b): return ("lam",p,ty,b)
def app(f,a): return ("app",f,a)

def gshow(g):
    return "{" + ", ".join(k+":"+show(v) for k,v in g.items()) + "}"

def check(e, g):
    if e[0]=="var":
        t=g[e[1]]
        print("(Var)", gshow(g), "|-", e[1], ":", show(t))
        return t
    if e[0]=="lam":
        ng=dict(g); ng[e[1]]=e[2]
        bt=check(e[3], ng)
        t=arrow(e[2], bt)
        print("(Abs)", gshow(g), "|- (\\"+e[1]+":"+show(e[2])+". ...) :", show(t))
        return t
    if e[0]=="app":
        ft=check(e[1], g); at=check(e[2], g)
        t=ft[2]
        print("(App)", gshow(g), "|- (f a) :", show(t))
        return t

term = lam("x","Int", var("x"))
print("== вывод для \\x:Int. x ==")
top = check(term, {})
print("ИТОГ:", show(top))

Вывод:

== вывод для \x:Int. x ==
(Var) {x:Int} |- x : Int
(Abs) {} |- (\x:Int. ...) : Int -> Int
ИТОГ: Int -> Int

Порядок печати (сначала Var, потом Abs) — это обход дерева в порядке завершения: листья доказываются раньше корня. Соедините строки мысленно в дробь — получите дерево из ASCII-примеров выше.

Как работает под капотом

Деревья вывода — не учебная декорация, а реальный объект: в системах вроде Coq построенное дерево вывода и есть доказательство, и его можно сохранить, переслать, перепроверить независимо. Эта мысль — мост к разделу про соответствие Карри — Говарда: дерево типового вывода буквально является доказательством соответствующего логического утверждения.

Частые ошибки

• Путать направление чтения. Проверка идёт снизу вверх (от цели к посылкам), но логически дерево обосновано сверху вниз (от аксиом к цели).
• Забывать ветвление App. У (App) две посылки — дерево ветвится; пропустив одну ветвь, вы «докажете» неверное.
• Считать дерево уникальным. В STLC оно по сути единственно (синтаксическая направленность), но в богатых системах деревьев может быть много или ни одного.

Итоги

• Дерево вывода — формальное доказательство суждения Γ |- e : T.
• Листья — аксиомы (Var), внутренние узлы — правила (Abs, App), корень — цель.
• Проверка читает дерево снизу вверх; обоснование — сверху вниз от аксиом.
• В Coq/Agda дерево вывода и есть проверяемое доказательство (мост к Карри — Говарду).