値 - pogi-log

値

値(value)

文脈によって微妙な差がある？

操作的意味論では、項を評価した最終結果が正規形なものは値？

v ::= true | false

評価の最終結果が正規系のものは値である

式から値になる？

プロセスベース

code:mermaid

flowchart LR

ファイルI/O -->|文字| 字句解析

字句解析 -->|トークン| 構文解析

構文解析 -->|項| 評価

評価 -->|値| 表示

対象ベース

code:mermaid

flowchart LR

文字 -->|"字句解析(lex)"| トークン

トークン -->|"構文解析(parsing)"| 項

項 -->|"評価(eval)"| 値

値 -->|"表示(print)"| 文字

Martin-Löf型理論あたりではbが型A上の族Bの断面(section)であるとき、$ b(a) が値

code:memo

A := Nat

B(n) := Vector String n

b : Π(n : Nat), Vector String n

b(n) := 長さnのベクトル

b(3)が値

Lean 4で#evalすると型クラスが混じるのでちょっと説明が難しい

code:lean

import Init.Data.Vector.Basic

def B (n : Nat) := Vector String n

def b : (n : Nat) → Vector String n :=

fun n => Vector.replicate n ""

#check b 3 -- Vector String 3

#eval b 3 -- { toArray := #"", "", size_toArray := _ }

#eval (b 3).toList -- "", ""

確認用

Q. 値