import FormalLab.TypeTheory.StructuralRules

/-!
# 第13章：操作的意味論・一段簡約・評価戦略

同じβ規則を持つラムダ計算でも、関数本体へ引数を渡す前にその引数を評価するかどうかで、計算の
途中経過と停止性は変わります。「簡約できる」という関係と、「次にこの簡約を選ぶ」という戦略を
分けなければ、言語の実行規則を一意に読めません。

本章では値呼びの小ステップ操作的意味論を定義します。まず一段の関係を推論規則として与え、同じ規則を
実行する `step?` を構成します。値、正規形、停止、発散を区別し、名前呼びとの対照から評価戦略が
選択するredexの位置を確かめます。

## 値呼びは引数を値にしてからβ簡約する

項 `λx.t` を値とします。値呼びの一段簡約 `t →ᵥ t'` は、次の三規則で評価位置を左から右へ選びます。

$$
\frac{t_1\to_v t_1'}{t_1\,t_2\to_v t_1'\,t_2}\;(\xi_1)
\qquad
\frac{t_2\to_v t_2'\qquad v_1\;\mathsf{value}}
     {v_1\,t_2\to_v v_1\,t_2'}\;(\xi_2)
$$

$$
\frac{v_2\;\mathsf{value}}
     {(\lambda x.t)\,v_2\to_v t[x:=v_2]}\;(\beta_v).
$$

左の項がまだ値でなければ左を進め、左が値になってから右を進めます。両方が値になった適用だけが
β規則を使います。この順序制約により、一つの項から異なる評価位置を同時に選びません。
-/

namespace FormalLab.TypeTheory.OperationalSemantics

open FormalLab.Foundation.UntypedLambdaCalculus

inductive Value : Term → Prop where
  | lam : Value (.lam body)

inductive Step : Term → Term → Prop where
  | beta : Value argument →
      Step (.app (.lam body) argument) (substitute 0 argument body)
  | appLeft : Step function function' →
      Step (.app function argument) (.app function' argument)
  | appRight : Value function → Step argument argument' →
      Step (.app function argument) (.app function argument')

example : Step (.app identity constant) constant :=
  .beta .lam

example : Step (.app (.app identity identity) constant) (.app identity constant) :=
  .appLeft (.beta .lam)

theorem valueCannotStep {value next : Term} (isValue : Value value) : ¬Step value next := by
  cases isValue
  intro step
  cases step

/-!
`valueCannotStep` は「値なら評価しない」という戦略上の事実です。値がβ正規形であることとは向きが
異なります。純粋ラムダ計算ではラムダ本体の内側にredexが残り得ますが、弱頭値を得た時点で本章の
値呼び評価はラムダの内側へ進みません。どこにもβ-redexがない正規形と、現在の戦略が停止する値を
同一視しないでください。

## 推論関係を一段実行する

`Step` は一段計算が許されることの証拠です。次の関数は同じ左から右の規則を実行し、次の項があれば
`some`、なければ `none` を返します。`isValue` は本章の値構文を判定可能な真偽値へ写します。
-/

def isValue : Term → Bool
  | .lam _ => true
  | _ => false

def step? : Term → Option Term
  | .var _ => none
  | .lam _ => none
  | .app function argument =>
      match function with
      | .lam body =>
          if isValue argument then
            some (substitute 0 argument body)
          else
            match step? argument with
            | some argument' => some (.app function argument')
            | none => none
      | _ =>
          match step? function with
          | some function' => some (.app function' argument)
          | none => none

example : step? (.app identity constant) = some constant := rfl
example : step? identity = none := rfl

theorem valueStepNone {term : Term} (value : Value term) : step? term = none := by
  cases value
  rfl

/-- Boolean値判定が成功した項から、関係としての値の証拠を回収します。 -/
theorem valueOfIsValue {term : Term} (result : isValue term = true) : Value term := by
  cases term with
  | var index => simp [isValue] at result
  | app function argument => simp [isValue] at result
  | lam body => exact .lam

/-- 実行関数が返すすべての一歩は、推論関係 `Step` が許す一歩です。 -/
theorem step?_sound {term next : Term} (result : step? term = some next) : Step term next := by
  induction term generalizing next with
  | var index => simp [step?] at result
  | lam body => simp [step?] at result
  | app function argument functionIH argumentIH =>
      cases function with
      | var index => simp [step?] at result
      | app left right =>
          cases reduced : step? (.app left right) with
          | none =>
              change (match step? (.app left right) with
                | some function' => some (.app function' argument)
                | none => none) = some next at result
              rw [reduced] at result
              contradiction
          | some function' =>
              change (match step? (.app left right) with
                | some function' => some (.app function' argument)
                | none => none) = some next at result
              rw [reduced] at result
              cases result
              exact .appLeft (functionIH reduced)
      | lam body =>
          simp only [step?] at result
          by_cases argumentValue : isValue argument = true
          · simp [argumentValue] at result
            subst next
            exact .beta (valueOfIsValue argumentValue)
          · have argumentValueFalse : isValue argument = false := by
              cases value : isValue argument <;> simp_all
            cases reduced : step? argument with
            | none => simp [argumentValueFalse, reduced] at result
            | some argument' =>
                simp [argumentValueFalse, reduced] at result
                subst next
                exact .appRight .lam (argumentIH reduced)

/-!
関係と関数には役割の差があります。`Step t u` は導出に対する帰納法や、複数の意味論の比較に向きます。
`step? t` は具体的な次状態を計算できます。両者が同じ一段を表すには、関数が返した結果から `Step` を
構成する健全性と、`Step` があるなら関数もその結果を返す完全性が必要です。具体例が一致するだけで
一般の対応定理を証明したことにはなりません。

`step?_sound` はこのうち健全性を全項について証明します。完全性と決定性は章末問題として残します。
したがって本文の実装済み結果から「関係と関数が同値である」とはまだ結論せず、片方向の証拠だけを
正確に利用します。

## 一段、有限回、無限回を分ける

反射推移閉包 `Steps t u` は、零回以上の有限回の簡約を表します。`refl` は零回、`tail` は既知の
有限簡約の末尾へ一段を加えます。到達可能性を定義しても、全ての項が値へ到達するとは限りません。
-/

inductive Steps : Term → Term → Prop where
  | refl : Steps term term
  | tail : Steps first middle → Step middle last → Steps first last

def omegaBody : Term :=
  .lam (.app (.var 0) (.var 0))

def omega : Term :=
  .app omegaBody omegaBody

theorem omegaOneStep : Step omega omega := by
  exact .beta .lam

example : step? omega = some omega := rfl

/-!
`omega` は一段進んでも同じ項へ戻ります。任意の有限回だけ `Steps omega omega` を作れますが、値へ
近づく測度は減りません。停止性は「次状態がある」ことではなく、無限に一段簡約を続けられないことです。
後の正規化章では、弱正規化、強正規化、評価器の停止を別々に定義します。

## 名前呼びでは未評価の引数を代入する

名前呼びの弱頭簡約は、引数が値かどうかを問わず最外のβ-redexを縮約します。関数位置だけを先に進め、
引数位置を独立には評価しません。
-/

inductive NameStep : Term → Term → Prop where
  | beta : NameStep (.app (.lam body) argument) (substitute 0 argument body)
  | appLeft : NameStep function function' →
      NameStep (.app function argument) (.app function' argument)

example : NameStep (.app identity omega) omega :=
  .beta

/-!
恒等関数ではどちらの戦略も最終的に `omega` を評価するため発散します。定数関数が引数を捨てる場合、
名前呼びは未評価の引数を本体へ代入して捨てられますが、値呼びは先に引数を値へしようとして止まりません。
これはβ規則の正しさの差ではなく、どのredexを選ぶかという戦略の差です。

## 要点

* 小ステップ意味論は、一段の状態変化を推論関係として定める。
* 値呼びは関数、引数の順に値を求め、値になった引数だけをβ簡約する。
* 値、β正規形、現在の戦略で次状態がない項は一般には異なる。
* 反射推移閉包は有限回の到達可能性であり、停止や正規化を自動的には保証しない。
* 名前呼びと値呼びは同じ項で停止挙動が異なり得る。

## 研究史と文献案内

Plotkinの1975年論文 [PLO75] は名前呼びと値呼びのラムダ計算を、プログラミング言語との対応を含めて
比較する基準文献です。本章の `Step` 構成子や `Option` 値の実行関数を同論文の記法そのものとは
みなしません。小ステップ意味論、評価文脈、決定性の標準的な展開は [TAPL02]、対象言語とメタ言語を
分離した意味論の設計は [PFPL16] を参照してください。

## 問題

### 一つの評価列を二つの表現で追う

三つ以上の適用を持つ閉項を作り、値呼びの各一段を推論木と `step?` の計算結果で並べてください。
各段階で `appLeft`、`appRight`、`beta` のどれを使い、他の二規則をなぜ使えないか説明します。
最後の項が値、β正規形、単なる行き詰まりのどれであるかを三定義から判定すれば完了です。

### 名前呼びと値呼びの停止挙動を分離する

第一引数を返す定数関数へ値と `omega` を異なる順で適用し、二戦略の簡約列を書いてください。
名前呼びだけが弱頭値へ到達する配置を特定し、使われない引数がいつ捨てられるかを示します。
「名前呼びは常に停止する」という誤った一般化に対して、恒等関数と `omega` から反例も与えます。
二つの結果を、値へ到達するか、有限列の長さ、評価されない部分項という三列の表にすれば完了です。

### 関係と実行関数の対応を証明する

`step? t = some u → Step t u` を項 `t` の構造帰納法で証明してください。各match分岐を三つの
`Step` 構成子へ対応づけ、関数位置がラムダのとき `appLeft` を選ばない理由を `valueCannotStep` から
説明します。逆向きも証明し、二方向から値呼び一段簡約の決定性を導けば完了です。
-/

end FormalLab.TypeTheory.OperationalSemantics