Mercurial > hg > Papers > 2020 > kono-prosym
changeset 3:57601db306e9
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 07 Jan 2021 13:28:35 +0900 |
| parents | 72ec93c67ab2 |
| children | 353edf5ef2d9 |
| files | Galois.mm Galois1.mm galois-prosym.ind info.txt main.tex presen.ind |
| diffstat | 6 files changed, 580 insertions(+), 43 deletions(-) [+] |
line wrap: on
line diff
--- a/Galois.mm Fri Dec 04 07:07:19 2020 +0900 +++ b/Galois.mm Thu Jan 07 13:28:35 2021 +0900 @@ -27,7 +27,7 @@ </node> </node> </node> -<node CREATED="1606376743358" ID="ID_396648943" MODIFIED="1606376745031" POSITION="right" TEXT="Agda"> +<node CREATED="1606376743358" FOLDED="true" ID="ID_396648943" MODIFIED="1606970261596" POSITION="right" TEXT="Agda"> <node CREATED="1606376745032" ID="ID_1337826128" MODIFIED="1606376830658" TEXT=" constructive logic "/> <node CREATED="1606376831782" ID="ID_470865242" MODIFIED="1606376838201" TEXT="functional programming language"/> <node CREATED="1606377112948" ID="ID_898910285" MODIFIED="1606377114878" TEXT="data type"> @@ -50,7 +50,7 @@ <node CREATED="1606377654200" ID="ID_744275621" MODIFIED="1606377660957" TEXT="as Unification"/> </node> </node> -<node CREATED="1606377593412" ID="ID_998775220" MODIFIED="1606377617749" POSITION="right" TEXT="Galois Theorem"> +<node CREATED="1606377593412" FOLDED="true" ID="ID_998775220" MODIFIED="1606970263675" POSITION="right" TEXT="Galois Theorem"> <node CREATED="1606377617749" ID="ID_833853645" MODIFIED="1606377627175" TEXT="equality on permutation"> <node CREATED="1606377627176" ID="ID_159348794" MODIFIED="1606377629558" TEXT="difficult"/> </node> @@ -117,7 +117,7 @@ </node> </node> </node> -<node CREATED="1606377006821" ID="ID_1359586090" MODIFIED="1606378512035" POSITION="left" TEXT="implementation"> +<node CREATED="1606377006821" FOLDED="true" ID="ID_1359586090" MODIFIED="1606970253780" POSITION="left" TEXT="implementation"> <node CREATED="1606377015762" ID="ID_287565717" MODIFIED="1606377020854" TEXT="group"> <node CREATED="1606377891530" ID="ID_1217977502" MODIFIED="1606377895546" TEXT="hierarchy"/> </node>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Galois1.mm Thu Jan 07 13:28:35 2021 +0900 @@ -0,0 +1,415 @@ +<map version="freeplane 1.8.0"> +<!--To view this file, download free mind mapping software Freeplane from http://freeplane.sourceforge.net --> +<node TEXT="Galois" FOLDED="false" ID="ID_1352391000" CREATED="1606376695618" MODIFIED="1606376704278"><hook NAME="MapStyle"> + <properties edgeColorConfiguration="#808080ff,#ff0000ff,#0000ffff,#00ff00ff,#ff00ffff,#00ffffff,#7c0000ff,#00007cff,#007c00ff,#7c007cff,#007c7cff,#7c7c00ff" fit_to_viewport="false"/> + +<map_styles> +<stylenode LOCALIZED_TEXT="styles.root_node" STYLE="oval" UNIFORM_SHAPE="true" VGAP_QUANTITY="24.0 pt"> +<font SIZE="24"/> +<stylenode LOCALIZED_TEXT="styles.predefined" POSITION="right" STYLE="bubble"> +<stylenode LOCALIZED_TEXT="default" ICON_SIZE="12.0 pt" COLOR="#000000" STYLE="fork"> +<font NAME="SansSerif" SIZE="10" BOLD="false" ITALIC="false"/> +</stylenode> +<stylenode LOCALIZED_TEXT="defaultstyle.details"/> +<stylenode LOCALIZED_TEXT="defaultstyle.attributes"> +<font SIZE="9"/> +</stylenode> +<stylenode LOCALIZED_TEXT="defaultstyle.note" COLOR="#000000" BACKGROUND_COLOR="#ffffff" TEXT_ALIGN="LEFT"/> +<stylenode LOCALIZED_TEXT="defaultstyle.floating"> +<edge STYLE="hide_edge"/> +<cloud COLOR="#f0f0f0" SHAPE="ROUND_RECT"/> +</stylenode> +</stylenode> +<stylenode LOCALIZED_TEXT="styles.user-defined" POSITION="right" STYLE="bubble"> +<stylenode LOCALIZED_TEXT="styles.topic" COLOR="#18898b" STYLE="fork"> +<font NAME="Liberation Sans" SIZE="10" BOLD="true"/> +</stylenode> +<stylenode LOCALIZED_TEXT="styles.subtopic" COLOR="#cc3300" STYLE="fork"> +<font NAME="Liberation Sans" SIZE="10" BOLD="true"/> +</stylenode> +<stylenode LOCALIZED_TEXT="styles.subsubtopic" COLOR="#669900"> +<font NAME="Liberation Sans" SIZE="10" BOLD="true"/> +</stylenode> +<stylenode LOCALIZED_TEXT="styles.important"> +<icon BUILTIN="yes"/> +</stylenode> +</stylenode> +<stylenode LOCALIZED_TEXT="styles.AutomaticLayout" POSITION="right" STYLE="bubble"> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level.root" COLOR="#000000" STYLE="oval" SHAPE_HORIZONTAL_MARGIN="10.0 pt" SHAPE_VERTICAL_MARGIN="10.0 pt"> +<font SIZE="18"/> +</stylenode> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,1" COLOR="#0033ff"> +<font SIZE="16"/> +</stylenode> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,2" COLOR="#00b439"> +<font SIZE="14"/> +</stylenode> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,3" COLOR="#990000"> +<font SIZE="12"/> +</stylenode> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,4" COLOR="#111111"> +<font SIZE="10"/> +</stylenode> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,5"/> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,6"/> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,7"/> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,8"/> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,9"/> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,10"/> +<stylenode LOCALIZED_TEXT="AutomaticLayout.level,11"/> +</stylenode> +</stylenode> +</map_styles> +</hook> +<node TEXT="polynominnal equation" POSITION="right" ID="ID_765661988" CREATED="1606376704806" MODIFIED="1606376724261"> +<node TEXT="permutation of solution" ID="ID_470208262" CREATED="1606376929822" MODIFIED="1606376964230"/> +<node TEXT="permutation group" ID="ID_753384811" CREATED="1606376967368" MODIFIED="1606376989881"/> +<node TEXT="reducing order" ID="ID_904343771" CREATED="1606376992888" MODIFIED="1606377002273"/> +</node> +<node TEXT="permutation" POSITION="right" ID="ID_1615933996" CREATED="1606376727933" MODIFIED="1606376730351"> +<node TEXT="mathematical notation" ID="ID_541308822" CREATED="1606377983762" MODIFIED="1606377988452"> +<node TEXT="abc" ID="ID_872236328" CREATED="1606377988737" MODIFIED="1606377990116"/> +</node> +</node> +<node TEXT="group" FOLDED="true" POSITION="right" ID="ID_1769513270" CREATED="1606376850192" MODIFIED="1606376853835"> +<node TEXT="symmetric" ID="ID_1566417965" CREATED="1606376853836" MODIFIED="1606376857323"/> +<node TEXT="commutator" ID="ID_1797364624" CREATED="1606376863163" MODIFIED="1606376870102"/> +<node TEXT="solvable" FOLDED="true" ID="ID_1581604178" CREATED="1606376886069" MODIFIED="1606376889986"> +<node TEXT="commutator is singleton" ID="ID_269958268" CREATED="1606376891769" MODIFIED="1606376910710"/> +<node TEXT="commutator enumeration" FOLDED="true" ID="ID_1136118392" CREATED="1606377741327" MODIFIED="1606377747155"> +<node TEXT="just a calcuration" ID="ID_389205569" CREATED="1606377747156" MODIFIED="1606377753781"/> +<node TEXT="is that a proof?" FOLDED="true" ID="ID_767647256" CREATED="1606377754818" MODIFIED="1606377760601"> +<node TEXT="first list contains everything" ID="ID_1858190223" CREATED="1606378353555" MODIFIED="1606378362619"/> +<node TEXT="is exact commutator list" ID="ID_188849330" CREATED="1606378363564" MODIFIED="1606378390432"/> +<node TEXT="everything have to be connected" ID="ID_838630093" CREATED="1606378391310" MODIFIED="1606378455916"/> +<node TEXT="in Agda" ID="ID_1529743539" CREATED="1606378457553" MODIFIED="1606378464964"/> +</node> +</node> +</node> +</node> +<node TEXT="Agda" FOLDED="true" POSITION="right" ID="ID_396648943" CREATED="1606376743358" MODIFIED="1606376745031"> +<node TEXT=" constructive logic " ID="ID_1337826128" CREATED="1606376745032" MODIFIED="1606376830658"/> +<node TEXT="functional programming language" ID="ID_470865242" CREATED="1606376831782" MODIFIED="1606376838201"/> +<node TEXT="data type" FOLDED="true" ID="ID_898910285" CREATED="1606377112948" MODIFIED="1606377114878"> +<node TEXT="Data.Fin" ID="ID_1941155842" CREATED="1606377114879" MODIFIED="1606377118014"/> +<node TEXT="Data.Fin.Permutation" ID="ID_1139692699" CREATED="1606377121895" MODIFIED="1606377131304"/> +<node TEXT="Data.List.Fresh" FOLDED="true" ID="ID_149755525" CREATED="1606377132775" MODIFIED="1606377139512"> +<node TEXT="direct write" ID="ID_1375126776" CREATED="1606727196377" MODIFIED="1606727202570"/> +</node> +<node TEXT="Data.List Any" ID="ID_698861196" CREATED="1606377780220" MODIFIED="1606377792633"/> +</node> +<node TEXT="data type with " FOLDED="true" ID="ID_984157342" CREATED="1606727152968" MODIFIED="1606727165737"> +<node TEXT="proof" ID="ID_1571937464" CREATED="1606727165738" MODIFIED="1606727167433"/> +<node TEXT="constraint" ID="ID_876063224" CREATED="1606727174606" MODIFIED="1606727178757"/> +</node> +<node TEXT="Bijection" FOLDED="true" ID="ID_316648697" CREATED="1606378049124" MODIFIED="1606378053107"> +<node TEXT="strange notation" ID="ID_641510883" CREATED="1606378059541" MODIFIED="1606378065594"/> +</node> +<node TEXT="equality" FOLDED="true" ID="ID_109508194" CREATED="1606377647512" MODIFIED="1606377651001"> +<node TEXT="as Set" ID="ID_1995052319" CREATED="1606377651001" MODIFIED="1606377653316"/> +<node TEXT="as Unification" ID="ID_744275621" CREATED="1606377654200" MODIFIED="1606377660957"/> +</node> +</node> +<node TEXT="Galois Theorem" FOLDED="true" POSITION="right" ID="ID_998775220" CREATED="1606377593412" MODIFIED="1606377617749"> +<node TEXT="equality on permutation" FOLDED="true" ID="ID_833853645" CREATED="1606377617749" MODIFIED="1606377627175"> +<node TEXT="difficult" ID="ID_159348794" CREATED="1606377627176" MODIFIED="1606377629558"/> +</node> +<node TEXT="equality on FL" FOLDED="true" ID="ID_1966973817" CREATED="1606377634711" MODIFIED="1606377642062"> +<node TEXT="refl" ID="ID_918693225" CREATED="1606377642062" MODIFIED="1606377645984"/> +</node> +</node> +<node TEXT="analysis" FOLDED="true" POSITION="right" ID="ID_594485495" CREATED="1606377913808" MODIFIED="1606377920415"> +<node TEXT="concrete and abstract" ID="ID_827184530" CREATED="1606377921047" MODIFIED="1606377932723"/> +<node TEXT="dynamic and static" ID="ID_1751276075" CREATED="1606377933376" MODIFIED="1606377938290"/> +<node TEXT="unfinished proofs" FOLDED="true" ID="ID_710334852" CREATED="1606378218212" MODIFIED="1606378233384"> +<node TEXT="Any" FOLDED="true" ID="ID_488108201" CREATED="1606378233385" MODIFIED="1606378236686"> +<node TEXT="carry Any returning function" ID="ID_1670776002" CREATED="1606378407387" MODIFIED="1606378417108"/> +</node> +<node TEXT="Commutator" FOLDED="true" ID="ID_1026280756" CREATED="1606378237149" MODIFIED="1606378246179"> +<node TEXT="done" ID="ID_1577934229" CREATED="1606727134876" MODIFIED="1606727138330"/> +</node> +<node TEXT="computation is possible" ID="ID_1867193418" CREATED="1606378250310" MODIFIED="1606378258673"/> +</node> +<node TEXT="computation time" FOLDED="true" ID="ID_502942305" CREATED="1606377946668" MODIFIED="1606377952605"> +<node TEXT="on proof" ID="ID_530532314" CREATED="1606377952606" MODIFIED="1606377954403"/> +<node TEXT="on enumaration" ID="ID_1325791815" CREATED="1606377955030" MODIFIED="1606377958838"/> +<node TEXT="no type inference on computation" ID="ID_864429394" CREATED="1606728034991" MODIFIED="1606728050441"/> +<node TEXT="overhead" FOLDED="true" ID="ID_463456042" CREATED="1606728051458" MODIFIED="1606728057116"> +<node TEXT="what is fresh list?" ID="ID_777871568" CREATED="1606728057117" MODIFIED="1606728073829"/> +<node TEXT="garbage" ID="ID_480597562" CREATED="1606728079796" MODIFIED="1606728084210"/> +</node> +</node> +<node TEXT="easier solution?" FOLDED="true" ID="ID_1589402453" CREATED="1606378008534" MODIFIED="1606378016376"> +<node TEXT="direct FL injection" ID="ID_1440585232" CREATED="1606378016376" MODIFIED="1606378026002"/> +<node TEXT="define FL-Group" FOLDED="true" ID="ID_1856387313" CREATED="1606378089783" MODIFIED="1606378097519"> +<node TEXT="define commutator for it" ID="ID_644573596" CREATED="1606378102162" MODIFIED="1606378116983"/> +<node TEXT="as concrete data " ID="ID_732030297" CREATED="1606378133381" MODIFIED="1606378150072"/> +</node> +<node TEXT="coinduction?" ID="ID_116943440" CREATED="1606379185458" MODIFIED="1606379189022"/> +</node> +<node TEXT="programming tech" FOLDED="true" ID="ID_56894444" CREATED="1606727239462" MODIFIED="1606727245853"> +<node TEXT="hole" FOLDED="true" ID="ID_1678999565" CREATED="1606728272433" MODIFIED="1606728275384"> +<node TEXT="unfinished proof" ID="ID_1070945075" CREATED="1606728276558" MODIFIED="1606728283528"/> +</node> +<node TEXT="unicode" FOLDED="true" ID="ID_1396622569" CREATED="1606727474640" MODIFIED="1606727477580"> +<node TEXT="like math book" ID="ID_1012474406" CREATED="1606727477581" MODIFIED="1606727485082"/> +</node> +<node TEXT="parallel recursion" ID="ID_1951835354" CREATED="1606727246300" MODIFIED="1606727254702"/> +<node TEXT="equalit" FOLDED="true" ID="ID_1240709277" CREATED="1606727588877" MODIFIED="1606727592242"> +<node TEXT="as refl" ID="ID_1313466010" CREATED="1606727592242" MODIFIED="1606727596598"/> +<node TEXT="as data" ID="ID_151150017" CREATED="1606727597429" MODIFIED="1606727600720"/> +<node TEXT="as record" ID="ID_474379006" CREATED="1606727601827" MODIFIED="1606727606619"/> +</node> +<node TEXT="mutual reference" FOLDED="true" ID="ID_805972014" CREATED="1606727260417" MODIFIED="1606727267607"> +<node TEXT="insertFL" ID="ID_232896969" CREATED="1606727295033" MODIFIED="1606727301472"/> +<node TEXT="list and fresh" ID="ID_808432820" CREATED="1606727305059" MODIFIED="1606727314613"/> +</node> +<node TEXT="Any" FOLDED="true" ID="ID_910007043" CREATED="1606727277546" MODIFIED="1606727280266"> +<node TEXT="insAny" ID="ID_1325857165" CREATED="1606727280267" MODIFIED="1606727286773"/> +</node> +<node TEXT="naming" ID="ID_1511159834" CREATED="1606727343852" MODIFIED="1606727347919"/> +<node TEXT="reference in a function" FOLDED="true" ID="ID_296697488" CREATED="1606727349007" MODIFIED="1606727370890"> +<node TEXT="as module" ID="ID_402061017" CREATED="1606727370891" MODIFIED="1606727373382"/> +</node> +<node TEXT="mononorphism" FOLDED="true" ID="ID_1372261696" CREATED="1606727379879" MODIFIED="1606727386518"> +<node TEXT="renaming" ID="ID_190346980" CREATED="1606727386519" MODIFIED="1606727391497"/> +<node TEXT="hiding" ID="ID_302032810" CREATED="1606727391865" MODIFIED="1606727394834"/> +</node> +</node> +</node> +<node TEXT="presentation" POSITION="right" ID="ID_1629686657" CREATED="1609990079623" MODIFIED="1609990087321"> +<node TEXT="motivation" ID="ID_68741792" CREATED="1609990469910" MODIFIED="1609990474518"> +<node TEXT="agda say" ID="ID_1410322270" CREATED="1609990475271" MODIFIED="1609990535394"> +<node TEXT="prove all of it" ID="ID_255800370" CREATED="1609990535912" MODIFIED="1609990544007"/> +</node> +<node TEXT="proof carrying data structure" ID="ID_701544233" CREATED="1609990566444" MODIFIED="1609990575065"/> +<node TEXT="all connected" ID="ID_1374956235" CREATED="1609990614612" MODIFIED="1609990619047"> +<node TEXT="not only the result" ID="ID_182559689" CREATED="1609990619481" MODIFIED="1609990628683"/> +<node TEXT="the result is proved to be correct" ID="ID_1428974315" CREATED="1609990629258" MODIFIED="1609990638772"/> +<node TEXT="What are you computing?" ID="ID_1070455381" CREATED="1609990639215" MODIFIED="1609990646503"/> +</node> +</node> +<node TEXT="galois theory" ID="ID_808810318" CREATED="1609990087828" MODIFIED="1609990103294"> +<node TEXT="polynominal equation" ID="ID_136330816" CREATED="1609990103797" MODIFIED="1609990113989"/> +<node TEXT="symmetric group on solutions" ID="ID_559235306" CREATED="1609990117978" MODIFIED="1609990145025"/> +<node TEXT="group mapping" ID="ID_1179675147" CREATED="1609990150139" MODIFIED="1609990186166"/> +<node TEXT="commutator" ID="ID_226118641" CREATED="1609990196079" MODIFIED="1609990198775"/> +<node TEXT="commutator group" ID="ID_742353850" CREATED="1609990200853" MODIFIED="1609990215758"/> +<node TEXT="solvable" ID="ID_1341500727" CREATED="1609990258050" MODIFIED="1609990261861"/> +</node> +<node TEXT="proof in math text book" ID="ID_789226485" CREATED="1609990263397" MODIFIED="1609990271252"/> +<node TEXT="formalization in agda" ID="ID_202327619" CREATED="1609990273986" MODIFIED="1609990286861"> +<node TEXT="agda introduction" ID="ID_35495184" CREATED="1609990288383" MODIFIED="1609990293516"> +<node TEXT="lambda" ID="ID_1794615583" CREATED="1609990303910" MODIFIED="1609990309568"/> +<node TEXT="data" ID="ID_1613871642" CREATED="1609990294061" MODIFIED="1609990295779"/> +<node TEXT="record" ID="ID_1150956997" CREATED="1609990296397" MODIFIED="1609990301522"/> +<node TEXT="unification" ID="ID_855340831" CREATED="1609990314851" MODIFIED="1609990323913"> +<node TEXT="equation" ID="ID_1714263025" CREATED="1609990324367" MODIFIED="1609990326267"/> +</node> +</node> +<node TEXT="commutator" ID="ID_1080677255" CREATED="1609990330404" MODIFIED="1609990340997"> +<node TEXT="Set valued function" ID="ID_477756039" CREATED="1609990341400" MODIFIED="1609990348973"/> +</node> +<node TEXT="solvable" ID="ID_178918488" CREATED="1609990354030" MODIFIED="1609990359075"/> +</node> +<node TEXT="symmetric group representation in agda" ID="ID_1083504702" CREATED="1609990379507" MODIFIED="1609990393339"> +<node TEXT="Data.Fin" ID="ID_1340949296" CREATED="1609990393883" MODIFIED="1609990404918"/> +<node TEXT="Bijection" ID="ID_316860227" CREATED="1609990405535" MODIFIED="1609990409631"/> +<node TEXT="List" ID="ID_1710126935" CREATED="1609990410154" MODIFIED="1609990413645"/> +<node TEXT="FL" ID="ID_235104633" CREATED="1609990415278" MODIFIED="1609990419436"/> +</node> +<node TEXT="proofs" ID="ID_1219242238" CREATED="1609992596012" MODIFIED="1609992600251"> +<node TEXT="2" OBJECT="java.lang.Long|2" ID="ID_514245484" CREATED="1609992600706" MODIFIED="1609992602407"/> +<node TEXT="injection" ID="ID_1366306030" CREATED="1609992603682" MODIFIED="1609992607205"> +<node TEXT="List <-> Permutation" ID="ID_1791881124" CREATED="1609992680676" MODIFIED="1609992688813"/> +<node TEXT="FL <-> Permutation" ID="ID_1601662820" CREATED="1609992667945" MODIFIED="1609992677520"/> +</node> +<node TEXT="3" OBJECT="java.lang.Long|3" ID="ID_1113221609" CREATED="1609992624578" MODIFIED="1609992625803"/> +<node TEXT="5" OBJECT="java.lang.Long|5" ID="ID_1339672501" CREATED="1609992627836" MODIFIED="1609992629038"> +<node TEXT="two sym 3" ID="ID_1648879383" CREATED="1609990866219" MODIFIED="1609991318427"/> +</node> +</node> +<node TEXT="a list contains everything" ID="ID_67235294" CREATED="1609990709190" MODIFIED="1609990733750"> +<node TEXT="sorted" ID="ID_73107613" CREATED="1609990734279" MODIFIED="1609990738112"/> +<node TEXT="any" ID="ID_1569296473" CREATED="1609990738656" MODIFIED="1609990745411"/> +</node> +<node TEXT="Fresh List" ID="ID_928929976" CREATED="1609990754285" MODIFIED="1609990759712"> +<node TEXT="Set valued function" ID="ID_1431257568" CREATED="1609990760342" MODIFIED="1609990767070"/> +<node TEXT="proof carrying data structure" ID="ID_1418161020" CREATED="1609990772447" MODIFIED="1609990792611"/> +<node TEXT="Any" ID="ID_1141421059" CREATED="1609990819140" MODIFIED="1609990822050"> +<node TEXT="here" ID="ID_1546836780" CREATED="1609991661319" MODIFIED="1609991663000"/> +<node TEXT="there" ID="ID_1162193758" CREATED="1609991663489" MODIFIED="1609991665378"/> +</node> +<node TEXT="insert" ID="ID_1479901665" CREATED="1609990795810" MODIFIED="1609990799803"/> +<node TEXT="insert / cons and Any" ID="ID_265930485" CREATED="1609990800355" MODIFIED="1609990813411"/> +</node> +<node TEXT="proofs" ID="ID_71982613" CREATED="1609990838839" MODIFIED="1609990843748"> +<node TEXT="2" OBJECT="java.lang.Long|2" ID="ID_1357773799" CREATED="1609990844233" MODIFIED="1609990848197"/> +<node TEXT="3" OBJECT="java.lang.Long|3" ID="ID_285070989" CREATED="1609990848906" MODIFIED="1609990849643"/> +<node TEXT="5" OBJECT="java.lang.Long|5" ID="ID_553387365" CREATED="1609990862246" MODIFIED="1609990864317"/> +<node TEXT="4" OBJECT="java.lang.Long|4" ID="ID_922425691" CREATED="1609991325580" MODIFIED="1609991327765"/> +<node TEXT="5" OBJECT="java.lang.Long|5" ID="ID_884482373" CREATED="1609991337411" MODIFIED="1609991338693"> +<node TEXT="compilation" ID="ID_1593187399" CREATED="1609991339281" MODIFIED="1609991342163"/> +</node> +</node> +<node TEXT="analysis" ID="ID_1668179685" CREATED="1609991697619" MODIFIED="1609991708118"> +<node TEXT="overhead of proof carrying data structure" ID="ID_976735517" CREATED="1609991348749" MODIFIED="1609991361000"> +<node TEXT="type" ID="ID_652487156" CREATED="1609991361589" MODIFIED="1609991365082"/> +<node TEXT="heap" ID="ID_876968413" CREATED="1609991365590" MODIFIED="1609991378981"> +<node TEXT="product" ID="ID_198657579" CREATED="1609991379414" MODIFIED="1609991383275"/> +</node> +<node TEXT="type check" ID="ID_1804210435" CREATED="1609991389516" MODIFIED="1609991394532"/> +<node TEXT="compiled" ID="ID_1786891269" CREATED="1609991395061" MODIFIED="1609991405394"/> +</node> +<node TEXT="connection of computation and type" ID="ID_1028780772" CREATED="1609991716388" MODIFIED="1609991737610"/> +</node> +<node TEXT="appendix" ID="ID_1923999271" CREATED="1609991414119" MODIFIED="1609991419659"> +<node TEXT="ZF fix" ID="ID_639095351" CREATED="1609991419999" MODIFIED="1609991498844"> +<node TEXT="od max" ID="ID_882118125" CREATED="1609991570586" MODIFIED="1609991574172"> +<node TEXT="Set and Class" ID="ID_785523216" CREATED="1609991576795" MODIFIED="1609991581126"/> +</node> +</node> +<node TEXT="next" ID="ID_987134788" CREATED="1609991499494" MODIFIED="1609991503587"> +<node TEXT="tychonov" ID="ID_1788489591" CREATED="1609991504061" MODIFIED="1609991513116"> +<node TEXT="topology" ID="ID_188550186" CREATED="1609991514960" MODIFIED="1609991518554"/> +</node> +<node TEXT="ZF" ID="ID_1650804627" CREATED="1609991556425" MODIFIED="1609991560227"> +<node TEXT="cohen model" ID="ID_77996053" CREATED="1609991560836" MODIFIED="1609991563971"/> +</node> +</node> +</node> +</node> +<node TEXT="implementation" POSITION="left" ID="ID_1359586090" CREATED="1606377006821" MODIFIED="1606378512035"> +<node TEXT="group" FOLDED="true" ID="ID_287565717" CREATED="1606377015762" MODIFIED="1606377020854"> +<node TEXT="hierarchy" ID="ID_1217977502" CREATED="1606377891530" MODIFIED="1606377895546"/> +</node> +<node TEXT="permutation" FOLDED="true" ID="ID_618128777" CREATED="1606377021262" MODIFIED="1606377026259"> +<node TEXT="bijection on Data.Fin" FOLDED="true" ID="ID_597466250" CREATED="1606377091642" MODIFIED="1606377110065"> +<node TEXT="abstract" ID="ID_1158865640" CREATED="1606378591811" MODIFIED="1606378598578"/> +</node> +<node TEXT="combinator" FOLDED="true" ID="ID_1921597264" CREATED="1606377392195" MODIFIED="1606377397374"> +<node TEXT="prep" ID="ID_330696821" CREATED="1606377397374" MODIFIED="1606377403998"/> +<node TEXT="swap" ID="ID_1228887457" CREATED="1606377426743" MODIFIED="1606377430099"/> +<node TEXT="pins" ID="ID_478525497" CREATED="1606377451571" MODIFIED="1606377453688"/> +<node TEXT="not unique" ID="ID_1582208431" CREATED="1606378599458" MODIFIED="1606378602838"/> +</node> +<node TEXT="List ℕ" FOLDED="true" ID="ID_447332615" CREATED="1606377147557" MODIFIED="1606377174712"> +<node TEXT="not unique" ID="ID_608038587" CREATED="1606378608757" MODIFIED="1606378614329"/> +</node> +<node TEXT="FL n" FOLDED="true" ID="ID_1784079007" CREATED="1606377179308" MODIFIED="1606377183560"> +<node TEXT="decremental Data.Fin List" FOLDED="true" ID="ID_1790506416" CREATED="1606377183560" MODIFIED="1606377199633"> +<node TEXT="unique" ID="ID_665257211" CREATED="1606378617080" MODIFIED="1606378619230"/> +<node TEXT="1 to 1" ID="ID_1530010631" CREATED="1606378626590" MODIFIED="1606378628302"/> +</node> +<node TEXT="FL n to Perm" ID="ID_767155416" CREATED="1606377458903" MODIFIED="1606377465105"/> +<node TEXT="Perm to FL" ID="ID_135453080" CREATED="1606377465737" MODIFIED="1606377469086"/> +<node TEXT="iso" ID="ID_1105006832" CREATED="1606377470255" MODIFIED="1606377472861"/> +<node TEXT="injection" ID="ID_846590614" CREATED="1606377473713" MODIFIED="1606377475642"/> +</node> +<node TEXT="conversion" FOLDED="true" ID="ID_1747777855" CREATED="1606377382892" MODIFIED="1606377386415"> +<node TEXT="direct refl" ID="ID_932941583" CREATED="1606727219039" MODIFIED="1606727227206"/> +</node> +</node> +<node TEXT="enumeration of permutation" FOLDED="true" ID="ID_1172252989" CREATED="1606377221243" MODIFIED="1606377228975"> +<node TEXT="List" ID="ID_239078628" CREATED="1606377230408" MODIFIED="1606377235895"/> +<node TEXT="Fresh List" FOLDED="true" ID="ID_1866566989" CREATED="1606377236436" MODIFIED="1606377239550"> +<node TEXT="term itself is simple" ID="ID_536448598" CREATED="1606378273582" MODIFIED="1606378282243"/> +<node TEXT="type is complicated" ID="ID_334436404" CREATED="1606378284710" MODIFIED="1606378294962"/> +</node> +</node> +<node TEXT="commutator" FOLDED="true" ID="ID_368973198" CREATED="1606377028929" MODIFIED="1606377032873"> +<node TEXT="generator" FOLDED="true" ID="ID_134730969" CREATED="1606377252812" MODIFIED="1606377264147"> +<node TEXT="not necessary" ID="ID_1941243109" CREATED="1606727532690" MODIFIED="1606727540677"/> +</node> +<node TEXT="cong" ID="ID_85252223" CREATED="1606377266582" MODIFIED="1606377272449"/> +</node> +<node TEXT="solvable" FOLDED="true" ID="ID_1847720925" CREATED="1606377033697" MODIFIED="1606377036804"> +<node TEXT="second order" ID="ID_854168913" CREATED="1606377038096" MODIFIED="1606377049483"/> +<node TEXT="third order" FOLDED="true" ID="ID_795750040" CREATED="1606377050074" MODIFIED="1606377055050"> +<node TEXT="a lof of easy equation" ID="ID_1251443358" CREATED="1606377679670" MODIFIED="1606377695159"/> +</node> +<node TEXT="forth order" FOLDED="true" ID="ID_128064534" CREATED="1606377055860" MODIFIED="1606377059872"> +<node TEXT="too many" ID="ID_660493111" CREATED="1606377695633" MODIFIED="1606377699494"/> +<node TEXT="use Fresh list" ID="ID_1107095798" CREATED="1606377807636" MODIFIED="1606377814089"/> +</node> +<node TEXT="fifth order" FOLDED="true" ID="ID_1986356" CREATED="1606377067933" MODIFIED="1606377071318"> +<node TEXT="5 contains 3" ID="ID_1761950431" CREATED="1606377814808" MODIFIED="1606377837816"/> +<node TEXT="in two different parts" ID="ID_649320127" CREATED="1606377838561" MODIFIED="1606377854524"/> +</node> +</node> +<node TEXT="solvable by Fresh List" FOLDED="true" ID="ID_1242936721" CREATED="1606377705411" MODIFIED="1606377721190"> +<node TEXT="sorted" ID="ID_228290840" CREATED="1606377721190" MODIFIED="1606377724012"/> +<node TEXT="insert" ID="ID_55633177" CREATED="1606377861188" MODIFIED="1606377863199"/> +<node TEXT="any" FOLDED="true" ID="ID_1234121961" CREATED="1606377863601" MODIFIED="1606377865965"> +<node TEXT="it contains everything?" ID="ID_1547561546" CREATED="1606377874500" MODIFIED="1606377881123"/> +</node> +</node> +<node TEXT="Equalizer" FOLDED="true" ID="ID_1439868847" CREATED="1606377291291" MODIFIED="1606377314716"> +<node TEXT="equality on concrete object" ID="ID_503791605" CREATED="1606377314717" MODIFIED="1606377329048"/> +<node TEXT="equality on abstract object" ID="ID_1955667161" CREATED="1606377330172" MODIFIED="1606377336895"/> +</node> +</node> +<node TEXT="paper" POSITION="left" ID="ID_873264480" CREATED="1606378512784" MODIFIED="1606378523086"> +<node TEXT="problem" FOLDED="true" ID="ID_696482092" CREATED="1606379096805" MODIFIED="1606379099309"> +<node TEXT="enumerating commutator" ID="ID_752930881" CREATED="1606379099309" MODIFIED="1606379107094"/> +<node TEXT="is this really a proof?" ID="ID_1614555070" CREATED="1606379107643" MODIFIED="1606379117201"/> +<node TEXT="all connected in Agda" ID="ID_1678061189" CREATED="1606379124041" MODIFIED="1606379130309"/> +</node> +<node TEXT="Galois introduction" FOLDED="true" ID="ID_917416576" CREATED="1606378515709" MODIFIED="1606378542758"> +<node TEXT="easy and quick" ID="ID_1764355857" CREATED="1606727909781" MODIFIED="1606727916012"/> +</node> +<node TEXT="Agda introduction" FOLDED="true" ID="ID_434512007" CREATED="1606378543316" MODIFIED="1606378547552"> +<node TEXT="Group representation" ID="ID_762123734" CREATED="1606378554127" MODIFIED="1606378563015"/> +<node TEXT="Permutation" ID="ID_610013381" CREATED="1606378568196" MODIFIED="1606378572610"/> +</node> +<node TEXT="Representation of Permutation" ID="ID_1573892815" CREATED="1606378575594" MODIFIED="1606378585288"> +<node TEXT="math" FOLDED="true" ID="ID_1797326547" CREATED="1606378644922" MODIFIED="1606378648975"> +<node TEXT="abc" ID="ID_1052913615" CREATED="1606378648976" MODIFIED="1606378650331"/> +</node> +<node TEXT="list" FOLDED="true" ID="ID_1900422285" CREATED="1606378653895" MODIFIED="1606378655245"> +<node TEXT="not unique" ID="ID_844966393" CREATED="1606378655246" MODIFIED="1606378658614"/> +<node TEXT="no permutation property" ID="ID_1727235552" CREATED="1606378668243" MODIFIED="1606378675693"/> +</node> +<node TEXT="bijection" FOLDED="true" ID="ID_1560893595" CREATED="1606378662595" MODIFIED="1606378666125"> +<node TEXT="abstract" ID="ID_147732297" CREATED="1606378666126" MODIFIED="1606378695445"/> +</node> +<node TEXT="combinator" FOLDED="true" ID="ID_1561884094" CREATED="1606378701314" MODIFIED="1606378706107"> +<node TEXT="not unique" ID="ID_560079212" CREATED="1606378706108" MODIFIED="1606378708991"/> +</node> +<node TEXT="FL" FOLDED="true" ID="ID_1817493034" CREATED="1606378715224" MODIFIED="1606378717668"> +<node TEXT="unique" ID="ID_1607834497" CREATED="1606378717668" MODIFIED="1606378719860"/> +<node TEXT="1 to 1" ID="ID_1710096678" CREATED="1606378721382" MODIFIED="1606378723061"/> +</node> +</node> +<node TEXT="enumeration of FL" ID="ID_1432020010" CREATED="1606378927269" MODIFIED="1606378933032"> +<node TEXT="Fresh List" ID="ID_124351974" CREATED="1606378933032" MODIFIED="1606378936038"/> +<node TEXT="Any" ID="ID_863395146" CREATED="1606378936579" MODIFIED="1606378938352"/> +</node> +<node TEXT="Solvable" FOLDED="true" ID="ID_115815719" CREATED="1606378586134" MODIFIED="1606378745085"> +<node TEXT="Commutator" ID="ID_132480944" CREATED="1606378745085" MODIFIED="1606378748529"/> +<node TEXT="Commutator implementationn" ID="ID_326008986" CREATED="1606378750600" MODIFIED="1606378757686"/> +</node> +<node TEXT="proof os Solvability" ID="ID_1064018730" CREATED="1606378771575" MODIFIED="1606378780946"> +<node TEXT="on abstract Permutation" FOLDED="true" ID="ID_679164783" CREATED="1606378780946" MODIFIED="1606378788919"> +<node TEXT="on 2" ID="ID_1953177659" CREATED="1606378834624" MODIFIED="1606378835927"/> +</node> +<node TEXT="using FL" FOLDED="true" ID="ID_1180179827" CREATED="1606378791247" MODIFIED="1606378794009"> +<node TEXT="on 3" ID="ID_1092149501" CREATED="1606378809099" MODIFIED="1606378817784"/> +<node TEXT="on 5" ID="ID_1783576565" CREATED="1606378818337" MODIFIED="1606378821442"/> +</node> +<node TEXT="using Fresh List" FOLDED="true" ID="ID_699752428" CREATED="1606378801731" MODIFIED="1606378808475"> +<node TEXT="on 4" ID="ID_413592226" CREATED="1606378827030" MODIFIED="1606378829422"/> +</node> +</node> +<node TEXT="anaysis" FOLDED="true" ID="ID_1520622758" CREATED="1606378844704" MODIFIED="1606378848322"> +<node TEXT="computation time" FOLDED="true" ID="ID_471167918" CREATED="1606378848322" MODIFIED="1606378857868"> +<node TEXT="overhead" ID="ID_1271917563" CREATED="1606728089529" MODIFIED="1606728094180"/> +</node> +<node TEXT="static and dynamic" ID="ID_913962071" CREATED="1606378865355" MODIFIED="1606378869923"/> +<node TEXT="abstract and concrete" ID="ID_1135285650" CREATED="1606378872154" MODIFIED="1606378879318"/> +<node TEXT="data type with proof" ID="ID_615335887" CREATED="1606378885692" MODIFIED="1606378890266"/> +<node TEXT="agda programming tech" ID="ID_490445683" CREATED="1606727991341" MODIFIED="1606728003312"/> +</node> +</node> +</node> +</map>
--- a/galois-prosym.ind Fri Dec 04 07:07:19 2020 +0900 +++ b/galois-prosym.ind Thu Jan 07 13:28:35 2021 +0900 @@ -1,4 +1,4 @@ --title: Agda によるガロア理論 +-title: AgdaによるGalois理論のプログラミング --All connected @@ -6,7 +6,7 @@ 群の要素の数え上げなどを直接に実行できる。この時に「正しく数え上げのか」ということが問題になる。4色問題が計算機を使って解かれた 時にも検算\cite{4color}が問題になった。 -Agdaは Curry Howard 対応に基づく定理証明を行う。命題が型であり証明がλ項に対応する。つまり、Agdaは証明を変数の値として持ち歩くことが +Agda\cite{AgdaWiki}は Curry Howard 対応に基づく定理証明を行う。命題が型であり証明がλ項に対応する。つまり、Agdaは証明を変数の値として持ち歩くことが できる。つまり、今計算している値だけでなく、その値の性質(5より小さいとか)、そして、その由来(何から作られたのか)を値として 持ち歩くことができる。 計算結果が、ちゃんと要求された証明につなかっていることを示すことが可能である。つまり計算だけなくて、証明としてちゃんとつながっていることになる。 @@ -335,10 +335,15 @@ --5次対称群 -abc はpinsなどで定義できる。5次の中の3次なので二つ空き場所がある。それを不等式で指定する。不等式なのはFinを指定するのに便利だからである。 +abc はpinsなどで定義できる。 + + --- 1 ∷ 2 ∷ 0 ∷ [] abc + 3rot : Permutation 3 3 + 3rot = pid {3} ∘ₚ pins (n≤ 2) + +5次の中の3次なので二つ空き場所がある。それを不等式で指定する。不等式なのはFinを指定するのに便利だからである。 abc : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 - abc i<3 j<4 = ins2 3rot i<3 j<4 これを交換子から生成してやればよい。{\tt [ dba , aec ]} なのだが、場所を正確に指定する必要がある。 @@ -353,23 +358,44 @@ [ ins2 (rot ∘ₚ rot) (fin≤n {3} dba0<3) (fin≤n {4} dba1<4) , ins2 (rot ∘ₚ rot) (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ] -これをすべての場所に付いて record を作成する。これがすべての組み合せについて記述される。10行程度である。 +これをすべての場所に付いて record を作成する。これがすべての組み合せについて記述される。図\ref{fig:3s}の10行程度である 中の値は自分で計算する必要がある。 +\begin{figure*}[tb] + open Triple triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 3rot - triple z≤n z≤n = - record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 - ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - triple z≤n (s≤s z≤n) = - record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 - ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - .... + triple z≤n z≤n = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple z≤n (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple z≤n (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + triple z≤n (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl } + triple (s≤s z≤n) z≤n = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 3 ; aec1<4 = # 1 ; abc= = pleq _ _ refl } + triple (s≤s z≤n) (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 3 ; aec1<4 = # 1 ; abc= = pleq _ _ refl } + triple (s≤s z≤n) (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + triple (s≤s z≤n) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 0 ; dba1<4 = # 3 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple (s≤s z≤n) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s z≤n)) z≤n = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s z≤n)) (s≤s z≤n) = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s z≤n)) (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 0 ; dba1<4 = # 3 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s (s≤s z≤n))) z≤n = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s (s≤s z≤n))) (s≤s z≤n) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s z≤n)) = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) = + record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } +\caption{5次対称群のめんどくさい計算の半分} +\label{fig:5s} +\end{figure*} -これだけでは閉じてなくて、もう一種類必要になる。 +これだけでは閉じてなくて、もう一種類必要になる。3次の置換には右回転と左回転があり、右回転は左回転の交換子で作るためである。 +この対称性は置換のレベルでもFL nのレベルでも自明には見えない。なので、別々に手計算する必要がある。 - dba-triple : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → Triple i<3 j<4 (3rot ∘ₚ 3rot ) + dba-triple : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) + → Triple i<3 j<4 (3rot ∘ₚ 3rot ) -つまり、5次対称群の中で3次の置換は二種類にわかれて存在していて、それらが交互に交換子を生成するようになっている。 +5次対称群の中で3次の置換は二種類にわかれて存在していて、それらが交互に交換子を生成するようになっている。 dervie-any-3rot0 : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → deriving n (abc i<3 j<4 ) @@ -380,32 +406,38 @@ このチェックにも時間はかかるが、3次対称群ほどではない。 -しかし、この方法では 4次対称群の可解性を示すのは厳しい。そこで、Sorted List である Fresh List を使う。 +しかし、この方法では 4次対称群の可解性を示すのは厳しい。そこで、Sorted List である Fresh List \cite{Coquand2002}を使う。 + +<center><img src="fig/fresh.pdf"></center> --Fresh List 各要素の大小関係がすべて入っている sort された List 。これを使うと重複要素を排除できる。 -<center><img src="fig/fresh.pdf"></center> + module _ {a} (A : Set a) (R : Rel A r) where - data List# : Set (a ⊔ r) - fresh : (a : A) (as : List#) → Set r + data List# : Set (a ⊔ r) + fresh : (a : A) (as : List#) → Set r - data List# where - [] : List# - cons : (a : A) (as : List#) → fresh a as → List# + data List# where + [] : List# + cons : (a : A) (as : List#) → fresh a as → List# - infixr 5 _∷#_ - pattern _∷#_ x xs = cons x xs _ + infixr 5 _∷#_ + pattern _∷#_ x xs = cons x xs _ - fresh a [] = ⊤ - fresh a (x ∷# xs) = R a x × fresh a xs + fresh a [] = ⊤ + fresh a (x ∷# xs) = R a x × fresh a xs + +% もう少し説明する これを使うと FList : {n : ℕ } → Set FList {n} = List# (FL n) ⌊ _f<?_ ⌋ +% ⌊ _f<?_ ⌋ を説明する + fr1 : FList fr1 = ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷# @@ -564,14 +596,16 @@ CommSolved : (x : Permutation n n) → (y : FList n) → y ≡ FL0 ∷# [] → (FL→perm (FL0 {n}) =p= pid ) → Any (perm→FL x ≡_) y → x =p= pid - CommSolved x .(cons FL0 [] (Level.lift tt)) refl eq0 (here eq) = FLpid _ eq eq0 + CommSolved x .(cons FL0 [] (Level.lift tt)) refl eq0 (here eq) + = FLpid _ eq eq0 stage3FList : CommFListN 3 2 ≡ cons (zero :: zero :: zero :: f0) [] (Level.lift tt) stage3FList = refl solved1 : (x : Permutation 3 3) → deriving 2 x → x =p= pid - solved1 x dr = CommSolved 3 x ( CommFListN 3 2 ) stage3FList p0id solved2 where + solved1 x dr = CommSolved 3 x ( CommFListN 3 2 ) + stage3FList p0id solved2 where solved2 : Any (perm→FL x ≡_) ( CommFListN 3 2 ) solved2 = CommStage→ 3 2 x dr @@ -590,6 +624,10 @@ agda sym4.agda 9.38s user 0.37s system 99% cpu 9.784 total agda sym5.agda 9.04s user 0.34s system 99% cpu 9.427 total +sym5 を実際に計算して反例を探すこともできるのだが、型検査時の実行では停止を確認できなかった。しかし、 +Agda には Haskell 経由で実行バイナリを生成する機能があり、それを用いれば瞬時に計算は終わる。 + + ./sym5n 0.00s user 0.01s system 37% cpu 0.044 total --Agdaの証明付きコード @@ -608,7 +646,8 @@ (Level.lift tt , Level.lift tt)) (Level.lift tt , Level.lift tt , Level.lift tt) -のような形になる。これは実行時に生成されてしまう。 これはオーバヘッドになる。 +のような形になる。これは実行時に生成されてしまう。 これはオーバヘッドになる。ただし、sym5n のようにコンパイルしてしまえば、使われない部分 +は計算/生成されない可能性がある。なので実行時のオーバヘッドはほとんどないかも知れない。 証明自体は線形挿入でもかなりめんどうでプログラミングの手間に見合うとは思えない。しかし、ライブラリは重要なので、その手間に見合う可能性も ある。また、証明自体は大半の証明は簡単なので機械学習が使える可能性が高い。 @@ -633,6 +672,11 @@ すべて持っているということになっている。 CommStage→ を示す時に使った可換性は Any が自然変換であることを意味している。この部分は 証明なので実際の計算には関係ない。しかし、その部分では圏論的なアプローチが有効かも知れない。 +コンパイルにより高速に計算が実行されるのは良いが、それを証明時、つまり型検査時に使用することは現状ではできない。Agda は +型検査結果を .agdai ファイルに取っておくので、実行時の結果を .agdai に埋め込む方法が考えられる。そのためには、都合良く +計算を引き伸ばすような実装が必要になる。 + + --終わりに Agda による対称群の可解性についての証明を行った。手計算では入力と検査時間がかかるが、Fresh List のような証明付きデータ構造を @@ -640,12 +684,16 @@ しかし、それにより Any のように、Fresh List に必要なものが全部入っていることを確認することができ、それをそのまま証明に使う ことがきる。これにより、計算結果を直接に証明で使うことができるようになる。 +五次対称群が可解群でない計算は FList を使ってない。deriving が不動点になるなら機械的にFListで証明できる。しかし、それは +非可解であることの説明にはならない。abc が他の置換の交換子として表されるという理由はそこからは出てこない。 + この例はプログラムの正しさを直接に証明としてコードに埋め込んだ例になっている。 +Agda による証明は\cite{galois-kono-github}で見ることができる。 + -
--- a/info.txt Fri Dec 04 07:07:19 2020 +0900 +++ b/info.txt Thu Jan 07 13:28:35 2021 +0900 @@ -1,8 +1,8 @@ -論文タイトル： Agda 上でのZF集合論の構成 +論文タイトル： AgdaによるGalois理論のプログラミング -論文タイトル英語： Constructing a model of ZF Set Theory on Agda +論文タイトル英語： Programming Galois Theory in Agda -キーワード： Agda Set-Theory Proof +キーワード： Agda Galois Proof 著者名： 河野真治 @@ -16,14 +16,13 @@ Agda は省略可能な型変数を持つ純関数型言語であり、カーリーハワード対応に基づく証明支援系として使うことができる。 数学的な命題は型として記述され、その証明は型を実現するλ項として記述される。 -ここでは直観主義論理に適した非構成的な仮定を -導入し、ZFC集合論の公理を証明する。集合はデータ構造である順序数上の述語(Ordinal definable)として導入する。 +ここではガロア理論の対称群の可解性について証明を行ない、証明付きのデータ構造の有効性を確認した。 論文抄録英語（英語論文の場合）： -Agda is pure fuctional langauge with implicit type variables, which can be used as a proof assistant system. -Methematical concepts are described as types and proofs are described as lambda terms. -In this paper, we show the validity of ZFC Set Thoeroy on a Mathematical model on Agda with non-constructive assumptions, -Sets are defined as an equation on Ordinal numbers which is called Ordinal definables. +Agda is pure functional language with implicit type variables, which can be used as a proof assistant system. +Mathematical concepts are described as types and proofs are described as lambda terms. +In this paper, we show the solvablity of symmetric group in Galois Theory. Effectiveness of Data structure with Proof is +demonstrated.
--- a/main.tex Fri Dec 04 07:07:19 2020 +0900 +++ b/main.tex Thu Jan 07 13:28:35 2021 +0900 @@ -4,7 +4,7 @@ \usepackage{graphicx} \usepackage{float} \restylefloat{figue} -\pagestyle{empty} +\pagestyle{empty} %\hoffset -1in \addtolength{\hoffset}{20mm} %\voffset -1in \addtolength{\voffset}{20mm} @@ -45,6 +45,7 @@ } \maketitle{} +\thispagestyle{empty} % to erase first page number \begin{abstract} \input{abstract} \end{abstract}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/presen.ind Thu Jan 07 13:28:35 2021 +0900 @@ -0,0 +1,74 @@ +-title: AgdaによるGalois理論のプログラミング + +--motivation + agda say prove all of it + proof carrying data structure +--all connected + not only the result + the result is proved to be correct +--What are you computing? +--Galois theory +--Galois theory : polynominal equation +--Galois theory : symmetric group on solutions +--Galois theory : group mapping +--Galois theory : commutator +--Galois theory : commutator group +--Galois theory : solvable +--proof in math text book +--formalization in agda +--Agda : lambda +--Agda : data +--Agda : record +--Agda : unification + equation +--Galois theory i nAgda : Commutator +--Galois theory in Agda : Set valued function +--Galois theory in Agda : Solvable +--Galois theory in Agda : Symmetric group +--Permutation : Data.Fin +--Permutation : Bijection +--Permutation : List +--Permutation : FL +--Proofs : 2 +--Proofs : Injection +--Proofs : 3 +--Proofs : 5 + +--A list contains everything + sorted + any +--Fresh List + Set valued function + proof carrying data structure +--Fresh List : Any + here + there +--Fresh List : Insert +--Fresh List : Property on Insert / Cons + +Any + +--Proofs : 2 +--Proofs : 3 +--Proofs : 5 + two sym 3 +--Proofs : 4 +--Proofs : 5 + compilation +--Analysis +--Analysis : overhead of proof carrying data structure + type + heap + product + type check + compiled +--Analysis connection of computation and type + +--Appendix : ZF fix + od max + Set and Class +--Appendix : Topology + Tychonov + +--Appendix : ZF + cohen model