コラッツ予想がとけたらいいな2

自分の考察を書いていきます。

Idris

何かのタネ

関数合成を連ねる感じで、Idris でプログラムを書いてみた。 何かのタネになるかもしれない。

自然数の加法の交換法則 by Idris

これは「Idris Advent Calendar 2020 - Qiita」の6日目の記事です。 Idris で自然数の加法の交換法則を証明してみましょう。 以下のように Comm.idr を書いて、ロードします。 関数commの型だけを書いた状態です。 %default totalはおまじないだと思ってくだ…

すごいFizzBuzz

すごいFizzBuzzがあったので紹介します。 let (m ~> str) x = str <$ guard (x `mod` m == 0) in map (fromMaybe . show <*> 3 ~> "fizz" <> 5 ~> "buzz") 何が何だかさっぱりですね! これだけの機能を使っています。 1行目 ・ ~>内のMaybeオルタナティブ(…

Idrisでラムゼーの有名なやつ、リベンジ

出来たので上げます。 定理証明はあきらめて、計算で示すことにした。 完全6点グラフK6の15本の辺から、任意の3本を選ぶ。(comb) これにmap allとanyをかます。 メイン関数ramseyは、引数をそのまま渡すもの(赤い三角形)と、 引数をnotして渡すもの(青…

Idris, Leanで余弦定理

Twitterで「ベクトルを使うと5秒位で余弦定理証明できるので良い」 とあったので、Idris, Leanでチャレンジしてみた。 参考記事: ちなみに、余弦定理の証明に、 (成分表示で証明した)内積の分配法則を 使ってしまうと循環論法になるそうです。 自分は仮定…

各桁の和が3の倍数な整数は3の倍数

Twitterで「各桁の和が3の倍数な整数は3の倍数、定理証明の練習に良さそう」 というのがあったので、チャレンジしてみる。 sumDigitは各桁の和を求める関数だが、 ここで一つズルをする。 直接、各桁の和を求めるのではなく、再帰した時の関係性を書くのだ。…

Idrisで余帰納?

無限長のリストであるStreamは、 Idrisではlibs/prelude/Prelude/Stream.idrで以下のように定義されている。 ||| An infinite stream data Stream : Type -> Type where (::) : (value : elem) -> Inf (Stream elem) -> Stream elem これは以下と同等だそう…

Idrisで挿入ソート

挿入ソート - Wikipedia foldrで挿入ソートを実装できることを知った。 insert : Nat -> List Nat -> List Nat insert x [] = [x] insert x (y::ys) = if lte x y then x :: y :: ys else y :: insert x ys -- 挿入ソート isort : List Nat -> List Nat isor…

Termuxを利用したAndroidでのIdris、Egison環境の構築

2020/05/09追記 うまくいかなくなっているようです。 修正記事を書くかどうかも未定です。 AndroidでIdris、Egison環境を構築できたので書いてみる。 アプリTermuxを使う。root化しなくても良い所が嬉しい。 使用スマホはZenFone 5、Android 8.0です。 1.端…

Idrisでラムゼーの有名なやつ、しかし……

失敗の記録です。 ラムゼーの定理 - Wikipedia ラムゼーの有名なやつ とは 「6人いれば、互いに知り合いである3人組か、互いに知り合いでない3人組が存在する」 というものです。 グラフ理論の言葉で言うと、 「完全6点グラフの各辺を赤か青に彩色したとき、…

Idrisでカリーのパラドックス

カリーのパラドックス - Wikipedia Idrisでもやってみた。Agda版とほとんど一緒。 Agdaでsubstは、Idrisではreplaceになる。 a=bと(func) aを渡すと(func) bを返してくれる。 lemmaも定理もlet f = replace p x in f xで終わる所が美しい。 module Curry %de…

IdrisとDecとFixと不完全性定理

Idrisでゲーデルの不完全性定理を証明しました。Decは、引数が真ならYesと証明を、偽ならNoと反証を返します。 (実際に判定、証明してくれる訳ではありません) そして、Not . Decな命題とは、証明も反証もできない命題という事になります。Fixは不動点コン…

<証明No.7・>割数列を用いたコラッツ予想の証明

証明の大まかな流れは、x1で反例があるとすると、それより小さいx2も反例になって、無限降下法より反例が無い事が言える、です。2014-07-15 18/11/18 完成しました! 19/08/31 完成してねえええ!20/09/19 完成したかな

IdrisでStateモナド

本記事では、関数型言語に触れているよくでてくる モナド について書きます。 Stateモナドを数学的に実装する Idrisでやってみた。 Control.Monad.Stateにもある。そこではモナド変換子として実装されている。 module MyState %default total -- %language E…

Idrisでrev_rev_id

rev_rev_idとは、リストに、逆順にする事を2回すると、元に戻る、というやつだ。みょんみょんさんがIsabelleで、 いとうかつとしさんがAgdaで、実装動画を上げている。ならば僕は、Idrisでやろう、と奮い立った。 (Idrisを起動するときは、> idris -XElabRe…