3 ms·
Good question: you can define m↑↑n as: \m n -> n (exp m) 1' where `exp` is Church exponentiation, `flip id`, and `1'` is the Church numeral for 1, that is
by scatters 6y ago
Good question: you can define m↑↑n as:
\m n -> n (exp m) 1'
where `exp` is Church exponentiation, `flip id`, and `1'` is the Church numeral for 1, that is, `id`. According to pointfree.io this expands to:
flip flip id . flip id . flip id
Which isn't particularly illuminating. Pentation isn't much worse, though:
flip flip id . flip id . flip flip id . flip id . flip id