🦄 Lean4 Puzzle, 🐢 C Puzzle, 🐍 Python Puzzle
🦄 Lean4 Puzzle:
inductive 𝒲 where
| α : 𝒲
| β : 𝒲 → 𝒲
def 𝒮 (ζ : Type) := Unit ⊕ ζ
def φ : 𝒮 𝒲 → 𝒲
| .inl _ => 𝒲.α
| .inr z => 𝒲.β z
#eval φ (.inr (.β (.β 𝒲.α)))
❓Guess: How deep is this number in Peano steps?
🐢 C Puzzle:
typedef struct Ω {
int tag;
struct Ω* next;
} Ω;
Ω* Φ(Ω* x) {
if (!x) return NULL;
Ω* y = malloc(sizeof(Ω));
y->tag = 1;
y->next = x;
return y;
}❓Guess: How many Φ calls before NULL?
🐍 Python Puzzle:
def 𝓕(x): return ("1", None) if x is None else ("+", x)
x = 𝓕(("+", ("+", None)))
print(x[1][1])❓Guess: What does x[1][1] yield?
I find it sort of fun, that this is a number, because it doesn't look like a number:
inductive 𝒲 where
| α : 𝒲
| β : 𝒲 → 𝒲
✨ Keep puzzling! Every function is a tiny theorem you can prove or refactor — functional code is mathematical art. 🎨🐙
𝒮 𝒲 := Unit ⊕ 𝒲
-- ∅ 🐾 something