🧞
ChatGPTとpythonでいつの間にか依存型に入門させられていた
はじめに
S式の自動生成関数と、簡約関数、元のS式と簡約させた式をラベルとした組をTransformerに学習させてどこまで学習できるか試す、S式GeneratorとTransformerによるDiscreminatorをGAN的に対決させて最もそれっぽいS式？を目指すと言った遊びをしていました。
pythonにはhy(hylang)というライブラリがあり、これはpythonをlisp風に使う、あるいはpython風のlisp(の方言)と言えるものです。list, dict,import with構文などもS式として表現されています。hyのevalを使えば文字列としてのS式を評価できます。hylangのpython側にはSymbol(S式)以外の幾つかのクラスが定義されていますが、基本的にSymbolとeval)があれば利用できます。
結局listや辞書の表記法や部分簡約、簡約ステップ数がほしいという理由からhyは使わずにChatGPTにS式処理系を実装してもらいました。その過程で
値::=0,1,2,3,4,5,6
bool::=True,False
ops::=+,-,*,/
cmps:==,<,>,<=,>=
変数::=x,y,z,t,v0,v1,...
list::=[expr,...]
expr::=値 | bool | 変数
| (ops expr,...）-> 値
| (cmps expr,...）-> bool
| (if expr expr expr)-> expr
| (fn [変数,...] expr) -> closure
| (expr expr,...)-> expr
| (compose expr expr)-> expr
| (partial expr expr,...)-> expr
| (map expr list)-> list
| (filter expr list)-> list
| (reduce expr list expr)-> expr
| (cons expr list)-> list
| (first list)-> expr
| (rest list)-> list
| (append list list)-> list
| (len list)-> 値
のような疑似BNF記法で書かれた文法の簡約化処理としてChatGPTが出してきたコードが以下のようなものです。
### S式(expr)自動生成関数 ###
# ---- 終端生成（深さが尽きたとき用） --------------------------
def gen_terminal(depth, want_kind="any"):
# 深さ 0 のときに使う、できるだけ型を合わせた終端
if want_kind == "int":# 値 or 変数を int 扱い
if random.random() < 0.7:
return random.choice(VALUES), "int"
else:
return random_var(), "int"
elif want_kind == "bool":
return random.choice(BOOLS), "bool"
elif want_kind == "list":# 空リストを返しておく
return "[]", "list"
elif want_kind == "closure": # 単純な恒等関数
v = random_var()
return f"(fn [{v}] {v})", "closure"
else:
# any の場合はランダムに選ぶ
choice = random.choice(["int", "bool", "list", "closure"])
return gen_terminal(depth, choice)
# ---- list リテラル -----------------------------------------
def gen_list_literal(depth):
# list ::= [expr,...]
# 深いほど要素数を増やし、各要素も複雑にする
if depth <= 0:
n = random.randint(0, 2)
else:
n = random.randint(2, 5)
elems = [gen_expr(depth - 1, "any")[0] for _ in range(n)]
return "[" + " ".join(elems) + "]", "list"
# ---- 各コンストラクタ（型つき） ----------------------------
def gen_op(depth): # (opsymbols expr,... ) -> 値 (int)
op = random.choice(OPS)
arity = random.randint(2, 4)
args = [gen_expr(depth - 1, "int")[0] for _ in range(arity)]
return "(" + " ".join([op] + args) + ")", "int"
def gen_cmp(depth): # (cmpsymbols expr,... ) -> bool
op = random.choice(CMPS)
arity = random.randint(2, 3)
args = [gen_expr(depth - 1, "int")[0] for _ in range(arity)]
return "(" + " ".join([op] + args) + ")", "bool"
def gen_if(depth, want_kind): # (if expr expr expr) -> want_kind
cond = gen_expr(depth - 1, "bool")[0]
then_expr, _ = gen_expr(depth - 1, want_kind)
else_expr, _ = gen_expr(depth - 1, want_kind)
return f"(if {cond} {then_expr} {else_expr})", want_kind
def gen_fn(depth):
# (fn [変数,...] expr) -> closure
num_params = random.randint(1, 3)
params = [random_var() for _ in range(num_params)]
# 関数本体は any 型にしておく
body, _ = gen_expr(depth - 1, "any")
return "(fn [" + " ".join(params) + "] " + body + ")", "closure"
...(中略)...
# ---- expr 生成のメイン -------------------------------------
def gen_expr(depth, want_kind="any"):
"""
指定された戻り値「kind」を持つ expr をランダム生成する。
want_kind: "int", "bool", "list", "closure", "any"
"""
if depth <= 0:
return gen_terminal(depth, want_kind)
# 深さがまだある場合は、なるべく「計算ステップが多くなりそうな」コンストラクタを優先
# kindごとに候補を用意
if want_kind == "int":
candidates = [
("value_terminal", 1),
("op", 4),
("len", 3),
("reduce", 4),
("if_int", 2),
("app", 2),
]
elif want_kind == "bool":
candidates = [
("bool_terminal", 1),
("cmp", 5),
("if_bool", 2),
("app", 1),
]
elif want_kind == "list":
candidates = [
("list", 5),
("if_list", 2),
("app", 1),
]
elif want_kind == "closure":
candidates = [
("fn", 4),
("compose", 3),
("partial", 3),
("if_closure", 1),
]
else: # any
...(中略）
kinds = [c[0] for c in candidates]
weights = [c[1] for c in candidates]
k = random.choices(kinds, weights=weights, k=1)[0]
# 各候補ごとの生成
if k == "value_terminal":
return gen_terminal(depth, "int")
if k == "bool_terminal":
return gen_terminal(depth, "bool")
if k == "op":
return gen_op(depth)
if k == "cmp":
return gen_cmp(depth)
if k == "len":
return gen_len(depth)
...
ここではkindは実質的に普通のプログラミング言語の型でintやboolのような基本型の他に特定の高階関数も型扱いされています(kindという名前は(Haskellのkindに由来するようです))。例えばmapやreduceの引数に(関数, list)以外のものが入っても処理できず簡約は止まってしまいます(そのようにChatGPT)に書いてもらいました。これによってランダムに生成するのではなく型(kind)があっているかどうかで最後まで簡約(計算)可能なS式のみを生成することが原理的には可能です。
型の階層と依存型
Haskellのようなある種の関数型言語やCoq, leanのような定理証明支援系の言語には依存型という値のような階層的で演算可能な性質をもった型システムがあります。これによって特定のサイズのlistやtensorが定義できてコンパイル時にtensorのサイズがあっているかがわかる、コンパイル可能なことを持ってプログラムや数学的証明の妥当性が示せると言った性質を持っています。とはいえ普通のプログラミング言語であることに代わりはなく別のプログラミング言語、今回はPython上に実装することが原理的には可能です。
そこで調子に乗ってkindを依存型のように演算可能に拡張した場合をpythonベースのS式処理系を作ってもらおうとしました。すると謎の用語を説明しだしました。
今の簡約器ではだいたいこうなっていますよね：
- 値: int, bool, list, closure, any くらいの kind
- 式: (+ 1 2), (map f [1 2 3]), (fn [x] (+ x 1)) … (expr)
- 式と kind: 「この expr は int を返す」「これは list を返す」
依存型付きの世界では、それをもう 1 段きちんと分けます：
- term（値レベルの項）
自然数 0, 1, 2, …、ベクトル Vec A n の具体的な値 - type（型）
Nat, Bool, Vec Nat 3, ∀ n : Nat, Vec Nat n → Nat など
依存型の場合、term に依存する type を持つ - universe / sort / kind
Type 0, Type 1, … とか Prop など
「型の型」を分類するもの（Lean の Sort u）
あなたが「kind」と呼んでいたものを、そのまま「Type の universe」に昇格させる
あるいは「Haskell の kind（*, * -> *）」のように上位分類にすることで、Lean 風の依存型システムを S 式で書けます。
だそうです。
依存型を含んだ文法
「型の型」sortに対して拡張された文法は
sort ::= Type0 | Type1 | Prop ; 宇宙 / kind
expr ::= x ; 変数
| (lambda ((x expr)) expr) ; λx:A. t
| (pi ((x expr)) expr) ; Πx:A. B (依存関数型)
| (expr expr) ; 関数適用
| Nat | zero | (succ expr) ; 自然数
| (eq expr expr) ; 同値型
| (Vec expr expr) ; Vec A n (型コンストラクタも expr)
| (match expr ... ) ; パターンマッチ（iota 簡約の源）
| ... ; 他の帰納的型
ctx ::= [(x expr) ...] ; x : A, y : B, ... という型付きコンテキスト
judg ::= (|- ctx expr expr) ; Γ ⊢ t : T
となるそうです。ctxは上記のclosureで底に型情報が入ります。最後の
judg ::= (|- ctx expr expr) ; Γ ⊢ t : T
Γ ⊢ t : T のΓは型コンテキスト(型と変数の対応関係の集合),Tは型、tは項(値)だそうで型のClosureみたいになってますSimply typed lambda calculus
例として
- 恒等関数
; λ (A : Type0) (x : A), x
(lambda ((A Type0))
(lambda ((x A))
x))
- 依存関数型（Lean の Π A : Type, A → A）
(pi ((A Type0))
(pi ((x A)) A))
- 長さ付きベクトル Vec
; Vec : Π (A : Type0), Nat → Type0
; これも expr として扱う
(Vec A n)
- ベクトルの長さを返す関数（型だけ）
; length : Π (A : Type0) (n : Nat), Vec A n → Nat
(pi ((A Type0))
(pi ((n Nat))
(pi ((v (Vec A n)))
Nat)))
を挙げています。ここでは Type0 も Nat も Vec も全部 expr の一種です
Lean も内部的にはそうなっていて、Sort u や Const など AST ノードになっているだけです
(そうなのか？計算機だからそうなのだろうが…)
いきなり出てきたΠは「依存関数型」、Leanでは∀で書かれるそうです。簡単な説明として長さnのVector型を返す関数
∀ n : Nat, Vector Nat n
とそれを使って関数vecHeadの出力が空でないことを保証したプログラムを示しています。
def vecHead: Π {A : Type} {n : Nat}, Vector A (Nat.succ n) → A :=
fun A n v => match v with | .cons x _ => x
vの型にNat.succ n が入っているので、空リストではないことが型で保証され、パターンマッチで .cons しか来ないことが保証されているので、安心して使うことができることになります。
型推論と簡約
よって
型推論（型検査）:
- Γ ⊢ t : T が成り立つかどうかと、T を求める
簡約（計算）: - β簡約：((lambda (x A) body) arg) → body[x := arg]
- ι簡約：(match (succ n) ... ) → ... など
- δ簡約：定義展開（Lean の定義を unfold）
ができれば型推論、証明の記述と検証ができるとしています。型推論は型のある言語で主にコンパイル時に行われているものです。実質的には木であるS式(expr)の簡約は型なしλ計算にもあるβ簡約でδ簡約は変数名を値で置き換えます。ι簡約は帰納法で用いられるものらしくCoqでは(match-reduction, eliminates match, fix-reduction)
cofix-reduction)、Coqでの説明が詳しいです。
Lean,Coqには帰納法のための型があります。
よってpythonでも
- expr の内部表現を S 式（木構造）にする
- type_of(expr) を計算する関数を持つ
- normalize(expr)（正規形への簡約）を定義する
を実装することで依存型言語処理系が実現できるとしています。
実際evalと呼んでいたものがkindも込みでnormalize(expr)とされ、type_of(expr)ではisinstance関数を使いまくって実現しています。
簡略化されたAST
from dataclasses import dataclass
from typing import Dict, List, Optional, Union
# Expr AST
@dataclass
class Sort:
level: int # Type0, Type1, ...
@dataclass
class Var:
name: str
@dataclass
class Pi:
var: str
var_type: Expr
body: Expr # body は var に依存できる
@dataclass
class Lam:
var: str
var_type: Expr
body: Expr
@dataclass
class App:
fn: Expr
arg: Expr
@dataclass
class Nat:
pass
@dataclass
class Zero:
pass
@dataclass
class Succ:
n: Expr
Expr = Union[Sort, Var, Pi, Lam, App, Nat, Zero, Succ]
Context = Dict[str, Expr] # x : A
def type_of(ctx: Context, t: Expr) -> Expr:
if isinstance(t, Sort):
# Type_i : Type_{i+1} 的な
return Sort(t.level + 1)
if isinstance(t, Var):
return ctx[t.name]
if isinstance(t, Nat):
return Sort(0)
if isinstance(t, Zero):
return Nat()
if isinstance(t, Succ):
n_ty = type_of(ctx, t.n)
# n : Nat であることをチェック
if not isinstance(n_ty, Nat):
raise TypeError("succ expects Nat")
return Nat()
if isinstance(t, Pi):
A_ty = type_of(ctx, t.var_type)
B_ty = type_of({**ctx, t.var: t.var_type}, t.body)
# 実際は宇宙レベルのmaxを取るなど
return Sort(0)
if isinstance(t, Lam):
A = t.var_type
B = type_of({**ctx, t.var: A}, t.body)
return Pi(t.var, A, B)
if isinstance(t, App):
fn_ty = type_of(ctx, t.fn)
if not isinstance(fn_ty, Pi):
raise TypeError("fn is not pi-type")
arg_ty = type_of(ctx, t.arg)
# arg_ty と fn_ty.var_type が同じか（≃か）チェック
# 依存型の場合、body で x を arg に置換して型を求める
return subst(fn_ty.body, fn_ty.var, t.arg)
raise NotImplementedError
これにβ簡約 normalize(t)を加えれば
- (Lam("x", Nat(), Var("x"))) を _ に適用したらβ簡約
- Pi による依存関数型もtype_ofでそのまま扱える
ことになります。
簡単な証明機能
そして非常に基本的な証明機能proveは以下のようになります。
from __future__ import annotations
from dataclasses import dataclass
from typing import List, Optional, Tuple, Union
# ======================
# 1. 論理式 (Formula)
# ======================
@dataclass(frozen=True)
class PropVar:
name: str # 命題変数 P, Q, R ...
@dataclass(frozen=True)
class Imp:
"""含意 A → B"""
left: "Formula"
right: "Formula"
@dataclass(frozen=True)
class And:
"""連言 A ∧ B"""
left: "Formula"
right: "Formula"
Formula = Union[PropVar, Imp, And]
# ======================
# 2. 項 (Proof Term)
# ======================
@dataclass
class TermVar:
name: str # 証明項としての変数 (Curry–Howard の "変数 = 仮定の証明")
@dataclass
class Lam:
"""λx. body （A→B の導入）"""
var: str
var_type: Formula
body: "Term"
@dataclass
class App:
"""関数適用 (f a) （→ 消去 = modus ponens に対応）"""
fn: "Term"
arg: "Term"
@dataclass
class Pair:
"""(p, q) : A∧B の証明"""
fst: "Term"
snd: "Term"
@dataclass
class Fst:
"""fst t : A∧B → A の証明"""
pair: "Term"
@dataclass
class Snd:
"""snd t : A∧B → B の証明"""
pair: "Term"
Term = Union[TermVar, Lam, App, Pair, Fst, Snd]
# ======================
# 3. コンテキスト Γ
# ======================
# Γ は (変数名, 型=論理式) のリスト
Context = List[Tuple[str, Formula]]
# ======================
# 4. 証明探索 prove
# ======================
def prove(ctx: Context, goal: Formula, fresh_id: int = 0) -> Optional[Term]:
"""
Γ ⊢ goal を探す。
証明が見つかれば Term を返し、失敗すれば None。
fresh_id は λ や中間変数生成用のカウンタ。
"""
# 1) すでに仮定に同じ型があるなら、それを使う（仮定の利用）
for (x, ty) in ctx:
if ty == goal:
return TermVar(x)
# 2) ゴールが含意 A → B なら、A を仮定に追加して B を証明する（→ 導入）
if isinstance(goal, Imp):
arg_name = f"x{fresh_id}"
new_ctx = ctx + [(arg_name, goal.left)]
body = prove(new_ctx, goal.right, fresh_id + 1)
if body is not None:
return Lam(arg_name, goal.left, body)
# 3) ゴールが連言 A ∧ B なら、A と B をそれぞれ証明してペアにする（∧ 導入）
if isinstance(goal, And):
left_term = prove(ctx, goal.left, fresh_id)
if left_term is None:
return None
right_term = prove(ctx, goal.right, fresh_id + 1000) # 適当なずらし
if right_term is None:
return None
return Pair(left_term, right_term)
# 4) → 消去（modus ponens）: Γ に A→goal があれば、その A を証明して f a とする
for (x, ty) in ctx:
if isinstance(ty, Imp) and ty.right == goal:
# A→goal の A を証明してから適用
arg_term = prove(ctx, ty.left, fresh_id + 2000)
if arg_term is not None:
return App(TermVar(x), arg_term)
# 5) ∧ 消去: もしゴールが A で、Γ に A∧B があれば fst で取り出せる
for (x, ty) in ctx:
if isinstance(ty, And) and ty.left == goal:
return Fst(TermVar(x))
if isinstance(ty, And) and ty.right == goal:
return Snd(TermVar(x))
# これ以上のルールがなければ失敗
return None
# ======================
# 5. pretty-print
# ======================
def formula_to_str(f: Formula) -> str:
if isinstance(f, PropVar):
return f.name
if isinstance(f, Imp):
return f"({formula_to_str(f.left)} → {formula_to_str(f.right)})"
if isinstance(f, And):
return f"({formula_to_str(f.left)} ∧ {formula_to_str(f.right)})"
return "<?>"
def term_to_str(t: Term) -> str:
if isinstance(t, TermVar):
return t.name
if isinstance(t, Lam):
return f"(λ {t.var}:{formula_to_str(t.var_type)}. {term_to_str(t.body)})"
if isinstance(t, App):
return f"({term_to_str(t.fn)} {term_to_str(t.arg)})"
if isinstance(t, Pair):
return f"({term_to_str(t.fst)}, {term_to_str(t.snd)})"
if isinstance(t, Fst):
return f"(fst {term_to_str(t.pair)})"
if isinstance(t, Snd):
return f"(snd {term_to_str(t.pair)})"
return "<?term?>"
# ======================
# 6. デモ
# ======================
if __name__ == "__main__":
# 命題変数
A = PropVar("A")
B = PropVar("B")
C = PropVar("C")
# 例1: A, A→B ⊢ B （modus ponens）
ctx1: Context = [("hA", A), ("hImp", Imp(A, B))]
goal1 = B
proof1 = prove(ctx1, goal1)
print("Goal:", formula_to_str(goal1))
print("Proof term:", term_to_str(proof1) if proof1 else "not provable")
print()
# 例2: A, B ⊢ A ∧ B
ctx2: Context = [("hA", A), ("hB", B)]
goal2 = And(A,B)
proof2 = prove(ctx2, goal2)
print("Goal:", formula_to_str(goal2))
print("Proof term:", term_to_str(proof2) if proof2 else "not provable")
print()
# 例3: A∧B ⊢ A
ctx3: Context = [("hAB", And(A,B))]
goal3 = A
proof3 = prove(ctx3, goal3)
print("Goal:", formula_to_str(goal3))
print("Proof term:", term_to_str(proof3) if proof3 else "not provable")
print()
# 例4: ⊢ A→A
ctx4: Context = []
goal4 = Imp(A, A)
proof4 = prove(ctx4, goal4)
print("Goal:", formula_to_str(goal4))
print("Proof term:", term_to_str(proof4) if proof4 else "not provable")
対話全文
最初タイプミスしてます。
コード、概略なのでそのままでは動きません。randhof_with_weight.pyをimportしてください。
感想
LLMと定理証明支援系を合体させて超数学得意AIを作るのが流行っていますがAI(ChatGPT)自身もかなり定理証明支援系のことを理解しているようです。個人的にはleanなど定理証明支援系に帰納法を単調に減少する変数を見出し、ヒントを与えて説かせるところまでは理解できたので、定理で帰納法、あるいは他の方法が使えるということを発見させる。単調減少する数を見出させることをやってみたいです。
この知識はどこから来たのか
型付きλ計算と呼ばれる分野らしいです。
既に述べたとおりι変換に関してはCoqのドキュメントが詳しく、Coq, Leanには帰納法のための型が有ります。
依存型リンク
http://www.a-k-r.org/pub/2018-09-02-deptype-proofsummit2018.pdf Coq ユークリッドの互除法(最大公約数を求める)が停止することの証明
Coqのcbv
Cbv は Coq の自動簡約（evaluation）タクティックのひとつで、名前は Call‐By‐Value（値呼び）に由来します。
Coq には項（証明項・関数定義）を簡約・評価するための複数のタクティックがあり
| tactic | 評価戦略 | 例 |
|---|---|---|
cbv |
call‐by‐value（値呼びで簡約 | cbv β iota zeta delta |
cbn |
call‐by‐name（名前呼び）寄り | cbn |
compute |
全展開（重い） | compute |
simpl |
ルールベースで軽量簡約 | simpl |
cbvはそのうち、項を call-by-value の戦略で厳密＆可制御に簡約するためのタクティックで以下の簡約をサポート：
- β（ラムダ計算：関数適用）
- δ（定義 unfold）
- ι（match/if の分岐消去）
- ζ（let 展開）
- η（η 簡約）
- fix（再帰 unfolding、要例外指定）
hylang情報
おすすめ本
Discussion