diff options
| -rw-r--r-- | .github/workflows/pull.yml | 24 | ||||
| -rw-r--r-- | bin/checkPeople.js | 36 | ||||
| -rw-r--r-- | entries/fbanados/fib.st | 8 | ||||
| -rw-r--r-- | entries/fbanados/fib.v | 90 | ||||
| -rw-r--r-- | entries/laelath/fib.bf | 3 | ||||
| -rw-r--r-- | entries/nritschel/assets/scratch.png | bin | 0 -> 752302 bytes | |||
| -rw-r--r-- | entries/nritschel/scratch/README.md | 1 | ||||
| -rw-r--r-- | entries/nritschel/scratch/fib.sb3 | bin | 0 -> 43364 bytes | |||
| -rw-r--r-- | entries/nritschel/xlsx/fib.xlsx | bin | 0 -> 11704 bytes | |||
| -rw-r--r-- | entries/nxjfxu/fib.hs | 5 | ||||
| -rw-r--r-- | entries/pkoronkevich/tex/README.md | 1 | ||||
| -rw-r--r-- | entries/pkoronkevich/tex/fib.tex | 29 | ||||
| -rw-r--r-- | entries/pkoronkevich/tex/render.pdf | bin | 0 -> 21807 bytes | |||
| -rw-r--r-- | entries/pkoronkevich/tex/render.png | bin | 0 -> 387387 bytes | |||
| -rw-r--r-- | entries/zgrannan/Fib.hs | 18 | ||||
| -rw-r--r-- | people.json | 67 |
16 files changed, 282 insertions, 0 deletions
diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml new file mode 100644 index 0000000..266b8f8 --- /dev/null +++ b/.github/workflows/pull.yml @@ -0,0 +1,24 @@ +name: Check people + +on: + pull_request: + branches: + - main + workflow_dispatch: + +jobs: + build: + runs-on: ubuntu-latest + + strategy: + matrix: + node: [ 16.x ] + + steps: + - uses: actions/checkout@v2 + - name: Install modules with Node ${{ matrix.node }} + uses: actions/setup-node@v1 + with: + node-version: ${{ matrix.node }} + - name: Check people + run: node bin/checkPeople.js ${{ github.actor }} diff --git a/bin/checkPeople.js b/bin/checkPeople.js new file mode 100644 index 0000000..3c564a4 --- /dev/null +++ b/bin/checkPeople.js @@ -0,0 +1,36 @@ +const fs = require("fs"); + +const PEOPLE_PATH = "./people.json"; + +const [actor] = process.argv.slice(2); + +console.log(`Triggered by ${actor}`); + +if (!fs.existsSync(PEOPLE_PATH)) { + throw "No people file found"; +} + +let people; +try { + people = JSON.parse(fs.readFileSync(PEOPLE_PATH)); +} catch (err) { + throw "Could not read people.json as JSON"; +} + +const person = people.find(person => person.github === actor); +if (!person) { + throw `${actor} isn't in people.json!`; +} + +if (!(person.entries && person.entries.length > 0)) { + throw `${actor} is missing entries!`; +} + +for (const entry of person.entries) { + const {link} = entry; + if (!(link.startsWith("http") || fs.existsSync(link))) { + throw `${link} not found!`; + } +} + +console.log("Checked!"); diff --git a/entries/fbanados/fib.st b/entries/fbanados/fib.st new file mode 100644 index 0000000..099407c --- /dev/null +++ b/entries/fbanados/fib.st @@ -0,0 +1,8 @@ +'From Pharo10.0.0 of 15 June 2022 [Build information: Pharo-10.0.0+build.521.sha.14f541319d443f4261f84f4fa19fbb34460a5edb (64 Bit)] on 24 October 2022 at 11:26:20.436554 am'! + +!Integer methodsFor: '*Fibonacci' stamp: 'FelipeBanados 10/24/2022 11:13'! +fibonacciNumber + self <= 2 ifTrue: [ ^ 1 ]. + ^ (self - 1) fibonacciNumber + (self - 2) fibonacciNumber. + +! ! diff --git a/entries/fbanados/fib.v b/entries/fbanados/fib.v new file mode 100644 index 0000000..e9fe796 --- /dev/null +++ b/entries/fbanados/fib.v @@ -0,0 +1,90 @@ +Require Import Coq.Arith.Wf_nat. (* import strong induction on naturals *) +Require Import Lia. (* Linear Integer Arithmetic solver *) + +(* First, simple specification *) + +Fixpoint fib_simpl (n : nat) {struct n} : nat := + match n with + | 0 => 1 + | S n => match n with + | 0 => 1 + | S m => fib_simpl n + fib_simpl m + end + end. + +Example fib_3 : (fib_simpl 2 = 2). reflexivity. Qed. +Example fib_4 : (fib_simpl 3 = 3). reflexivity. Qed. +Example fib_5 : (fib_simpl 4 = 5). reflexivity. Qed. + +Lemma fib_simpl_spec : forall n, (* useful lemma for rewriting *) + fib_simpl (S (S n)) = fib_simpl (S n) + fib_simpl n. +Proof. + destruct n. + - (* case n := 0 *) + reflexivity. + - (* case n := (S n) *) + destruct n; reflexivity. +Qed. + +(* For a (slightly) faster version *) + +Fixpoint fib_acc_aux (n : nat) (acc : nat) (prev : nat) {struct n} : nat := + match n with + | 0 => acc + prev + | S n => fib_acc_aux n (acc + prev) acc + end. + +Definition fib_faster (n : nat) : nat := + match n with + | 0 => 1 + | S n => match n with + | 0 => 1 + | S m => (fib_acc_aux m 1 1) + end + end. + +Example fib_faster_3 : (fib_faster 2 = 2). reflexivity. Qed. +Example fib_faster_4 : (fib_faster 3 = 3). reflexivity. Qed. +Example fib_faster_5 : (fib_faster 4 = 5). reflexivity. Qed. + +Lemma fib_acc_aux_rewrite : forall n a b c d, + fib_acc_aux n a c + fib_acc_aux n b d = fib_acc_aux n (a + b) (c + d). +Proof. + induction n; intros. + - (* case n := 0 *) + simpl; lia. + - (* case n := (S n) *) + simpl. + rewrite IHn. + f_equal. + lia. +Qed. + +Theorem fib_faster_spec: forall n, fib_simpl n = fib_faster n. +Proof. + induction n using lt_wf_ind. (* use strong induction *) + rename H into strong_induction_hypothesis. + destruct n. (* lt_wf_ind does not deal immediately with cases *) + - (* case n := 0 *) + reflexivity. + - (* case n := (S n) *) + destruct n. + + (* case n := 1 *) + reflexivity. + + (* case n := (S (S n)) *) + rewrite ?fib_simpl_spec. + do 2 rewrite strong_induction_hypothesis by lia. + enough (forall n, fib_faster (S n) + fib_faster n = fib_faster (S (S n))) as lemma by apply lemma. + clear. + destruct n. + * (* for lemma, case n := 0 *) + reflexivity. + * (* for lemma, case n := S n *) + destruct n. + -- (* for lemma, case n := 1 *) + reflexivity. + -- (* for lemma, case n := S (S n) *) + simpl. + apply fib_acc_aux_rewrite. +Qed. + diff --git a/entries/laelath/fib.bf b/entries/laelath/fib.bf new file mode 100644 index 0000000..ff7d67a --- /dev/null +++ b/entries/laelath/fib.bf @@ -0,0 +1,3 @@ +>101p011p&:v:-1 < + v+g11g10_11g.@ + >11g01p11p ^ diff --git a/entries/nritschel/assets/scratch.png b/entries/nritschel/assets/scratch.png Binary files differnew file mode 100644 index 0000000..5883245 --- /dev/null +++ b/entries/nritschel/assets/scratch.png diff --git a/entries/nritschel/scratch/README.md b/entries/nritschel/scratch/README.md new file mode 100644 index 0000000..e059267 --- /dev/null +++ b/entries/nritschel/scratch/README.md @@ -0,0 +1 @@ +<img src="../assets/scratch.png" alt="scratch preview">
\ No newline at end of file diff --git a/entries/nritschel/scratch/fib.sb3 b/entries/nritschel/scratch/fib.sb3 Binary files differnew file mode 100644 index 0000000..a3cf2cc --- /dev/null +++ b/entries/nritschel/scratch/fib.sb3 diff --git a/entries/nritschel/xlsx/fib.xlsx b/entries/nritschel/xlsx/fib.xlsx Binary files differnew file mode 100644 index 0000000..e1b662d --- /dev/null +++ b/entries/nritschel/xlsx/fib.xlsx diff --git a/entries/nxjfxu/fib.hs b/entries/nxjfxu/fib.hs new file mode 100644 index 0000000..0f0d871 --- /dev/null +++ b/entries/nxjfxu/fib.hs @@ -0,0 +1,5 @@ +fib :: Int -> Int +fib = (fibs !!) + where + fibs = 0 : 1 : [fibs !! (i - 2) + fibs !! (i - 1) | i <- [2..]] + diff --git a/entries/pkoronkevich/tex/README.md b/entries/pkoronkevich/tex/README.md new file mode 100644 index 0000000..225773b --- /dev/null +++ b/entries/pkoronkevich/tex/README.md @@ -0,0 +1 @@ +<img src="./render.png" alt="fib.tex preview">
\ No newline at end of file diff --git a/entries/pkoronkevich/tex/fib.tex b/entries/pkoronkevich/tex/fib.tex new file mode 100644 index 0000000..cef9138 --- /dev/null +++ b/entries/pkoronkevich/tex/fib.tex @@ -0,0 +1,29 @@ +\documentclass[11pt]{article} +\usepackage[fleqn]{amsmath} + +\newcommand{\one}{\lambda f . \lambda x . f \ x} +\newcommand{\two}{\lambda f . \lambda x . f \ (f \ x)} +\newcommand{\tru}{\lambda x . \lambda y . x} +\newcommand{\flse}{\lambda x . \lambda y . y} +\newcommand{\isz}{\lambda n . n \ (\lambda c . \flse) \ \tru} +\newcommand{\ife}{\lambda p . \lambda a . \lambda b . p \ a \ b} +\newcommand{\suc}{\lambda n . \lambda f . \lambda x . f \ (n \ f \ x)} +\newcommand{\plus}{\lambda m . \lambda n . m \ (\suc) \ n} +\newcommand{\pred}{\lambda n . \lambda f . \lambda x . n \ (\lambda g . \lambda h . h \ (g \ f)) \ (\lambda u . x) \ (\lambda u . u)} +\newcommand{\sub}{\lambda m . \lambda n . n \ (\pred) \ m} +\newcommand{\lleq}{\lambda m . \lambda n . \\ \qquad \isz \ ((\sub) \\ \qquad \ m \ n)} +\newcommand{\fix}{\lambda g . (\lambda x . g \ (x \ x)) \ (\lambda x . g \ (x \ x))} +\newcommand{\appo}[2]{#1 \ #2} +\newcommand{\appt}[3]{#1 \ #2 \ #3} + +\begin{document} +\begin{gather*} + \fix \\ % recursive function application + \quad \lambda r . \lambda n . (\ife) \\ % of fib, which takes itself and n, if expression + \quad \ \appt{(\lleq)}{n}{\one} \\ % if n less than or equal to one + \quad \ (\one) \\ % if so, return 1 + \quad \ (\plus) \\ % if not, add + \qquad \appo{r}{(\appo{(\pred)}{n})} \\ % the first recursive call, n - 1, to + \qquad \appo{r}{(\appt{(\sub)}{n}{\two})} % the second recursive call, n - 2 +\end{gather*} +\end{document} diff --git a/entries/pkoronkevich/tex/render.pdf b/entries/pkoronkevich/tex/render.pdf Binary files differnew file mode 100644 index 0000000..8ee60c7 --- /dev/null +++ b/entries/pkoronkevich/tex/render.pdf diff --git a/entries/pkoronkevich/tex/render.png b/entries/pkoronkevich/tex/render.png Binary files differnew file mode 100644 index 0000000..a1896a2 --- /dev/null +++ b/entries/pkoronkevich/tex/render.png diff --git a/entries/zgrannan/Fib.hs b/entries/zgrannan/Fib.hs new file mode 100644 index 0000000..1918fc8 --- /dev/null +++ b/entries/zgrannan/Fib.hs @@ -0,0 +1,18 @@ +-- Point-less fibonacci +fib :: Int -> Int +fib = fix fib' + where + fib' = + ap (when 0 . (0 ==)) . + ap (when 1 . (1 ==)) . + ap (ap . ((+) .) . (. subtract 1)) (. subtract 2) + + when t c e = if c then t else e + + ap mf m = mf >>= (\f -> m >>= return . f) + + fix f = f (fix f) + + +main :: IO () +main = mapM_ (print . fib) [0 .. 10] diff --git a/people.json b/people.json index bb44dde..b84c8d8 100644 --- a/people.json +++ b/people.json @@ -130,6 +130,14 @@ { "name": "fib-java", "link": "./entries/nritschel/fib-java/src" + }, + { + "name": "xlsx", + "link": "./entries/nritschel/xlsx/fib.xlsx" + }, + { + "name": "scratch", + "link": "./entries/nritschel/scratch" } ] }, @@ -198,5 +206,64 @@ "link": "https://github.com/wilbowma/fib-lang/tree/2ec2d1dfd141220882d824cf3dac5b374ed291f3" } ] + }, + { + "github": "fbanados", + "name": "Felipe Bañados Schwerter", + "title": "PhD Candidate, UBC", + "entries": [ + { + "name": "coq", + "link": "./entries/fbanados/fib.v" + }, + { + "name": "pharo-smalltalk", + "link": "./entries/fbanados/fib.st" + } + ] + }, + { + "github": "laelath", + "name": "Justin Frank", + "title": "PhD Student, UMD", + "entries": [ + { + "name": "befunge", + "link": "./entries/laelath/fib.bf" + } + ] + }, + { + "github": "nxjfxu", + "name": "Junfeng Xu", + "title": "MSc Student, UBC", + "entries": [ + { + "name": "ouroboros", + "link": "./entries/nxjfxu/fib.hs" + } + ] + }, + { + "github": "zgrannan", + "name": "Zack Grannan", + "title": "MSc Computer Science Student, UBC", + "entries": [ + { + "name": "haskell", + "link": "./entries/zgrannan/Fib.hs" + } + ] + }, + { + "github": "pkoronkevich", + "name": "Paulette Koronkevich", + "title": "PhD Student, UBC", + "entries": [ + { + "name": "tex", + "link": "./entries/pkoronkevich/tex" + } + ] } ] |
