Apr 23, 2009 The files in this directory are part of the article "The critical renormalization fixed point for commuting pairs of area-preserving maps" by G. Arioli and H. Koch. They contain the details of the proofs of Proposition 4.2 and Lemma 5.1, written in the programming language Ada95. The strategy and structure of the proofs is described in Section 7. A short discussion of the main program is given below. Some of the programs are purely numerical, producing approximate solutions for certain equations that are used later in the proof. The proof itself is divided into declarations (definitions), procedures and functions (lemmas), and main programs (theorems). This includes the declaration of data types (Ball, Taylor2, Fun, ...) that correspond to the standard sets described in Section 7. Procedures and functions that are centered around a given data type are organized into Packages ======== package (name) declaration (file) body (file) --------------------------------------------------- Balls balls.ads balls.adb Funs2 funs2.ads funs2.adb Funs2.Num funs2-num.ads funs2-num.adb Ints ints.ads ints.adb Ints.IO ints-io.ads ints-io.adb Messages messages.ads messages.adb MiniFuns minifuns.ads minifuns.adb MiniFuns.Ops minifuns-ops.ads minifuns-ops.adb Numerics numerics.ads numerics.adb NumFuns2 numfuns2.ads Reps reps.ads reps.adb Reps.IO reps-io.ads reps-io.adb Reps.Ops reps-ops.ads reps-ops.adb RG rg.ads rg.adb RGParam rgparam.ads Rounding rounding.ads rounding.adb ScalVectors scalvectors.ads scalvectors.adb ScalVectors.Ops scalvectors-ops.ads scalvectors-ops.adb Taylors2 taylors2.ads taylors2.adb Taylors2.Num taylors2-num.ads taylors2-num.adb Vectors vectors.ads vectors.adb Zeros zeros.ads zeros.adb Separate procedures and/or Programs =================================== procedure (name) body (file) comment ----------------------------------------------- CheckDM checkdm.adb check contraction CheckFix checkfix.adb check approx fixed point etc CheckMaps checkmaps.adb check map domains/ranges IterRG iterrg.adb # MakeMatrix makematrix.adb # ShowFun showfun .adb # Verify verify.adb main program The procedures (#) are purely numerical and not part of the proof. They have been used to create the input data and can be used for further experimentation. Verify just runs CheckFix, CheckDM, CheckMaps. These three programs can also be run individually, first CheckFix, then CheckDM and CheckMaps (any order). Data ==== file comment --------------------------- gapprox.data the approximate fixed point matrix30.data contraction matrix vapprox.data approximate midpoint function Other files =========== file comment --------------------------- modify_fp_env.c needed if rounding_libc.adb is used README this file rounding_asm.ads * (same as rounding.ads) rounding_asm.adb * (same as rounding.adb) rounding_libc.ads * (rename to rounding.ads if needed) rounding_libc.adb * (rename to rounding.adb if needed) rounding_libm.ads * (rename to rounding.ads if needed) rounding_libm.adb * (rename to rounding.adb if needed) verify.log output of the main program "Verify" The files (*) are described below. Portability =========== Floating point type ------------------- The type Rep is defined in reps.ads as Long_Long_Float. This type is specific to the gnat compiler. It implements the IEEE 754 Extended 80 bit (64 bit mantissa) floating point format. It is possible to change Long_Long_Float to the more standard Long_Float (e.g. when using other compilers), and the proof will still run, but the bounds on lambda and mu will not be as good as described in Theorem 1.1. Rounding -------- Currently, rounding can be controlled only in a way that depends on the platform (hardware or operating system). The default version of the package Rounding (in rounding.ads/rounding.adb) will work on most machines. The files (*) above contain alternative versions of the package Rounding. To use e.g. the libm version, make rounding.ads/rounding.adb copies of the files rounding_libm.ads/rounding_libm.adb The current (default) versions of rounding.ads/rounding.adb are copies of rounding_asm.ads/rounding_asm.adb The procedures in rounding.ads/rounding.adb use (two lines of) assembly code for the x86/x87 processors. The procedure Asm that is used for this is gnat specific, but other compilers have functionally equivalent procedures that can be substituted for Asm. The procedures in rounding_libc.ads/rounding_libc.adb use a small C program (modify_fp_env.c) which calls libc functions to switch rounding modes. This version should be the most portable. The procedures in rounding_libm.ads/rounding_libm.adb use libc and libm functions; three constants are x87 specific and will have to be changed for use with other processors. This version works e.g. with the Aonix ObjectAda compiler. Compilation with gnat ===================== The current version is compiled simply by typing gnatmake verify To use rounding_libm.ads/rounding_libm.adb, first rename these files to rounding.ads/rounding.adb. Then type gnatmake -c verify.adb gnatbind verify.ali gnatlink -lm verify.ali To use rounding_libc.ads/rounding_libc.adb, first rename these files to rounding.ads/rounding.adb. Then type gnatgcc -c modify_fp_env.c gnatmake -c verify.adb gnatbind verify.ali gnatlink verify.ali modify_fp_env.o The programs CheckFix, CheckDM and CheckMaps, that are used by Verify, can also be compiled/run separately. Running Verify ============== Jun run the executable file (e.g. named verify) produced by the compiler. This takes about 28 hours on current personal computers. (The less precise Long_Float version takes about 8 hours.) To help endure the wait, imagine having to do this by hand. Or set "Verbosity := 3" in checkfix.adb, checkdm.adb, checkmaps.adb