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

2021/11/20追記
自分では試してないが、以下の記事を参考にすると良いかもしれない。
【Termux】Google Play のTermuxはもうメンテされませーん！って言われているんだけれど… - 駅前散策ブログ＠かわさき HOT
【随時更新】個人的 Termuxセットアップメモ
Idrisのインストール | κeenのHappy Hacκing Blog

2020/05/09追記
うまくいかなくなっているようです。
修正記事を書くかどうかも未定です。

AndroidでIdris、Egison環境を構築できたので書いてみる。
アプリTermuxを使う。root化しなくても良い所が嬉しい。
使用スマホはZenFone 5、Android 8.0です。

1.端末を充電ケーブルに繋ぎ、スリープをOFFにする

2.Termux、Hacker's KeyboardをPlayストアからインストールする

3.Termuxを起動する

4.

$ pkg upgrade
$ pkg install wget proot

5.termux-ubuntuのインストール

$ mkdir -p ~/jails/ubuntu
$ cd ~/jails/ubuntu
$ wget https://raw.githubusercontent.com/Neo-Oli/termux-ubuntu/master/ubuntu.sh
$ bash ubuntu.sh

6.Ubuntuを起動

$ cd
$ cd ~/jails/ubuntu
$ ./start-ubuntu.sh

7.cabalのインストール

# apt-get update
# apt-get install cabal-install
# cabal update

8.Idrisのインストール

# apt-get install git make
# git clone git://github.com/idris-lang/Idris-dev.git idris
# cd idris
# echo 'CABALFLAGS += -f curses' > custom.mk
# make
（ここで一息つく）

9.Egisonのインストール

# cabal install regex-tdfa-1.2.3.1 --force-reinstalls
# cabal install egison --force-reinstalls
（ここで一息つく）

10.エディタnanoのインストール

# apt-get install nano

11.Idrisの実行

# cd
# cd .cabal/bin
# ./idris

12.Idrisの終了

> :q

13.Egisonの実行

# cd .cabal/bin
# ./egison

14.Egisonの終了

> [ctrl+d]
（Hacker's Keyboard使っているよね？！）

15.Ubuntuの終了

# exit

16.Termuxの終了

$ exit
（Enter）

今の場所に何があるか分からなくなったらpwdかls -LAFしましょう。
それでは素敵なプログラミングライフを！
（ついでにHaskellも使えるよ！）
.
.

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

失敗の記録です。

ラムゼーの定理 - Wikipedia

ラムゼーの有名なやつ　とは

「6人いれば、互いに知り合いである3人組か、互いに知り合いでない3人組が存在する」
というものです。

グラフ理論の言葉で言うと、
「完全6点グラフの各辺を赤か青に彩色したとき、どんな塗り分けに対しても、
赤一色の三角形か、青一色の三角形が存在する」
となります。

完全6点グラフの辺15本と、その論理式15個を引数にとり、
赤色三角形か青色三角形が存在する、というtheoremにした。

module Ramsey03

%default total


-- 頂点は A, B, C, D, E, F の6つ
data Vertex = A | B | C | D | E | F

-- 辺は未定義関数で、2つの頂点を取り、Bool値を返す
postulate edge : (v1, v2 : Vertex) -> Bool

syntax "RED" = False
syntax "BLUE" = True


lemma1 : edge A B = RED -> edge A C = RED -> edge A D = RED
  -> (b06, b10, b07 : Bool)
    -> edge B C = b06 -> edge C D = b10 -> edge B D = b07
      -> (v1 ** (v2 ** (v3 ** ((edge v1 v2) = (edge v2 v3), (edge v2 v3) = (edge v1 v3)) )))
-- A-B, A-C and B-C is RED.
lemma1 eAB eAC eAD  RED b10 b07  eBC eCD eBD  = (A ** (B ** (C ** (lemma1_1 eAB eBC, lemma1_2 eBC eAC) )))
  where
    lemma1_1 : edge A B = RED -> edge B C = RED -> edge A B = edge B C
    lemma1_1 eAB eBC = rewrite eAB in rewrite eBC in Refl
    lemma1_2 : edge B C = RED -> edge A C = RED -> edge B C = edge A C
    lemma1_2 eBC eAC = rewrite eBC in rewrite eAC in Refl
lemma1 eAB eAC eAD  BLUE b10 b07  eBC eCD eBD = ?lrhs_2

-- Aから出ている5本の辺(b01~b05)がどんな色でも、赤一色か青一色の三角形が存在する
ramsey : (b01, b02, b03, b04, b05,  b06, b07, b08, b09, b10, b11, b12, b13, b14, b15 : Bool)
  -> edge A B = b01 -> edge A C = b02 -> edge A D = b03 -> edge A E = b04 -> edge A F = b05
                    -> edge B C = b06 -> edge B D = b07 -> edge B E = b08 -> edge B F = b09
                                      -> edge C D = b10 -> edge C E = b11 -> edge C F = b12
                                                        -> edge D E = b13 -> edge D F = b14
                                                                          -> edge E F = b15
    -> (v1 ** (v2 ** (v3 ** ((edge v1 v2) = (edge v2 v3), (edge v2 v3) = (edge v1 v3)) )))
      -- A-B, A-C, A-D is RED.
ramsey RED RED RED b04 b05  b06 b07 b08 b09 b10 b11 b12 b13 b14 b15 eAB eAC eAD eAE eAF  eBC eBD eBE eBF  eCD eCE eCF  eDE eDF  eEF
  = lemma1 eAB eAC eAD  b06 b10 b07  eBC eCD eBD
ramsey RED RED BLUE b04 b05   b06 b07 b08 b09 b10 b11 b12 b13 b14 b15 eAB eAC eAD eAE eAF  eBC eBD eBE eBF  eCD eCE eCF  eDE eDF  eEF
  = ?rhs_2
ramsey RED BLUE b03 b04 b05     b06 b07 b08 b09 b10 b11 b12 b13 b14 b15 eAB eAC eAD eAE eAF  eBC eBD eBE eBF  eCD eCE eCF  eDE eDF  eEF
  = ?rhs_3
ramsey BLUE b02 b03 b04 b05       b06 b07 b08 b09 b10 b11 b12 b13 b14 b15 eAB eAC eAD eAE eAF  eBC eBD eBE eBF  eCD eCE eCF  eDE eDF  eEF
  = ?rhs_4

途中まで作ったところでギブした。
全部作ったらこの5倍以上のコード量になるだろう。
これはあかんでしょ。

Egisonでは数十行でできたのに、なんでや？！
設計方針が悪いのかなあ。
.
.

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

%default total


lemma : {X, Y : Type} -> (X = (X -> Y)) -> X
lemma p = rewrite p in \x=> let f = replace p x in f x

curry'sParadox : {X, Y : Type} -> (X = (X -> Y)) -> Y
curry'sParadox p = let x = lemma p in
                    let f = replace p x in f x

Egisonでラムゼーの有名なやつ

wikipedia:ラムゼーの定理

ラムゼーの有名なやつ　とは

「6人いれば、互いに知り合いである3人組か、互いに知り合いでない3人組が存在する」
というものです。

グラフ理論の言葉で言うと、
「完全6点グラフの各辺を赤か青に彩色したとき、どんな塗り分けに対しても、
赤一色の三角形か、青一色の三角形が存在する」
となります。

証明は以下です。 （Wikipediaより）

6つの点があり、その中のどの2つの点も赤い線か青い線で結ばれているとする。
赤一色の三角形か青一色の三角形が存在することを示せばよい。
6つの点のうち、どれでも良いので1つの点に着目し、その点をAとする。
Aからは5本の線が出ているので、そのうちの3本以上は同じ色の線である筈である。
.
Aから赤い線が3本以上出ている場合を考える。
Aと赤い線でつながっている点は3つ以上あるが、そのうちの3点をB,C,Dとする。
BとCが赤い線で結ばれている場合、三角形ABCはどの辺も赤い赤一色の三角形である。
CとD、DとBが赤い線で結ばれている場合も同様に赤一色の三角形が存在する。
よって、B,C,Dの中のいずれか2点が赤い線で結ばれている場合は赤一色の三角形が存在する。
そうでない場合、即ち、B,C,Dのうちどの2点も青い線で結ばれている場合、
三角形BCDはどの辺も青い青一色の三角形である。
よってこの場合も一色の三角形が存在する。
.
Aから青い線が3本以上出ている場合も同様である。

図を描くと分かりやすいです。

.
.

これをEgisonで証明します。

まず、Aから赤い線が3本以上出ている場合を考えます。
これらの線に1, 2, 3の名前を付けます。
これらの線に繋がっている三角形を4, 5, 6とし、
4, 5, 6のどんな塗り分けに対しても、
赤一色の三角形か、青一色の三角形が存在する事を言います。

.
.

公式ドキュメントにも載っている例です。
4,5,6を二つの集合に分けたと解釈できます。
第一集合を、辺を赤に塗ったもの、第二集合を、辺を青に塗ったものとします。
> (match-all {4 5 6} (multiset integer) [<join $xs $ys> {xs ys}])
{{{} {4 5 6}} {{4} {5 6}} {{5} {4 6}} {{6} {4 5}} {{4 5} {6}} {{4 6} {5}} {{5 6} {4}} {{4 5 6} {}}}
>

この出力の各第一集合（赤）に{1 2 3}と、インデックス100～107番を加えます。
それに対して三角形(456, 412, 523, 631)が存在するかパターンマッチします。
全てのインデックス100～107番が出力されれば、証明完了です。
.
.

.
.

EgisonでQuine

クワインとは、ソースコードと同じ文字列を出力するプログラムのことです。

3年前のこの記事のやりかたには欠陥があって、

s="...s=?...s.replace("?", s)..." ...s.replace("?", s)...

だと?が2箇所あるので、その2箇所にsが埋め込まれてしまいます。
なので、置換文字列には、2通りの表現方法があるものを使う必要があります。
前回のようにASCIIコード(itoc)を使っても良いですが、
今回はアルファベットの大文字小文字を使います。
「Z」を置換文字列にします。
.
.

実行結果
C:\me\Egison\quine>type quine.egi
(define $main (lambda [$args] (let {[$s "(define $main (lambda [$args] (let {[$s Z]} (print (S.replace (pack {(upper-case c#z)}) (show s) s)))))"]} (print (S.replace (pack {(upper-case c#z)}) (show s) s)))))
C:\me\Egison\quine>egison quine.egi
(define $main (lambda [$args] (let {[$s "(define $main (lambda [$args] (let {[$s Z]} (print (S.replace (pack {(upper-case c#z)}) (show s) s)))))"]} (print (S.replace (pack {(upper-case c#z)}) (show s) s)))))

.
.

Quine Museum

GitHubにQuine Museumというのがあって（こんなのがあるのですね）、そこにEgisonの、僕と違うやつもある。
.
.

Egisonでrev_rev_id？

失敗の記録です。
いつにも増して投げやりですが、許してください。
そんな、Egisonで定理証明なんて、無謀っすよ。

部分的な証明

;; (load-file "rev_rev_id.egi")

;; reverse 4要素以上
(define $myReverse
  (lambda [$xs]
    (match xs (list something)
      {[<nil> {}]
       [<snoc $x <cons $x2 $rs>>
        (snoc x2 (cons x (myReverse rs)))]
       [$y {y}] ;; ←誤魔化しがあるかも
      })))

;; snoc
(define $snoc
  (lambda [$x $xs] (append xs {x}) ))

;; proof
(define $theorem
  (lambda []
    (let {[$rs (myReverse (myReverse rs))]}
;; こっちが本来         (eq? (snoc x (cons x2 rs))
         (eq? (snoc x (cons x2 (myReverse (myReverse rs))))
              (myReverse (myReverse (snoc x (cons x2 rs)))) ))))

じっこ
C:\me\Egison\rev_rev_id
egison
Egison Version 3.7.12 (C) 2011-2018 Satoshi Egi
https://www.egison.org
Welcome to Egison Interpreter!
> (load-file "rev_rev_id.egi")
> (theorem)
#t
>

帰納法のinduction case、
(myReverse (myReverse rs)) = rsという仮定の元で、
(myReverse (myReverse (snoc x (cons x2 rs)))) = (snoc x (cons x2 rs))
を証明している。

read "x"を返す

「←誤魔化しがあるかも」のところを
read "(myReverse xs)"
とやれば、「xsを分解できない時は評価しない」を表現できる。
例として、
> (read "(* 3 5)")
(* 3 5)
>
となるのだが、これを再評価する手立ては無い。
"*"がついているのだが、これは関数ではなく、得体の知れない何かです。
まあ、ダメだってことです。

数学的帰納法

これも実装しないといけない。

rewrite

showで文字列に変えて、S.replaceで置換したらいけるかも。
一度文字列にしたら、readで戻しても評価できないので、最後にしかできない。

ガチでやるとしたら

「定理証明手習い」のJ-Bobとか、ACL2とかの実装が参考になると思う。
思っただけです。やらないです。
　
　
　
　
　

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

Idrisでゲーデルの不完全性定理を証明しました。

Decは、引数が真ならYesと証明を、偽ならNoと反証を返します。
（実際に判定、証明してくれる訳ではありません）
そして、Not . Decな命題とは、証明も反証もできない命題という事になります。

Fixは不動点コンビネータです。ここでは説明しません。

そして、notDec (Fix notDec)を証明しました。
これは、(Fix notDec)は証明できない事を表しています。

何気にすごいと自分では思っているのですが、どうでしょうか。

と思ったら、fixValueが停止しない気がしてきた。ダメっぽい。

18/09/30　修正しました。
いとうかつとしさんのuniversesを参考にしました。

ついでに第二不完全性定理も証明しました。

module Godel04

%default total
-- %language ElabReflection
%hide Dec

-- Decは、引数が真ならYesと証明を、偽ならNoと反証を返す
-- そして、Not . Decな命題とは、証明も反証もできない命題という事になる
data Dec : Type -> Type where
  Yes : (prf    : prop)         -> Dec prop
  No  : (contra : prop -> Void) -> Dec prop

notDec : Type -> Type
notDec = Not . Dec

-- 不動点コンビネータ
data Fix : (Type -> Type) -> Type where
  In : f (Fix f) -> Fix f
partial
Out : Fix f -> f (Fix f)
Out (In x) = x


partial
fixValue : Fix notDec
fixValue = In (Out fixValue)

-- (Fix notDec)は証明できない
partial
Godel'sIncompletenessTheorem : notDec (Fix notDec)
Godel'sIncompletenessTheorem = Out {f=notDec} fixValue

修正後

module Godel06

%default total
-- %language ElabReflection
%hide Dec
%hide Functor


-- Decは、引数が真ならYesと証明を、偽ならNoと反証を返す
-- そして、Not . Decな命題とは、証明も反証もできない命題という事になる
data Dec : Type -> Type where
  Yes : (prf    : prop)         -> Dec prop
  No  : (contra : prop -> Void) -> Dec prop

notDec : Type -> Type
notDec = Not . Dec

-- Functor
data Functor : Type where
  I : Functor
  K : Type -> Functor
  H : (Type -> Type) -> Functor

-- decoding function
decode : Functor -> Type -> Type
decode I x = x
decode (K c) _ = c
decode (H f) x = f x
syntax "[" [F] "]" [x] = decode F x

-- 不動点コンビネータ
data Fix : Functor -> Type where
  In : {F : Functor} -> decode F (Fix F) -> Fix F
Out : {F : Functor} -> Fix F -> [ F ] (Fix F)
Out (In x) = x


-- 第一不完全性定理
-- Fix (H notDec)が真ならば、Fix (H notDec)は証明できない
godel'sIncompletenessTheorem : Fix (H notDec) -> notDec (Fix (H notDec))
godel'sIncompletenessTheorem p = Out p



-- 二重否定除去
postulate dne : ((a -> Void) -> Void) -> a 

-- 第二不完全性定理
-- (0=1)が証明されない事が、体系の無矛盾性を表しているらしい
-- 体系が無矛盾ならば、それを証明できない
godel'sIncompletenessTheorem2nd : notDec (Z = (S Z)) -> notDec (notDec (Z = (S Z)))
godel'sIncompletenessTheorem2nd p _ = let p2 = dne (p . No) in absurd p2

18/12/08　さらに追記