無型むがたλ計算けいさんの基本きほん

date2026-07-14document_iddoc_229c9f53411adeb4170ec31e1d63f8badescription無型λ計算の構文、自由変数、捕獲回避置換、α同値、β簡約、正規形、評価戦略の相違を説明する講義である。prerequisitesdata/lecture/information/programming-languages/foundation/substitution-and-alpha-equivalence-basics.lecture.n.md / data/lecture/information/programming-languages/foundation/variable-binding-and-free-variables-basics.lecture.n.md / data/lecture/information/programming-languages/foundation/introduction-to-functional-programming.lecture.n.mdtype講義statusactive

informationprogramming-languageslambda-calculuslecture

1導入どうにゅう

この講義こうぎでは、無型むがたλ計算けいさんの構文こうぶんとβ簡約かんやくを説明せつめいする。置換ちかんによる変数捕獲へんすうほかくを回避かいひするため、自由変数じゆうへんすうとα同値どうちをβ簡約かんやくより先さきに確認かくにんする。ここでは型判断かたはんだんを導入どうにゅうしない。

21. 構文こうぶんと結合規則けつごうきそく

変数へんすうの集合しゅうごうを可算無限集合かさんむげんしゅうごうとする。λ項こう $t$ は次つぎの文法ぶんぽうで帰納的きのうてきに定義ていぎする。

t : := x ∣ λ x . t ∣ t t

$λ x . t$ は $x$ を束縛そくばくするλ抽象ちゅうしょう、 $t s$ は適用てきようである。適用てきようは左結合ひだりけつごうであり、λ抽象ちゅうしょうの本体ほんたいは可能かのうな限かぎり右みぎへ延長えんちょうする。したがって、 $t u v = (t u) v$ 、 $λ x . t u = λ x . (t u)$ である。

32. 自由変数じゆうへんすうとα同値どうち

自由変数集合じゆうへんすうしゅうごう $F V (t)$ を次つぎで定義ていぎする。

F V (x) = {x}, F V (λ x . t) = F V (t) ∖ {x}, F V (t u) = F V (t) \cup F V (u) .

束縛変数そくばくへんすうの一貫いっかんした改名かいめいだけが異ことなる項こうをα同値どうちとする。たとえば、 $λ x . x =_{α} λ z . z$ である。ただし、 $z$ が本体ほんたいで自由じゆうに出現しゅつげんする場合ばあい、 $x$ を $z$ に改名かいめいできない。

43. 捕獲回避置換ほかくかいひちかん

$t [x := s]$ は、 $t$ における $x$ の自由出現じゆうしゅつげんを $s$ で置換ちかんする項こうである。 $x \notin F V (t)$ なら $t [x := s] = t$ とする。変数へんすうと適用てきようでは構造こうぞうに沿そって定義ていぎし、λ抽象ちゅうしょうでは次つぎの条件じょうけんを用もちいる。

(\lambda y.t)[x:=s]= \begin{cases} \lambda y.t & y=x,\\ \lambda y.(t[x:=s]) & y\ne x\ \text{かつ}\ y\notin\mathrm{FV}(s),\\ \lambda z.((t[y:=z])[x:=s]) & y\ne x\ \text{かつ}\ y\in\mathrm{FV}(s), \end{cases}(\lambda y.t)[x:=s]= \begin{cases} \lambda y.t & y=x,\\ \lambda y.(t[x:=s]) & y\ne x\ \text{かつ}\ y\notin\mathrm{FV}(s),\\ \lambda z.((t[y:=z])[x:=s]) & y\ne x\ \text{かつ}\ y\in\mathrm{FV}(s), \end{cases}

最後さいごの場合ばあいでは、 $t$ と $s$ のどこにも出現しゅつげんせず、 $x$ とも異ことなる新あたらしい変数へんすう（fresh variable） $z$ を選択せんたくする。たとえば、 $(λ y . x) [x := y]$ をそのまま $λ y . y$ とすると、置換項ちかんこうの自由変数じゆうへんすう $y$ が捕獲ほかくされる。先さきにα改名かいめいして、 $(λ y . x) [x := y] =_{α} (λ z . x) [x := y] = λ z . y$ とする。

54. β簡約かんやくと正規形せいきけい

$(λ x . t) s$ という部分項ぶぶんこうをβ簡約基かんやくきといい、捕獲回避置換ほかくかいひちかんによって次つぎのように簡約かんやくする。

(λ x . t) s \to_{β} t [x := s] .

項こうの任意にんいの位置いちにあるβ簡約基かんやくきを一段いちだん簡約かんやくできる。β簡約基かんやくきを含ふくまない項こうをβ正規形せいきけいという。

(λ x . λ y . x) a b \to_{β} (λ y . a) b \to_{β} a .

一方いっぽう、 $Ω = (λ x . x x) (λ x . x x)$ のβ簡約基かんやくきは項全体こうぜんたいだけであり、その簡約かんやくは $Ω \to_{β} Ω$ に戻もどる。したがって、どの簡約列かんやくれつもβ正規形せいきけいへ到達とうたつしない。無型むがたλ計算けいさんでは停止性ていしせいを一般いっぱんに保証ほしょうできない。

65. 評価戦略ひょうかせんりゃく

β簡約かんやくは簡約基かんやくきの選択順せんたくじゅんを規定きていしない。最左外側さいさひだりそとがわの簡約基かんやくきを選択せんたくする正規順序せいきじゅんじょと、最左内側さいさひだりうちがわの簡約基かんやくきを選択せんたくする適用順序てきようじゅんじょでは、停止挙動ていしきょどうが異ことなりうる。

(λ x . a) Ω

正規順序せいきじゅんじょでは外側そとがわを先さきに簡約かんやくして $a$ に到達とうたつする。適用順序てきようじゅんじょでは $Ω$ の簡約かんやくを反復はんぷくするため停止ていししない。これは戦略せんりゃくの停止性ていしせいの差さであり、β簡約規則かんやくきそくそのものの差さではない。β正規形せいきけいが存在そんざいする項こうについて、正規順序せいきじゅんじょはそれに到達とうたつする。

76. η変換へんかんとの区別くべつ

$x \notin F V (f)$ のとき、 $λ x . f x =_{η} f$ とするη変換へんかんは、関数かんすうの外延的がいえんてきな同一視どういつしを表あらわす。これは関数適用かんすうてきようを実行じっこうするβ簡約かんやくとは別べつの規則きそくである。

8まとめ

無型むがたλ計算けいさんの計算けいさんは、α同値どうちを考慮こうりょした捕獲回避置換ほかくかいひちかんによるβ簡約かんやくである。正規形せいきけいの存在そんざいと、特定とくていの評価戦略ひょうかせんりゃくが停止ていしすることは区別くべつする必要ひつようがある。

data/lecture/information/programming-languages/foundation/substitution-and-alpha-equivalence-basics.lecture.n.md

Basics of the Untyped Lambda Calculus

1Introduction

This lecture explains the syntax and beta-reduction of the untyped lambda calculus. It reviews free variables and alpha-equivalence before beta-reduction because substitution must avoid variable capture. No typing judgment is introduced here.

21. Syntax and association conventions

Let the set of variables be countably infinite. Lambda terms $t$ are defined inductively by

t : := x ∣ λ x . t ∣ t t .

The term $λ x . t$ is a lambda abstraction that binds $x$ , and $t s$ is an application. Application associates to the left, and the body of an abstraction extends as far right as possible. Thus $t u v = (t u) v$ and $λ x . t u = λ x . (t u)$ .

32. Free variables and alpha-equivalence

The set $F V (t)$ of free variables is defined by

F V (x) = {x}, F V (λ x . t) = F V (t) ∖ {x}, F V (t u) = F V (t) \cup F V (u) .

Terms that differ only by a consistent renaming of bound variables are alpha-equivalent. For example, $λ x . x =_{α} λ z . z$ . A binder cannot, however, be renamed to $z$ when $z$ occurs free in its body.

43. Capture-avoiding substitution

The term $t [x := s]$ replaces every free occurrence of $x$ in $t$ with $s$ . If $x \notin F V (t)$ , then $t [x := s] = t$ . Its variable and application cases follow the term structure. The abstraction case is

(\lambda y.t)[x:=s]= \begin{cases} \lambda y.t & y=x,\\ \lambda y.(t[x:=s]) & y\ne x\ \text{and}\ y\notin\mathrm{FV}(s),\\ \lambda z.((t[y:=z])[x:=s]) & y\ne x\ \text{and}\ y\in\mathrm{FV}(s), \end{cases}(\lambda y.t)[x:=s]= \begin{cases} \lambda y.t & y=x,\\ \lambda y.(t[x:=s]) & y\ne x\ \text{and}\ y\notin\mathrm{FV}(s),\\ \lambda z.((t[y:=z])[x:=s]) & y\ne x\ \text{and}\ y\in\mathrm{FV}(s), \end{cases}

where the last case chooses a fresh variable $z$ that differs from $x$ and does not occur anywhere in either $t$ or $s$ . For example, directly producing $λ y . y$ from $(λ y . x) [x := y]$ would capture the free $y$ of the substituted term. Alpha-renaming first gives $(λ y . x) [x := y] =_{α} (λ z . x) [x := y] = λ z . y$ .

54. Beta-reduction and normal forms

A subterm of the form $(λ x . t) s$ is a beta-redex. Capture-avoiding substitution contracts it as follows:

(λ x . t) s \to_{β} t [x := s] .

A beta-redex at any position in a term may be contracted in one step. A term containing no beta-redex is a beta-normal form.

(λ x . λ y . x) a b \to_{β} (λ y . a) b \to_{β} a .

In contrast, the only beta-redex of $Ω = (λ x . x x) (λ x . x x)$ is the whole term, and contracting it returns $Ω \to_{β} Ω$ . Hence no reduction sequence reaches a beta-normal form. The untyped lambda calculus does not guarantee termination in general.

65. Evaluation strategies

Beta-reduction does not prescribe an order for selecting redexes. Normal order selects the leftmost outermost redex, whereas applicative order selects the leftmost innermost redex; the two strategies can have different termination behavior. Consider

(λ x . a) Ω .

Normal order contracts the outer redex first and reaches $a$ . Applicative order repeatedly reduces $Ω$ and does not terminate. This is a difference in strategy termination, not a difference in the beta-reduction rule. If a term has a beta-normal form, normal-order reduction reaches it.

76. Distinguishing eta-conversion

When $x \notin F V (f)$ , the eta-conversion $λ x . f x =_{η} f$ expresses extensional identification of functions. It is distinct from beta-reduction, which performs function application.

8Summary

Computation in the untyped lambda calculus is beta-reduction by capture-avoiding substitution, considered modulo alpha-equivalence. The existence of a normal form must be distinguished from termination under a particular evaluation strategy.

data/lecture/information/programming-languages/foundation/substitution-and-alpha-equivalence-basics.lecture.n.md