Idris
関数合成を連ねる感じで、Idris でプログラムを書いてみた。 何かのタネになるかもしれない。
これは「Idris Advent Calendar 2020 - Qiita」の6日目の記事です。 Idris で自然数の加法の交換法則を証明してみましょう。 以下のように Comm.idr を書いて、ロードします。 関数commの型だけを書いた状態です。 %default totalはおまじないだと思ってくだ…
すごいFizzBuzzがあったので紹介します。 let (m ~> str) x = str <$ guard (x `mod` m == 0) in map (fromMaybe . show <*> 3 ~> "fizz" <> 5 ~> "buzz") 何が何だかさっぱりですね！ これだけの機能を使っています。 1行目 ・ ~>内のMaybeオルタナティブ（…
出来たので上げます。 定理証明はあきらめて、計算で示すことにした。 完全6点グラフK6の15本の辺から、任意の3本を選ぶ。（comb） これにmap allとanyをかます。 メイン関数ramseyは、引数をそのまま渡すもの（赤い三角形）と、 引数をnotして渡すもの（青…
Twitterで「ベクトルを使うと5秒位で余弦定理証明できるので良い」 とあったので、Idris, Leanでチャレンジしてみた。 参考記事： ちなみに、余弦定理の証明に、 （成分表示で証明した）内積の分配法則を 使ってしまうと循環論法になるそうです。 自分は仮定…
Twitterで「各桁の和が3の倍数な整数は3の倍数、定理証明の練習に良さそう」 というのがあったので、チャレンジしてみる。 sumDigitは各桁の和を求める関数だが、 ここで一つズルをする。 直接、各桁の和を求めるのではなく、再帰した時の関係性を書くのだ。…
無限長のリストであるStreamは、 Idrisではlibs/prelude/Prelude/Stream.idrで以下のように定義されている。 ||| An infinite stream data Stream : Type -> Type where (::) : (value : elem) -> Inf (Stream elem) -> Stream elem これは以下と同等だそう…
挿入ソート - 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…
2021/11/20追記 自分では試してないが、以下の記事を参考にすると良いかもしれない。 【Termux】Google Play のTermuxはもうメンテされませーん！って言われているんだけれど… - 駅前散策ブログ＠かわさき HOT 【随時更新】個人的 Termuxセットアップメモ Id…
失敗の記録です。 ラムゼーの定理 - Wikipedia ラムゼーの有名なやつ とは 「6人いれば、互いに知り合いである3人組か、互いに知り合いでない3人組が存在する」 というものです。 グラフ理論の言葉で言うと、 「完全6点グラフの各辺を赤か青に彩色したとき、…
カリーのパラドックス - 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は、引数が真ならYesと証明を、偽ならNoと反証を返します。 （実際に判定、証明してくれる訳ではありません） そして、Not . Decな命題とは、証明も反証もできない命題という事になります。Fixは不動点コン…
証明の大まかな流れは、x1で反例があるとすると、それより小さいx2も反例になって、無限降下法より反例が無い事が言える、です。2014-07-15 18/11/18 完成しました！ 19/08/31 完成してねえええ！20/09/19 完成したかな
本記事では、関数型言語に触れているよくでてくる モナド について書きます。 Stateモナドを数学的に実装する Idrisでやってみた。 Control.Monad.Stateにもある。そこではモナド変換子として実装されている。 module MyState %default total -- %language E…
rev_rev_idとは、リストに、逆順にする事を2回すると、元に戻る、というやつだ。みょんみょんさんがIsabelleで、 いとうかつとしさんがAgdaで、実装動画を上げている。ならば僕は、Idrisでやろう、と奮い立った。 （Idrisを起動するときは、> idris -XElabRe…
