6 Abstractions and quantifiers

(* 本章より，入力行の先頭の#記号も記しますが，それ自体は入力ではありません．*)
　前の章の最初に挙げたtermの４つの目の種類，abstractionsについて述べます．
　3.3で紹介したINSTのtypeは

# INST;;
val it : (term * term) list -> thm -> thm =

なので，theoremに現れる複数の自由変数を例えば

# ARITH_RULE `x+y=y+x`;;
val it : thm = |- x + y = y + x
# INST[(`a:num`,`x:num`);(`1`,`y:num`)] it;;
val it : thm = |- a + 1 = 1 + a

のように置き換えることができます．
　HOL Lightが基礎レベルにおいて有する変数の束縛と言う概念は，abstractionによって表されるもののみで，それはapplicationの逆に当たります．
　与えられた変数xとterm tに対して，x の像が t である関数を表すλx.tをlambda-abstractionと言い，HOL Lightでは `\x.t` と書きます．

# `\x.x+1`;;
val it : term = `\x. x + 1`
# type_of it;;
val it : hol_type = `:num->num`

これはOCamlでのfunと->で表される

# (fun x->x+1);;
val it : int -> int =
# (fun x->x+1) 5;;
val it : int = 6

と同種のものです．
　abstractionとapplicationとが逆の作用であることは，基礎的な推論規則BETAが |- (λx.t) x=t と告げることから判ります．

# BETA `(\x.x+1) x`;;
val it : thm = |- (\x. x + 1) x = x + 1
# BETA `(\x.x+1) y`;;
Exception: Failure "BETA: not a trivial beta-redex".

x以外の引数によるtheoremを得るには

# BETA`(\x.x+1)x`;;
val it : thm = |- (\x. x + 1) x = x + 1
# INST [`y:num`,`x:num`] it;;
val it : thm = |- (\x. x + 1) y = y + 1

とするか，７章で述べるBETA_CONVを用います．