<http://fumieval.hatenablog.com/entry/20...

http://fumieval.hatenablog.com/entry/2018/10/31/150056 最近の議論を受け、取り急ぎ「束縛」という言葉の使い方についての記事を執筆しました。なるべく正確を期したつもりですが、もし不適当な記述があればご教示ください

Replies

http://fumieval.hatenablog.com/entry/2018/10/31/150056 最近の議論を受け、取り急ぎ「束縛」という言葉の使い方についての記事を執筆しました。なるべく正確を期したつもりですが、もし不適当な記述があればご教示ください

ちなみに、 x = 42 のように Haskell で = を使った場合は何て読むのが正しいのでしょう?定義とかですかね?

(関数|変数)定義が一番無難だと思います。

なるほど 👍

読ませていただきました.うまく理解できないところがありましたのでコメントします.

>これは**あくまで変数とそれを導入する抽象の関係**であり、**変数と実体の関係ではない**ことだ。

「自由な」とか「束縛された」が修飾するのは構文上の**位置**なので,λ変数とそれを導入する抽象の関係を「束縛」といえることは確かだと思います.しかし,λ変数は後続の構文中での出現によって,どの位置がどの抽象で束縛されているか示すため方法の1つにすぎません.どの位置がどの抽象で束縛されているか示せれば,変数が存在しなくてもよいわけです.そうだとすると**変数と実体の関係ではない**というためにはさらに説明が必要な気がします.

>Haskellは、x = 42のような定義を与えることによって、変数で値を参照できる。だからといって「Haskellでは変数を値にバインドする」と言い切ってしまうことには大きな問題がある。理由は簡単で、変数に対して値以外もバインドできるからだ。例えばy = x + 1という宣言を考えてみよう。この宣言はyをバインドするが、その対象はx + 1という計算であり、式を評価した結果の値ではない。

>定義がインライン化(その名前が使われている場所に展開)されず、メモリ上に領域を確保すべきものと処理系が判断した場合、初めて値に関する議論が始まる――これが「代入」である。代入は、オブジェクトをヒープ(実行時に確保されるメモリ領域)上の場所にセットする。ここで言うオブジェクトは大きく分けて2種類ある。

私には,式42と式6 * 7とでは,一方は値で一方は計算であるという区別をする理由がよく判らないです.どちらの式も,「よんじゅうに」という同じ値を表わ(denote)すと考えたとき,どのような不都合がありますでしょうか?
一般にはHaskellで書かれたプログラムの意味は,数学的な関数モデルで考えるのが判りやすいと思われています.関数モデルは**構文**と**意味**で二元的に構成されている体系だとすると,**式**と**値**がその2つに相当すると考えてよいでしょう.そこに3つめの**計算**という元素を入れて,さらにメモリ,関数モデルではないモデルで説明する理由が示されていると判りやすいのかもしれません.

>この混乱は言語仕様ですらやらかしてしまっている。Haskell 2010 Language Reportの3.17.2 Informal Semantics of Pattern Matchingを見ると、"Binding does not imply evaluation"と注記しているにもかかわらず、本来オブジェクトに対するものであるパターンマッチを値に対するものと宣言してしまい、変数を値に束縛するという旨の表現を二箇所で使ってしまっている。学習者は言語仕様を読むだけでなく、case undefined + undefined of _ -> 42のような式を手元で評価し、実際の意味論を把握することを推奨する。

私としては「パターンマッチは値に対するものではなく,オブジェクトに対するものである」ことがうまく理解できません.「パターンマッチは値に対するもの」では,どのような不都合があるのでしょうか?
またcase undefined + undefined of _ -> 42はなにを説明する例なのでしょうか.

>以下のような主張はすべて**誤り**である.

定義が明示されていないので,すこし判りにく気がします.「定義によるんじゃないの」というひねくれものが出そう(相手にしなければいいだけかもしれないですが).

bindがどのような意味で使われているかに注意を払うべき,という主張は,肝に銘じます.

> **変数と実体の関係ではない**というためにはさらに説明が必要な気がします.

この部分はよく理解できませんでした。変数が存在しなくても良いというのは例えばde-Bruijn indexのようなものを指しているのでしょうか?また、どのような説明が必要だとお考えですか?

> さらにメモリ,関数モデルではないモデルで説明する理由が示されていると判りやすいのかもしれません.

「関数モデル」(私は使わない言葉ですが)は崩していません。「式」と「値」ではなく、「式」と「オブジェクト」がより正確であると主張しています。

> 「パターンマッチは値に対するもの」

今まで述べたことに沿って考えると、もし値に対するものとした場合、サンクのような値でないオブジェクトに対してパターンマッチできないことになります。すると、case undefined + undefined of _ -> 42の結果はundefinedになってしまいます(実際の処理系は42を返します)。

> 定義が明示されていないので

主張が正しくなってしまうような定義でないことは本文で示唆したつもりでしたが、どのあたりが不十分とお考えでしょうか?

はい,変数がないというのは de Bruijin インデックスを想定しました.
>...さらに説明が必要な気がします.
しかし,ここまでの部分は自分でもなにを言いたかったのかわかりません.撤回させてください.すみません.

>「式」と「オブジェクト」がより正確であると主張しています。

ここが要点だと思っていますが,動機というか「こころ」が良く理解できません.

サンクに対するパターンマッチするとは,どういう状況でしょう?サンクの値は⊥とみなせばよく,変数パターンはすべての値にマッチするので case undefined + undefined of _ -> 42 は42です.

>定義が明示されてないので,

これも完全に私の惚けでした.すみません.撤回させてください.誤った主張をしている側が誤った定義を使っているので,そもそも主張に意味がないことに気づいていませんでした.

雑なコメントで申し訳けありません.

蛇足かもしれませんがde-Bruijn indexはあくまで文字列の代わりに自然数を変数の表現に用いる仕組みで、変数が存在しないわけではありません(変数の存在しないコンビネータ論理の場合、当然束縛も存在しません)。
> ここが要点だと思っていますが,動機というか「こころ」が良く理解できません.
それが実際に使われているモデルだから、というのは十分な動機になると思います。
> サンクに対するパターンマッチするとは,どういう状況でしょう?サンクの値は⊥とみなせばよく,変数パターンはすべての値にマッチするので case undefined + undefined of _ -> 42 は42です.
サンクの値をボトムとみなしていいというのはまったく聞いたことがありません。代わりにcase 1+2+3+4+...100000 ofとかを考えてもらってもいいです。パターンマッチの話はコーナーケースといえばコーナーケースですが、Informalと前置きしているにせよ一貫性のない説明だったため、それを本文で指摘しました。

変数とは何か?も難しいですね.私は変数と構文上位置を指示する名前とを同一視して話していました.de Bruijnインデックスはその位置を束縛する抽象の位置を指示する指標ですから,変数とは別の機能なので,変数とは言わないかな.と思うしだいです.もちろん,どちらも,抽象とそれが束縛する位置を特定するために使うので目的は同じですね.

>それが実際に使われているモデルだから、というのは十分な動機になると思います。

Haskellのモデルで使われているのなら十分な動機だと思います.興味としては,単純な式と値のモデルではなく,そのモデルが採用されたモチベーションは何か,ということです.

> その位置を束縛する抽象の位置を指示する指標ですから,変数とは別の機能
これは同意しかねます…私ならそれこそが束縛変数の定義だと言います。

> そのモデルが採用されたモチベーションは何か
これはまさに遅延評価の動機、つまり「使わない計算は評価しない」「評価した結果である値を共有する」(https://wiki.haskell.org/Lazy_evaluation)であると言えると思います

評価しようとしまいと,1+2 が表示(denote)する値は「さん」と考えています.これは評価戦略にかかわらずです.

>それこそが束縛変数の定義だと言います。
はい,それは同意です.私の方が変数と変数名,あるいは変数と変数の出現を混同しています.

>サンクの値をボトムとみなしていいというのはまったく聞いたことがありません。
⊥値の導入の動機は,「Well-formedな式は例外なく値を表示(denote)する」と単純に考えるために特定の型の特定の値として定義されない⊥値があれば都合がよい,というものです.inf :: Integer; inf = inf + 1とあれば,infの表示(denote)する値は確定できない値⊥です.評価機計算中は表示(denote)する値は確定できないので,そのことを⊥とみなしても不都合はないように思います.

あんまり議論を追えてないのですが,値自体の定義を https://www.haskell.org/onlinereport/haskell2010/haskellch1.html#dx6-12001
> An expression evaluates to a value and has a static type.
に則って考えた場合,Haskellでは let x = 1 * 2 はxに(1 * 2を計算した)値を束縛しているのではなく,言うとしたら(call by name的には)1 * 2という式自体への束縛,または(call by need的には)1 * 2という計算自体への束縛というのが正しいと思います(なので記事の値への束縛というのが誤った使用法というのはHaskellでは誤りというのに同意です).なお,Haskellではcaseも(Formal Semanticsに則れば)まず対象の式を変数に束縛する変換がなされるので同じ議論を適用できると思います(これもつまり記事と同意見です):

また,一般的なdenotational semanticsは明るくないので分かりませんが,Haskellでは https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-230003.1@U4KU9ABL0 の用法はHaskellにおいてはあまり一般的ではないと思います.

それからここからは個人的な意見ですが,(取り急ぎと言うことなので続編があるのかもしれませんが)正しい言い方に対する言及がないのが色々疑問を招いているのではないかと感じました.

はい,let-束縛で変数を束縛するのは値ではなく,計算であるというのは理解できました.
「サンク」であることと「停止しない計算」とは区別できないように思いますがどうでしょう.

それと,let x = 1 のときx に束縛されるのは 1 という式で表される計算であって,値ではないと考えていいように思います.
>オブジェクトは大きく分けて2種類ある
計算の1種類だけでよいような気がしますがどうですか?

> 「サンク」であることと「停止しない計算」とは区別できないように思いますがどうでしょう.
Haskellの関数は基本的には値を取るため、オブジェクトがサンクかどうかを判定することはできません(GHCにはunpackClosure#のような例外あり)が、書き手が区別しないわけではないというのが重要だと思います。
> 計算の1種類だけでよいような気がしますがどうですか?
サンクは計算を指し示していますが、計算そのものとは別に扱うべきで、実際のモデルと乖離した定義をする(GHCなら17種類あるものを全部"計算"と呼ぶ)ことには賛成できません。

本文中では、「代入が」オブジェクトに関するものだとしており、この束縛と計算の議論とは直接関係ないので、あえてオブジェクトの定義に触れる必要はないと思います。

ああ.またやらかしました.すみません.変数にバインドできるものをオブジェクトと読んでしまってました.

評価完了していない値を_|_と書くのは、Wikipediaに載ってる不動点意味論の流儀なのかなあと思うのですが、確かにHaskellの一般的な用法とちょっと違う感じがしますね https://ja.wikipedia.org/wiki/%E8%A1%A8%E7%A4%BA%E7%9A%84%E6%84%8F%E5%91%B3%E8%AB%96

> 評価完了していない値を_|_と書くのは、Wikipediaに載ってる不動点意味論の流儀なのかなあと思うのですが
なるほど、これは僕の勉強不足でした 🙇

⊥の話は,R.Bird "Introduction to Functional Programming using Haskell" に少し出てきます.

>Haskellでは let x = 1 * 2 はxに(1 * 2を計算した)値を束縛しているのではなく,言うとしたら(call by name的には)1 * 2という式自体への束縛,または(call by need的には)1 * 2という計算自体への束縛というのが正しいと思います(なので記事の値への束縛というのが誤った使用法というのはHaskellでは誤りというのに同意です).

「変数の値へのバインド」ではcall-by-needを実現できないということでしょうか?変数と値の対(バインディング)のリストを環境として,式を環境下で解釈して値を得る意味関数ではcall-by-need流の意味論を構成できないということでしょうか?

議論が後退している気がします。値をバインドするとしてしまうと、評価していないものをバインドできない(したがってcall-by-needにならない)というのは本文でもこの議論でも触れたとおりです。

また、「λ変数」「意味関数」のような一般的に使われていない用語を定義せずに持ち込むのは、議論が困難になるので避けていただきたいです

>また、「λ変数」「意味関数」のような一般的に使われていない用語を定義せずに持ち込むのは、議論が困難になるので避けていただきたいです
すみません.「λ変数」は「束縛変数」,「意味関数」は「評価器」と読みかえてください.今後は,この用語は使いません.

>値をバインドするとしてしまうと、評価していものをバインドできない(したがってcall-by-needにならない)というのは本文でもこの議論でも触れたとおりです。
ここのところは「値をバインドするとしてしまうとcall-by-needになるような評価器を作成できない」と解釈してもいいですか?

はい、実装してみようとしてみるとできないことが比較的簡単にわかると思います

ありがとうございます.ちょっとやってみます.

Lazyな(おもちゃ)言語を作ってみました.
変数を値にバインドしたバインディングのリストで環境を構成しています.

Bindの定義を見るとわかる通り、これは変数名と「Valueの計算」の対(タプルは要素について非正格なため)になっていますね

「Value」と「Valueの計算」は別ものですか?

別物であるがゆえに、その評価器はcall-by-needを実現しています。

どうやって区別するのですか?

タプルはその要素が値である必要はなく、サンクも入れることができます。http://hackage.haskell.org/package/ghc-heap-view-0.5.10/docs/GHC-HeapView.html を使えばプログラムの中で判別することもできますよ。

書くのに全く区別を意識したわけではなです.

区別を意識して実装しなければ議論が成り立ちません。

区別する必要が全くなかったので意識しませんでした.私が議論が理解できなかったのはそこですね.なぜ区別するのかが判らないんです.

申し訳ないのですが、これ以上議論を進められる気がしないのでこれ以上のコメント(おそらく同じ説明を繰り返すことになるでしょう)は控えさせていただきます。

はい.ここからは,自分で考えてみたいとおもいます.長々とお付き合いいただきありがとうございます.

おそらく実装する言語を正格な言語(例えばRustやOCamlなど)にしてみるのがいいのではないでしょうか?

正格な言語を使えば意識せざるを得ないだろうことは想像できますが,非正格の言語を使うときにどう考えるのかという話であったように思います.それで,ふつうにHaskellで実装しました.Haskellを使っている限りにおいて意識しませんし,しなくてよいのではという思いが私の根底にあるようです.だからこそ,Haskellを使っているのに何故,意識しなければならないのかを理解したかったのです.

式が評価ずみであろうが評価中であろうが,式が表す値は値だという考え方に,何か不都合があるのならそれを知りたかったということです.アドバイスありがとうございます.

うーん、ではcall by valueを実装してみればよいのでは無いでしょうか?今回のはHaskellで意識しなくていいという話というより、たまたまHaskellでcall by needの実装だったからだと思います

Haskellから機械語へのコンパイラをHaskellで作れば絶対に理解できます。

>Haskellから機械語へのコンパイラをHaskellで作れば絶対に理解できます。
はい,是非挑戦してみたいです.

>call by valueを実装してみればよいのでは無いでしょうか?
これもちょっとやってみます.

call-by-valueを実装してみました.

本質的に変更したのは,関数適用式の評価に際して,関数部分の式を評価して得られる関数値を,引数部分の式を評価して得られる値に「正格に」適用しただけです.もう一箇所,Valueの関数ではない方は,裸のIntと同型になるようにbangを付けています.これはLazyの方も修正してあり,Valueの定義自身は両方で同じです.

通常call by valueでは,let x = e in e’ ~ (\x -> e’) eな気がするので,let bot = bot in botが無限ループしないのはあまりcall by valueと言えない気がします

あらら.

手元では無限ループしますが...doctestの記述を修正しわすれた.

あ,すいません.無限ループしますね.ちょっと勘違いでした.言いたかったのは次のパターンですね

eval $ Let [("bot",Div (Con 1) (Con 0))] (Con 0)

これがexceptionを吐かないのはおかしな気がします

あちゃーっ!!

修正.Valueの関数を正格関数として生成.interpの際はそのまま適用.

ようやく理解できたような気がします.
メモを公開してあります.(不備の指摘などいただけると嬉しいです) ありがとうございました.
https://scrapbox.io/ny-sketch-book/%E5%A4%89%E6%95%B0%E3%82%92%E6%9D%9F%E7%B8%9B%E3%81%99%E3%82%8B%E3%81%AE%E3%81%AF%E5%80%A4%E3%81%A7%E3%81%AF%E3%81%AA%E3%81%84%E3%81%AE%E3%81%8B

> 実際,[Lazyな(おもちゃ)言語 https://gist.github.com/nobsun/5b310dd4a397af624690b6ca4b0af2c8]も`interp`は意味関数(semantic function あるいは meaning function)という表示意味論で登場する意味を決める関数なわけで,操作意味論における簡約過程を書いたものではない.計算済みかどうかを意識して区別していない(できないし,必要もない)のはその所為である.

意味論については議論の途中で出てきたURLを踏んだりして勉強している所で、これは私見なのですが。denotativeに評価器を定義したいなら、ステップを陽に見えるように書かない限り、ちゃんとした定義にならないのではないかと思います。

現状だと⊥をdenoteする式に対してinterpを動かすと「プログラムが停止しない」という結果が得られる訳ですが、これはHaskellの持つ操作的意味論によって意味づけられているだけで、数学的にはinterpは部分関数で、⊥に相当する部分がill-definedなのではないかと思います。

Haskellにおいてステップを陽に書くなら、Iterモナドを用いると綺麗になりそう。 http://hackage.haskell.org/package/free-5.1/docs/Control-Monad-Trans-Iter.html#t:Iter

はい,ご指摘のとおりです.Div e1 e2 の意味がHaskellのdivに依存しているからです.

divというか、 let inf = inf + 1 in inf みたいなのの事を想定していました。こういうものの意味論をきちんと定義するために、Wikipediaの記事で言うところのprogressionを使った手法を導入したはずなので、表示的意味論でinterpを定義するなら考慮しないと駄目では、と思った次第 https://ja.wikipedia.org/wiki/%E8%A1%A8%E7%A4%BA%E7%9A%84%E6%84%8F%E5%91%B3%E8%AB%96

⊥を表示する式で停止するのは,Lazyおもちゃ言語では div ? 0 だけですが.

申し訳ない、「停止しない」でした(訂正済)

そうですねぇ.⊥から始まる近似列を実装しなければなりませんが,たとえば,inf = inf + 1 の場合,infの値はその近似列の極限になるわけで, +1 が値構成子 Succ :: Nat -> Nat で構成されていればなんとかなるかもしれませんが,その場合は,inf ≠ ⊥ですねぇ.実装上は単に停止しないということで表現する以外は思いつかなかったです.

単にsuccでいいのかな.

+ がプリミティブだとむずかしそう.

すいません,あれから少し不動点意味論の勉強をして,言いたかったことやHaskellの仕様が混乱していないという主張の意味がわかりました.

@U570660KX さんと同じ疑問は持ったのですが,個人的にはHaskellの意味関数を[],Toy言語の意味関数を[| |]とした時,[|e|] = [interp e]でHaskellの意味領域に接地させることで,意味関数と主張しているのだと思っていました.

primitiveの場合単に [e1 + e2] = { ⊥ if [e1] = ⊥ || [e2] = ⊥; [e1] + [e2] else }で定義すればいいのではないでしょうか?

あ,それで1つ前で言いたかったのは,例えばparallel ifなどを実装する際多分そのままの定義ではできなくて,それは何故できないかというと
> ⊥に相当する部分がill-defined

が効いてきてるのではないかなと思ったという感じです(あんまり説明になっていないかも)

停止が判定できないので,[e]=⊥が判定できないです.

> 例えばparallel ifなどを実装する際多分そのままの定義ではできなくて
parallel-orのことでしょうか?多分,⊥のように計算が停止しない値ではなく,値にバインドされていない変数が表示する値(emptyMVarの中身)みたいな計算をブロックするような値を考えないといけないですね.(たぶん)

asyncパッケージにあるControl.Concurrent.Async.raceみたいなもの実装のことですよね.

はい,C[pif L then M else N](env) = { [M](env) if [L](env) = true; [N](env) if [L](env) = false; [N](env) if [L](env) = ⊥ and [M](env) = [N](env); ⊥ else } みたいなやつですね.parallel orでも同じ議論ができますし,そっちの方が単純なのでそっちで考えてもらっても大丈夫です.

> 停止が判定できないので,[e] = ⊥が判定できないです.

これがよく分からないのですが,別に意味論上は停止するかどうかは判定しなくてよくて,その表示を満たせば良いと思うのですが,何か勘違いしてるでしょうか?実装上は, seq e1 . seq e2 $ e1 + e2 で問題ないはずです(Haskellの場合はそもそもe1 + e2でもいいですね)

また,自分の言っていることが混乱しているような気がしてきました.すみません.
>⊥に相当する部分がill-defined
がよく判っていない気がします(私が).どうなっていれば,well-definedですか?

ああ.プリミティブの場合はおっしゃるとおりですね.

要は,⊥となるtermへの扱いが明確に定められていなくて,Haskellの式が結果的に計算が停止しないので評価器も停止しないようになっているだけで,por のような⊥の扱いが重要になる場合にそれが問題になりそうというのが言いたいことでした.個人的には,
> Haskellの意味関数を[],Toy言語の意味関数を[| |]とした時,[|e|] = [interp e]でHaskellの意味領域に接地させることで,意味関数と主張している
ということでも問題ないとは思うのですが,denotativeと主張するならHaskellに接地させるのでなくtermに対する定義が明確になっていて,
> let inf = inf + 1 in inf みたいなの
@U570660KX さんがいうように評価器がちゃんとステップを陽に見えるよう書かれていれば,porはステップを同時進行させることで実装できるはずです)

プログラムのコードでいうと,ValueにBotが含まれているべきということになりますか?

それもありますが,主に
> progressionを使った手法を導入したはずなので、表示的意味論でinterpを定義するなら考慮しないと駄目では
ですね.多分ValueにBotを導入しただけではporは実装できないはずです(片方が停止しなくてももう片方が停止してtrueになれば結果が返せるので)

x por y = if isBot x then y else x は無理ですよね.

はい,その定義は二重にだめで,isBotがおそらく停止するように実装するのが無理なのと,⊥ por falseは通常⊥になるはずっていうのですね(なので,結構実装は難しいはずです)

>let inf = inf + 1 in infに対する定義がなされているべき
これがそもそもできそうもない(私の能力的に)

(まあ,本題からかなり外れる気がするのでどうなんですかね?個人的には,
> 実際,[Lazyな(おもちゃ)言語 https://gist.github.com/nobsun/5b310dd4a397af624690b6ca4b0af2c8]も`interp`は意味関数(semantic function あるいは meaning function)という表示意味論で登場する意味を決める関数なわけで,操作意味論における簡約過程を書いたものではない
という文が気になったというだけなので.後この議論で不動点意味論の気持ちが分かったので,感謝の気持ちしかないです)

意味が定められない = ⊥ ?

Iterモナドを使えば行ける...と思ったんですけど、意外に難しくてまだ組み途中です

interpをinterpFの不動点として定義してできたことにする.じゃだめかな? <- 適当にいってます.

https://gist.github.com/as-capabl/9dfb4cff6c08f6b5027741e2fc4bf40b por実装したやつできました

これは,call-by-name だけど,call-by-needじゃないようですが,そこは意図的ですか?

なるほど、そこは意識できてなかったです。おそらく改良すればcall-by-needも実装可能ですが、考える事が増えそうですね

単純にnormalizeがcall-by-need用になっていないだけです.

たまたま正格版のコードを元にして作り始めて、そうすると非正格評価に戻したときlet内でbotが呼び出しエラーになる事が分かって、結果的にほとんどnormalizeしていない形に修正しました。上の非正格版のnormを埋め込めば動くかどうか。

それはそれとして、このスレッドの本題としては「変数に束縛されるのはIter Valueだが、これを『値』とみなして良いのかどうか」かと

そうですね.Iter Value は値ではなく計算なので,「変数に束縛されるのは値ではなく,値を求める計算」ということになります.ただし,解釈器interp の最終結果すなわち,式が表示するものが,Iter Valueであるとするなら,Iter Valueを改めて値と読んでもよいと思います.

ちょっと強引かな.

Lazy版を修正してみました.Porの意味は勝手に替えてしまいましたが,動くようです.
https://gist.github.com/nobsun/5b310dd4a397af624690b6ca4b0af2c8

@U570660KX さんのだと

>>> eval $ Div (Con 1) (Con 0) `Por` Div (Con 1) (Con 1)
*** Exception: divide by zero

@U4KU9ABL0 の修正見るまで気づかなかった).本来のdenotational semanticsに立ち戻るならIter ValueはあくまでValueの近似であって,Iter Value ~ Valueとみなしても良いのではないでしょうか?まあただdenotationalにも近似を束縛する,計算を束縛するとも言えるかもしれないですね.

evalShow :: Int -> Expr -> String
というのを実装してみました.値の近似列を指定した段数まで,または,確定するまで表示します.

@U57D08Z9U それは1/0が無限ループになるようにDivの定義を変えて辻褄合わせるしかないですね…

個人的にはdenotation、つまり式が抽象的に持つ値をvalueと呼ぶ立場は実はけっこう好きなんですが、ただ一般的なプログラマの感覚とずれる部分は間違いなくあるっぽいんですよね…

@U570660KX 停止するボトムにコンストラクタを割り当てることでも可能じゃないですかね?

変更したLazy版は 1/0が無限ループに落るようになってます.:)

たとえば今回の場合、Iter Value'をvalueと呼んでしまうとcall-by-valueというタームが意味不明になってしまう

Porの定義は、何をfalseとするかの問題なので、あまり細かく考えてないです

call-by-hogehoge はあんまり使いたくないというのが正直なところ,
一般的な「imperative」プログラマの感覚とはずれるけど...
(私はもはやimperativeな感覚を失なっているようで,declarativeな表現の方がしっくりきます)

新しいPorの定義だと、 Por (Con 1) (Con 2)Por (Let (...) (Con 1)) (Con 2) が違う値になってしまうのが気持ち悪いかな…

この場合は Por の意味は先に計算が終った方という意味なので,ありかなと思います.

まあ,最適化とか考えるときに問題にはなると思いますが,あくまでToyなのでそこは突っ込みませんでした

もちろん,左のオペランドにすこしバイアスがありますが,

Por は非決定性をもちこむことになるので,決定性があることが前提の最適化とは最悪の相性でしょうねぇ.

@U570660KX さんの方も書けなそう.あと,porがstrictじゃない(⊥ por ⊥ /= ⊥)のも気になる感じですね).なので,今の定義だと幾つか嬉しい性質が壊れる気がします

eval (Por bot bot)が停止しないのと,evalShow 20 (Por bot bot) =>"⊥,⊥,⊥,⊥,⊥,⊥,⊥,⊥,⊥,⊥,⊥,⊥,⊥,⊥,⊥,⊥,⊥,⊥,⊥,⊥,..." なので多分 Por ⊥ ⊥ = ⊥になると思います.

あ,すいません勘違いでした. 想定してたのは Por (Div (Con 1) (Con 0)) (Div (Con 1) (Con 0)) みたいなやつなんですが,普通にこれは exception 吐くんですね.普通にstrictでした

あれっ.いまのは,例外をはかないと思います.

@U570660KX@U4KU9ABL0#C4M4TT8JJ|random にも投稿してしまったっっ)

@U570660KX さんの方で問題になりそうと思ったのは,

>>> eval $ Div (Con 1) (Con 0) `Por` Con 1
1
>>> eval $ Div (Con 1) (Con 0) `Por` Div (Con 1) (Con 1)
*** Exception: divide by zero

ですね

それも1/0が無限ループするようにすれば整合性がつきますが、それはそれとしてporの意味論とかはもう少し勉強してきます

私が勝手に意味を変えたPorは参照透明性を破壊します.

というわけでまともなものではないです.