From ffdf33c10a5ccfc5a19021d45764094a6b1bec30 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 24 Oct 2024 11:05:59 -0400 Subject: [PATCH] Move OEIS to literature (#1208) This PR moves the OEIS module to the literature --- references.bib | 10 ++- .../ackermann-function.lagda.md | 25 ++++-- .../euclid-mullin-sequence.lagda.md | 4 +- .../fermat-numbers.lagda.md | 2 +- src/literature.lagda.md | 3 +- .../oeis.lagda.md | 86 ++++++++----------- ...encyclopedia-of-integer-sequences.lagda.md | 9 -- 7 files changed, 68 insertions(+), 71 deletions(-) rename src/{online-encyclopedia-of-integer-sequences => literature}/oeis.lagda.md (60%) delete mode 100644 src/online-encyclopedia-of-integer-sequences.lagda.md diff --git a/references.bib b/references.bib index 548ba2d0b5..d709f0c64f 100644 --- a/references.bib +++ b/references.bib @@ -488,10 +488,12 @@ @misc{Mye21 primaryclass = {math.CT} } -@online{OEIS, - title = {The {{On-Line Encyclopedia}} of {{Integer Sequences}} ({{OEIS}})}, - organization = {{{OEIS}} Foundation Inc.}, - url = {https://oeis.org/} +@online{oeis, + title = {The {{On-Line Encyclopedia}} of {{Integer Sequences}}}, + author = {OEIS Foundation Inc.}, + date = {1996}, + url = {https://oeis.org}, + howpublished = {website}, } @book{Rie17, diff --git a/src/elementary-number-theory/ackermann-function.lagda.md b/src/elementary-number-theory/ackermann-function.lagda.md index be5add2d11..05c34bda2a 100644 --- a/src/elementary-number-theory/ackermann-function.lagda.md +++ b/src/elementary-number-theory/ackermann-function.lagda.md @@ -15,14 +15,27 @@ open import elementary-number-theory.natural-numbers ## Idea The -{{#concept "Ackermann function" WD="Ackermann function" WDID=Q341835 Agda=ackermann}} -is a fast growing binary operation on the natural numbers. +{{#concept "Ackermann-Péter function" WD="Ackermann function" WDID=Q341835 Agda=ackermann-péter-ℕ}} +is a fast growing binary operation on the +[natural numbers](elementary-number-theory.natural-numbers.md). ## Definition +### The Ackermann-Péter function + +```agda +ackermann-péter-ℕ : ℕ → ℕ → ℕ +ackermann-péter-ℕ zero-ℕ n = + succ-ℕ n +ackermann-péter-ℕ (succ-ℕ m) zero-ℕ = + ackermann-péter-ℕ m 1 +ackermann-péter-ℕ (succ-ℕ m) (succ-ℕ n) = + ackermann-péter-ℕ m (ackermann-péter-ℕ (succ-ℕ m) n) +``` + +### The simplified Ackermann function + ```agda -ackermann : ℕ → ℕ → ℕ -ackermann zero-ℕ n = succ-ℕ n -ackermann (succ-ℕ m) zero-ℕ = ackermann m 1 -ackermann (succ-ℕ m) (succ-ℕ n) = ackermann m (ackermann (succ-ℕ m) n) +simplified-ackermann-ℕ : ℕ → ℕ +simplified-ackermann-ℕ n = ackermann-péter-ℕ n n ``` diff --git a/src/elementary-number-theory/euclid-mullin-sequence.lagda.md b/src/elementary-number-theory/euclid-mullin-sequence.lagda.md index 42a51f3d3a..363b26e655 100644 --- a/src/elementary-number-theory/euclid-mullin-sequence.lagda.md +++ b/src/elementary-number-theory/euclid-mullin-sequence.lagda.md @@ -36,8 +36,8 @@ by euclid-mullin-ℕ 0 := 2, ``` -and `euclid-mullin-ℕ (n + 1)` is the least [prime -factor](elementary-number-theory.prime numbers.md) of the product of all +and `euclid-mullin-ℕ (n + 1)` is the least +[prime factor](elementary-number-theory.prime-numbers.md) of the product of all previous entries in the Euclid–Mullin sequence plus one. ## Definitions diff --git a/src/elementary-number-theory/fermat-numbers.lagda.md b/src/elementary-number-theory/fermat-numbers.lagda.md index 25be74d35c..8a76e9fc21 100644 --- a/src/elementary-number-theory/fermat-numbers.lagda.md +++ b/src/elementary-number-theory/fermat-numbers.lagda.md @@ -28,7 +28,7 @@ are numbers of the form $F_n := 2^{2^n}+1$. The first five Fermat numbers are ``` The sequence of Fermat numbers is listed as A000215 in the -[Online Encyclopedia of Integer Sequences](online-encyclopedia-of-integer-sequences.oeis.md). +[Online Encyclopedia of Integer Sequences](literature.oeis.md). Alternatively, the Fermat numbers can be defined with [strong induction](elementary-number-theory.strong-induction-natural-numbers.md) diff --git a/src/literature.lagda.md b/src/literature.lagda.md index 2127b478fa..2164beb6a2 100644 --- a/src/literature.lagda.md +++ b/src/literature.lagda.md @@ -11,10 +11,11 @@ module literature where open import literature.100-theorems public open import literature.idempotents-in-intensional-type-theory public +open import literature.oeis public open import literature.sequential-colimits-in-homotopy-type-theory public ``` ## References {{#bibliography}} {{#reference SvDR20}} {{#reference Shu17}} -{{#reference 100theorems}} +{{#reference 100theorems}} {{#reference oeis}} diff --git a/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md b/src/literature/oeis.lagda.md similarity index 60% rename from src/online-encyclopedia-of-integer-sequences/oeis.lagda.md rename to src/literature/oeis.lagda.md index 59bb1d5c1a..5ee125ff2e 100644 --- a/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md +++ b/src/literature/oeis.lagda.md @@ -1,33 +1,19 @@ # Sequences of the online encyclopedia of integer sequences +This file records formalized sequences of the +[Online Encyclopedia of Integer Sequences](https://oeis.org) {{#cite oeis}}. + ```agda -module online-encyclopedia-of-integer-sequences.oeis where +module literature.oeis where ```
Imports ```agda -open import elementary-number-theory.ackermann-function -open import elementary-number-theory.catalan-numbers -open import elementary-number-theory.cofibonacci -open import elementary-number-theory.collatz-bijection -open import elementary-number-theory.euclid-mullin-sequence -open import elementary-number-theory.eulers-totient-function open import elementary-number-theory.exponentiation-natural-numbers -open import elementary-number-theory.factorials -open import elementary-number-theory.fermat-numbers -open import elementary-number-theory.fibonacci-sequence -open import elementary-number-theory.infinitude-of-primes -open import elementary-number-theory.kolakoski-sequence -open import elementary-number-theory.multiset-coefficients open import elementary-number-theory.natural-numbers -open import elementary-number-theory.pisano-periods - -open import finite-group-theory.finite-groups open import foundation.function-types - -open import univalent-combinatorics.main-classes-of-latin-squares ```
@@ -37,15 +23,15 @@ open import univalent-combinatorics.main-classes-of-latin-squares ### [A000001](https://oeis.org/A000001) The number of groups of order `n` ```agda -A000001 : ℕ → ℕ -A000001 = number-of-groups-of-order +open import finite-group-theory.finite-groups using + ( number-of-groups-of-order) ``` ### [A000002](https://oeis.org/A000002) The Kolakoski sequence ```agda -A000002 : ℕ → ℕ -A000002 = kolakoski +open import elementary-number-theory.kolakoski-sequence using + ( kolakoski) ``` ### [A000004](https://oeis.org/A000004) The zero sequence @@ -66,8 +52,8 @@ A000007 (succ-ℕ _) = 0 ### [A000010](https://oeis.org/A000010) Euler's totient function ```agda -A000010 : ℕ → ℕ -A000010 = eulers-totient-function-relatively-prime +open import elementary-number-theory.eulers-totient-function using + ( eulers-totient-function-relatively-prime) ``` ### [A000012](https://oeis.org/A000012) All 1's sequence @@ -87,15 +73,15 @@ A000027 = succ-ℕ ### [A000040](https://oeis.org/A000040) The prime numbers ```agda -A000040 : ℕ → ℕ -A000040 = prime-ℕ +open import elementary-number-theory.infinitude-of-primes using + ( prime-ℕ) ``` ### [A000045](https://oeis.org/A000045) The Fibonacci sequence ```agda -A000045 : ℕ → ℕ -A000045 = Fibonacci-ℕ +open import elementary-number-theory.fibonacci-sequence using + ( Fibonacci-ℕ) ``` ### [A000079](https://oeis.org/A000079) Powers of `2` @@ -108,22 +94,22 @@ A000079 = exp-ℕ 2 ### [A000108](https://oeis.org/A000108) The Catalan numbers ```agda -A000108 : ℕ → ℕ -A000108 = catalan-numbers +open import elementary-number-theory.catalan-numbers using + ( catalan-numbers) ``` ### [A000142](https://oeis.org/A000142) Factorials ```agda -A000142 : ℕ → ℕ -A000142 = factorial-ℕ +open import elementary-number-theory.factorials using + ( factorial-ℕ) ``` ### [A000215](https://oeis.org/A000215) The Fermat numbers ```agda -A000215 : ℕ → ℕ -A000215 = fermat-number-ℕ +open import elementary-number-theory.fermat-numbers using + ( fermat-number-ℕ) ``` ### [A000244](https://oeis.org/A000244) Powers of `3` @@ -136,29 +122,29 @@ A000244 = exp-ℕ 3 ### [A000720](https://oeis.org/A000720) The prime counting function ```agda -A000720 : ℕ → ℕ -A000720 = prime-counting-ℕ +open import elementary-number-theory.infinitude-of-primes using + ( prime-counting-ℕ) ``` ### [A000945](https://oeis.org/A000945) The Euclid–Mullin sequence ```agda -A000945 : ℕ → ℕ -A000945 = euclid-mullin-ℕ +open import elementary-number-theory.euclid-mullin-sequence using + ( euclid-mullin-ℕ) ``` ### [A001175](https://oeis.org/A001175) Pisano periods ```agda -A001175 : ℕ → ℕ -A001175 = pisano-period +open import elementary-number-theory.pisano-periods using + ( pisano-period) ``` ### [A001177](https://oeis.org/A001177) The cofibonacci sequence ```agda -A001177 : ℕ → ℕ -A001177 = cofibonacci +open import elementary-number-theory.cofibonacci using + ( cofibonacci) ``` ### [A001477](https://oeis.org/A001477) The natural numbers @@ -171,20 +157,24 @@ A001477 = id ### [A003090](https://oeis.org/A003090) The number of main classes of Latin squares of order `n` ```agda -A003090 : ℕ → ℕ -A003090 = number-of-main-classes-of-Latin-squares-of-order +open import univalent-combinatorics.main-classes-of-latin-squares using + ( number-of-main-classes-of-Latin-squares-of-order) ``` ### [A006369](https://oeis.org/A006369) Collatz' bijection ```agda -A006369 : ℕ → ℕ -A006369 = map-collatz-bijection +open import elementary-number-theory.collatz-bijection using + ( map-collatz-bijection) ``` ### [A046859](https://oeis.org/A046859) The main diagonal of the Ackermann–Péter function ```agda -A046859 : ℕ → ℕ -A046859 n = ackermann n n +open import elementary-number-theory.ackermann-function using + ( simplified-ackermann-ℕ) ``` + +## References + +{{#bibliography}} diff --git a/src/online-encyclopedia-of-integer-sequences.lagda.md b/src/online-encyclopedia-of-integer-sequences.lagda.md deleted file mode 100644 index 697e4582db..0000000000 --- a/src/online-encyclopedia-of-integer-sequences.lagda.md +++ /dev/null @@ -1,9 +0,0 @@ -# Online encyclopedia of integer sequences - -## Modules in the OEIS namespace - -```agda -module online-encyclopedia-of-integer-sequences where - -open import online-encyclopedia-of-integer-sequences.oeis public -```