以下の内容はhttps://m-hiyama-memo.hatenablog.com/entry/2021/01/09/150952より取得しました。

無名の自由変数

論理 本編ネタ
  1. \lambda\, x:A.( G(F(x, y), w) ) \;::\; y:B,\; w:D \Rightarrow A \to C
  2. y:B,\; w:D \Rightarrow \lambda\, x:A.( G(F(x, y), w) ) \,:A \to C
  3. y:B,\; w:D \vdash \lambda\, x:A.( G(F(x, y), w) ) \,:A \to C

自由変数を番号にすると：

  1. \lambda\, x:A.( G(F(x, $1), $2) ) \;::\; B,\; D \Rightarrow A \to C
  2. B,\; D \Rightarrow \lambda\, x:A.( G(F(x, $1), $2) ) \,:A \to C
  3. B,\; D \vdash \lambda\, x:A.( G(F(x, $1), $2) ) \,:A \to C

束縛変数も番号にしても構わない。



以上の内容はhttps://m-hiyama-memo.hatenablog.com/entry/2021/01/09/150952より取得しました。
このページはhttp://font.textar.tv/のウェブフォントを使用してます
不具合報告/要望等はこちらへお願いします。
モバイルやる夫Viewer Ver0.14