タグ

smullyanに関するkazutanakaのブックマーク (7)

  • Combinator Birds

  • To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction

    To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction David C Keenan, 27-Aug-1996 last updated 1-Apr-2014 116 Bowman Parade, Bardon QLD 4065, Australia http://dkeenan.com Abstract The lambda calculus, and the closely related theory of combinators, are important in the foundations of mathematics, logic and computer science. This paper provides an informal an

  • To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction

    To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction David C Keenan, 27-Aug-1996 last updated 1-Apr-2014 116 Bowman Parade, Bardon QLD 4065, Australia http://dkeenan.com Abstract The lambda calculus, and the closely related theory of combinators, are important in the foundations of mathematics, logic and computer science. This paper provides an informal an

  • 史上最も難しい論理パズル - しのごの録

    「史上最も難しい論理パズル」(The Hardest Logic Puzzle Ever)と名づけられたパズル*1がおもしろかったので、紹介します。 3人の神様A、B、Cがいる。彼らにはシン、ギ、ランという名前があるが、A、B、Cの誰がどの名前を持つかをあなたは知らない。(ただし神様同士はお互いの名前を知っている。)シンは常に正しいことを話し、ギは常に嘘を話すが、ランが正しいことを話すか嘘を話すかは完全にランダムである。あなたに課せられた課題は、YES/NOクエスチョン(YESかNOで答えられる質問)を3回することによって、A、B、Cの正体を特定することである。ただし各質問は、ただ1人の神様に向けて行うものとする。神様は人間の言葉を理解するが、回答は彼ら独自の言語で行われる。その言語では「YES」と「NO」に相当する言葉は「ダ」と「ジャ」だが、どっちがどっちを意味するのかをあなたは知らない

    史上最も難しい論理パズル - しのごの録
  • 鳥たちと戯れる - Life Goes On

    To Mock a Mockingbird を読んでいます。言わずと知れたコンビネータ論理の教科書(?)です。 そこで算術や論理を関数で表すという、ラムダ計算でよくある話が登場するのですが、自然数の定義が一般的なチャーチ数と違っていて分かりにくかったので、検算用のコードを書きました。 ふつうのチャーチ数では、zero f x = x = KIfx、one f x = f x = Ifx、two f x = f (f x) = SBIfx と定義しますが、zero = I、one = V(KI)I、two = V(KI)(V(KI)I) という定義になってます。 こんな感じ(↓)で遊べます。 Main> toInt $ exp five (multi three two) 15625 Main> toBool $ greater (multi two five) (multi three t

    鳥たちと戯れる - Life Goes On
  • Rubyのある風景 - Y+Combinator+2

    以前取り上げたY Combinatorですが、何故"Y"なのかと思って調べてみたところ、どうやら"To Mock a Mockkingbird" がもとになっているようです。 このでは色々な鳥の名前を各ラムダ式に割り当てて、組み合わせ理論(Combinatory Logic)を解説しています。 ちなみにYは"Why Bird (aka Sage Bird)"だそうで。 さて、組み合わせ理論の有名な話として、 K = λxy.x S = λxyz.xz(yz) の二つを用いることで、チューリングマシンと等価な計算能力が得られるということが知られています(ということは、この二つさえあれば、今一般に使われているプログラムは全て記述できるわけですね)。 例えば、恒等写像I(λx.x)は SKK = (λxyz.xz(yz))(λxy.x)(λxy.x) = (λyz.(λxy.x)z(yz))(

  • λx.x K S K @ はてな - #009 賢人鳥をまねる

    OCaml では,let rec を使わずに再帰関数を模倣することができる. 但し「for ループを使えばできる」とかそういう話ではない. 例えば,階乗を計算する関数 fact は,通常 let rec を用いて, let rec fact n = if n > 0 then n * fact (n-1) else 1 と再帰的に定義されるが,次のように let rec を使わなくても定義できる.let turing (`M x) y = y (fun z -> x (`M x) y z) let fact = turing (`M turing) (fun f n -> if n > 0 then n * f (n-1) else 1) ちょっと読み難いが,実際に fact 10 と実行してみれば, 3628800 と正しい出力が得られることが確認できるだろう. このカラクリを支えている

    λx.x K S K @ はてな - #009 賢人鳥をまねる
  • 1