Process journal of learning by Attila Vajda

Mini Puzzle - βˆ€, βˆƒ, normalization challenge

πŸŽΉβ›΅πŸšγ‚Έγƒ£γ‚Ί meets πŸ™TypeTheory #

Mini Puzzle: βˆ€, βˆƒ, normalization challenge

🐬 Lean4

def ιΎπŸ‰ (Ο€:β„•) : β„• := match Ο€ with
| 0     => 8
| β„•.succ 🧠 => ιΎπŸ‰ (🧠) + 3

#eval ιΎπŸ‰ 2

🐍 Python

def πŸͺ€(ζ–‡): return 8 if ζ–‡==0 else πŸͺ€(ζ–‡-1)+3
print(πŸͺ€(2))

🧊 C

int πŸ₯„(int ζ°΄){return ζ°΄==0?8:πŸ₯„(ζ°΄-1)+3;}
int main(){printf("%d",πŸ₯„(2));}

These puzzles are so cool! (in my experience)
You can see the visualisation here: https://pythontutor.com/render.html#mode=display
and learn a lot about recursion, abstract mathematics and coding

def πŸͺ€(ζ–‡): return 8 if ζ–‡==0 else πŸͺ€(ζ–‡-1)+3

These puzzles are awesome! You can learn a LOT about recursion in fact understand it powerfully perhaps, and I can now visualise the algorithm on Python tutor. So I learnt that maybe πŸͺ€(ζ–‡-1)+3 goes ζ–‡ to 0 and then adds 3 at each step returning (is returning inverse arrows? It seems like a loop, going there, and back, going there steps two arrows -1 -1, then comes back +3 +3 ! Awesome, so there is categories here.

8 is the starting point yes? A
-1

or is 2 the starting point, whatever you input?
2 ---{-1}---> 1 ---{-1}---> 0 ---{return 8}---> 8 ---{+3}---> 11 ---{+3}---> 14

Go until 0 in -1s, then turn 8, and go as many steps it took you to get to 0 from 2 in 3s.

input ⟢ base-case ⟢ return-anchor ⟢ output

n ⟢ 0  
return 8 + (n Γ— 3)

πŸ€–πŸŒΏ 🌱Recursion = journey + rebuild = fold + unfold 🧩

--βˆ€ recursion : input ⟢ base-case ⟢ return-anchor ⟢ output?

f(x) := if base(x) then anchor else step(f(prev(x)))

πŸ€–πŸŒΏ πŸ” Unfold + Refold 🧩

#recursion

I got these puzzles from ChatGPT (thanks πŸ€–),
using the espansos:

matches:
  - trigger: ":quests"
    replace: "pls show quests 🧩"

  - trigger: ":pzl-a"
    replace: "pls write puzzle to guess output, in Lean4 and a different style in Python, and another in C, with all gibberish/unicode-symbol/grapheme/kanji/greek for everything variable"

  - trigger: ":l4a-a"
    replace: "pls show the pareto quests of Lean4 architect craft, being able to build Lean4 core and mathlib4 from scratch, and refactor it with clean code practices."

  - trigger: ":100"
    replace: "pls respond in ≀ 500 characters"
  - trigger: ":300"
    replace: "pls respond in ≀ 500 characters"
  - trigger: ":500"
    replace: "pls respond in ≀ 500 characters"

Reference: #

Christian Mayer's work on code puzzles: