Skip to content

Latest commit

 

History

History
93 lines (74 loc) · 3.84 KB

README.md

File metadata and controls

93 lines (74 loc) · 3.84 KB
Raw

Investigation of Hofstadter's G function, tree, and mirror

A Coq development by Pierre Letouzey, started in summer 2015. It now extends to a whole family of functions generalizing G, and it also considers related infinite morphic words extending the Fibonacci word.

Documentation:

Usage

  • Use make to compile the Coq files.
  • Use make gallinahtml to generate the short html documentation.
  • Use cd reports/g && pdflatex report to generate the pdf of the technical report.

Some recent files depend on Coq >= 8.16 and < 8.20 as well as external libraries Coquelicot >= 3.3.0 and QuantumLib >= 1.5.1. I advise to fetch them via opam. For instance:

opam pin add coq 8.19.2
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-coquelicot
opam pin add coq-quantumlib 1.5.1

Summary of files:

  1. Auxiliary
  • More*.v : additions to the various libraries used.
  • Approx.v: lightweight interval arithmetic for bounding reals by Q
  • DeltaList.v: lists of natural numbers with constrained differences
  1. Old files specialized to function G
  • Fib.v: Fibonacci sequence and decomposition
  • FunG.v: Hofstadter's G function and tree
  • FunG_prog.v: Alternative definition of Hofstadter's G function
  • FlipG.v: Hofstadter's flipped G tree
  • Phi.v: Hofstadter G function and the golden ratio
  1. New, generalized versions of G with more nested recursive calls
  • GenFib.v: Fibonacci-like sequences A q and decomposition
  • GenG.v: Hofstadter's G-like functions f q
  • GenFlip.v: Mirror of the G-like trees
  • GenAdd.v: Study of the quasi-additivity of G-like functions
  • Shift.v: quasi-reciprocal of the G-like functions
  1. Some infinite morphic words related to functions f q
  • Words.v: morphic words kseq k, first properties, link with f q.
  • WordGrowth.v: compare some letter frequencies, f q <= f (q+1)
  • WordSuffix.v: enumerate and count the kword suffixes
  • WordFactor.v: factors of kseq k (i.e. finite sub-words)
  • Special.v: unique left special factor for kseq q, complexity
  1. Hoftadter G-like functions and real numbers
  • ThePoly.v: start studying polynomial X^(q+1)-X^q-1
  • Mu.v: real roots of this polynomial
  • Freq.v: frequencies of letters in qseq q, limit of (f q n)/n.
  • LimCase2.v: Hofstadter H (i.e. f 2) at dist <1 of n*τ_2
  • LimCase3.v: f 3 at dist <2 of n*τ_3
  • LimCase4.v: f 4 at unbounded dist of n*τ_4
  1. A companion Coq file for a forthcoming article

References:

License

The documents in all subdirectories (especially reports/ talks/ poster/) are released under the CC-BY 4.0 license, see http://creativecommons.org/licenses/by/4.0/.

The Coq files of this development are released in the Public Domain, see the LICENSE file in the current directory.