6
  1. 関数構成の例を挙げられる人はいますか?

  2. これが関数合成演算子の定義？

    (.) :: (b -> c) -> (a -> b) -> a -> c
f . g = \x -> f (g x)

これは、2つの関数を取り、関数を返すことを示していますが、誰かがロジックを英語で次のように表現したことを覚えています

男の子は人間 -> アリは男の子 -> アリは人間

  1. 関数合成に関連するこのロジックは何ですか?
  2. 関数適用と合成の強い結合の意味と、どちらがより強い結合か?

助けてください。

ありがとう。

4

1 に答える 1

20

(編集 1:最初に質問のいくつかのコンポーネントを見逃しました。私の回答の下部を参照してください。)

この種のステートメントについて考える方法は、型を見ることです。あなたが持っている議論の形式は三段論法と呼ばれます。しかし、私はあなたが何かを間違って覚えていると思います。さまざまな種類の三段論法があり、あなたの三段論法は、私が知る限り、機能構成に対応していません。次のような三段論法を考えてみましょう。

  1. 晴れたら暑くなる。
  2. 暑くなったら泳ぎに行きます。
  3. だから、晴れたら泳ぎに行きます。

これを仮説三段論法といいます。論理的には次のように書けます。Sは「晴れている」という命題、 Hは「暑くなります」という命題、 Wは「泳ぎに行きます」という命題です。 . 「 αはβを意味する」をα → βと書き、「したがって」を∴と書くと、上記は次のように翻訳できます。

  1. 小→高
  2. 上→西
  3. ∴南→西

もちろん、これは、S、H、およびWを任意のα、β、およびγに置き換えれば機能します。さて、これはおなじみのはずです。含意矢印 → を関数矢印 に変える->とこうなる

  1. a -> b
  2. b -> c
  3. ∴a -> c

そして、見よ、合成演算子の型の 3 つのコンポーネントがあります! これを論理的な三段論法として考えるには、次のように考えることができます。

  1. type の値がある場合、 typeaの値を生成できますb。
  2. type の値がある場合、 typebの値を生成できますc。
  3. したがって、 type の値がある場合、 typeaの値を生成できますc。

これは理にかなっています。ではf . g、関数の存在は、g :: a -> b前提 1 が真でf :: b -> cあることを示し、前提 2 が真であることを示します。したがって、関数f . g :: a -> cが証人である最終ステートメントを結論付けることができます。

あなたの三段論法が何を意味するのか完全にはわかりません。それはほとんどmodus ponensのインスタンスですが、完全ではありません。Modus ponens 引数は次の形式を取ります。

  1. もし雨が降っていたら、私はびしょぬれになります。
  2. 雨が降っている。
  3. だから濡れちゃう。

「雨が降っている」をR 、「濡れます」をWと書くと、論理形式が得られます。

  1. 右→西
  2. R
  3. ∴ワ

含意矢印を関数矢印に置き換えると、次のようになります。

  1. a -> b
  2. a
  3. ∴b

の型からわかるように、これは単なる関数適用です($) :: (a -> b) -> a -> b。これを論理的な議論として考えたい場合は、次の形式になる可能性があります。

  1. type の値がある場合、 typeaの値を生成できますb。
  2. type の値がありますa。
  3. したがって、 type の値を生成できますb。

ここで、式を考えますf x。関数f :: a -> bは、命題 1 の真偽の証人です。値x :: aは、命題 2 の真偽の証人です。したがって、結果は型bである可能性があり、結論を証明します。まさに証明からわかったことです。

これで、元の三段論法は次の形式になります。

  1. すべての男の子は人間です。
  2. アリは男の子です。
  3. したがって、アリは人間です。

これを記号に置き換えてみましょう。 Bxはxが男の子であることを示します。Hxはxが人間であることを示します。aはアリを意味します。と ∀ x . φは、φがxのすべての値に対して真であることを示しています。次に、

  1. ∀ ×。Bx → Hx
  2. バ
  3. ∴は

これはほとんど手口ですが、forall をインスタンス化する必要があります。論理的には有効ですが、型システム レベルで解釈する方法がわかりません。誰かが助けたいなら、私はすべて耳を傾けます。1 つの推測では、 のようなランク 2 のタイプになりますが(forall x. B x -> H x) -> B a -> H a、それが間違っていることはほぼ確実です。もう 1 つの推測は、 のような単純な型(B x -> H x) -> B Int -> H Intで、ここIntで Ali は Ali を表しますが、これも間違いであると確信しています。繰り返しますが、ご存知でしたら私にも教えてください！

そして、最後に 1 つ注意してください。このように物事を見て、証明とプログラムの関係をたどると、最終的にカリー・ハワード同型写像の深い魔法にたどり着きますが、それはより高度なトピックです。（でも、めっちゃかっこいい！）

編集1:関数構成の例も求めました。これが一例です。人々のミドルネームのリストがあるとします。すべてのミドル ネームのリストを作成する必要がありますが、そのためにはまず存在しないミドル ネームをすべて除外する必要があります。ミドル ネームが null であるすべての人を除外するのは簡単です。ミドルネームがnull でないすべての人を含めるだけです。同様に、誰かのミドルネームのイニシャルを で簡単に取得できるため、リストを取得するために必要なことは単純です。つまり、次のコードがあります。filter (\mn -> not $ null mn) middleNamesheadmap head filteredMiddleNames

allMiddleInitials :: [Char]
allMiddleInitials = map head $ filter (\mn -> not $ null mn) middleNames

しかし、これはイライラするほど具体的です。中頭文字生成関数が本当に必要です。それでは、これを次のように変更しましょう。

getMiddleInitials :: [String] -> [Char]
getMiddleInitials middleNames = map head $ filter (\mn -> not $ null mn) middleNames

では、興味深いものを見てみましょう。関数mapには type(a -> b) -> [a] -> [b]があり、headtype があるため[a] -> a、map headtype があり[[a]] -> [a]ます。同様に、filterは type(a -> Bool) -> [a] -> [a]を持ち、 type もfilter (\mn -> not $ null mn)持ち[a] -> [a]ます。したがって、パラメーターを削除して、代わりに次のように記述できます。

-- The type is also more general
getFirstElements :: [[a]] -> [a]
getFirstElements = map head . filter (not . null)

そして、composition のボーナス インスタンスがあることがわかります: nothas type Bool -> Bool、nullhas type [a] -> Bool、つまりnot . nullhas type [a] -> Bool: 最初に指定されたリストが空かどうかをチェックし、次に空でないかどうかを返します。ちなみに、この変換により、関数はポイントフリー スタイルに変更されました。つまり、結果の関数には明示的な変数がありません。

あなたは「強い結合」についても尋ねました。あなたが言及していると思うのは、.and$演算子の優先順位です (おそらく関数適用も)。Haskell では、算術演算と同様に、特定の演算子が他の演算子よりも優先順位が高いため、より緊密にバインドされます。たとえば、式1 + 2 * 3では、これは として解析され1 + (2 * 3)ます。これは、Haskell では次の宣言が有効であるためです。

infixl 6 +
infixl 7 *

数値 (優先レベル) が高いほど、そのオペレーターが呼び出されるのが早くなるため、オペレーターはより緊密にバインドされます。関数適用は効果的に無限の優先順位を持つため、最も緊密にバインドされます。式はあらゆる operatorと同様にf x % g y解析されます。( composition) および(application) 演算子には、次の固定宣言があります。(f x) % (g y)%.$

infixr 9 .
infixr 0 $

優先レベルの範囲は 0 から 9 であり、これが意味することは、オペレーターが他のどのオペレーターより.も強くバインドされ (関数アプリケーションを除く)、バインドがそれほど強くないということです。したがって、式は次のように解析されます。実際、ほとんどの演算子はと になります。(唯一の例外は、他の少数のゼロまたは 9 優先順位の演算子です。)$f . g $ h(f . g) $ hf . g % h(f . g) % hf % g $ hf % (g $ h)

于 2010-06-25T09:05:53.077 に答える