外延性 - mrsekut-p

外延性

2つのラムダ抽象の同値関係の定義

2つの型付きラムダ式$ M, M': A\to Bについて、任意の$ N:Aについて$ M(N)=_{\beta\eta}M'(N)が成り立つならば$ M=_{\beta\eta}M'が成り立つという性質

関数$ f,gについて

$ \forall x, f(x)=g(x)\Rightarrow f=gがなりたつこと

「外延性」という言葉がわかりにくすぎるなmrsekut.icon

内容自体はシンプルなのに無駄に難しそうに見える

参考