Skip to content

Commit

Permalink
Fun new tupling technique
Browse files Browse the repository at this point in the history
  • Loading branch information
marvinborner committed Sep 8, 2024
1 parent f7be717 commit 8896fb6
Show file tree
Hide file tree
Showing 3 changed files with 71 additions and 11 deletions.
2 changes: 1 addition & 1 deletion samples/fun/goldbach.bruijn
Original file line number Diff line number Diff line change
Expand Up @@ -18,4 +18,4 @@ primes sieve zeroS
check y [[[[[primes 0 (1 (4 0))] testp1]]]]
testp1 [0 0 2 [0 4] 0]

main primes (check [[[[0]]]])
main [primes (check [[[[0]]]])]
77 changes: 69 additions & 8 deletions samples/rosetta/variadic_fixed-point_combinator.bruijn
Original file line number Diff line number Diff line change
@@ -1,22 +1,83 @@
:import std/Combinator .
:import std/Number .
:import std/List .

y* [[[0 1] <$> 0] ([[1 <! ([[1 2 0]] <$> 0)]] <$> 0)]
# ---------------
# explicit Church
# ---------------

# --- example usage ---
# mutual recurrence relation of odd?/even?
# passes all functions explicitly
explicit-y* [[[0 1] <$> 0] ([[1 <! ([[1 2 0]] <$> 0)]] <$> 0)]

# even x = if x == 0 then true else odd? (x-1)
g [[[=?0 [[1]] (1 --0)]]]

# odd x = if x == 0 then false else even? (x-1)
h [[[=?0 [[0]] (2 --0)]]]

even? ^(y* (g : {}h))
# merged even/odd
rec explicit-y* (g : {}h)

odd? _(y* (g : {}h))
:test (^rec (+5)) ([[0]])
:test (_rec (+5)) ([[1]])

:test (even? (+5)) ([[0]])
:test (odd? (+5)) ([[1]])
# n % 3
mod3 ^(explicit-y* (zero : (one : {}two)))
zero [[[[=?0 (+0) (2 --0)]]]]
one [[[[=?0 (+1) (1 --0)]]]]
two [[[[=?0 (+2) (3 --0)]]]]

main [[0]]
:test ((mod3 (+5)) =? (+2)) ([[1]])

# ----------------
# explicit tupling
# ----------------

# passes all functions explicitly
# requires a tuple mapping function first
tupled-y* [y [[2 (1 0) 0]]]

# merged even odd
rec tupled-y* map [0 g h]
map [&[[[0 (3 2) (3 1)]]]]

# [[1]] / [[0]] are tuple selectors:

:test (rec [[1]] (+5)) ([[0]])
:test (rec [[0]] (+5)) ([[1]])

# n % 3, [[[2]]] selects first tuple element
mod3 tupled-y* map [0 zero one two] [[[2]]]
map [&[[[[0 (4 3) (4 2) (4 1)]]]]]
zero [[[[=?0 (+0) (2 --0)]]]]
one [[[[=?0 (+1) (1 --0)]]]]
two [[[[=?0 (+2) (3 --0)]]]]

:test ((mod3 (+5)) =? (+2)) ([[1]])

# ---------------
# implicit Church
# ---------------

# passes all functions in a single list
implicit-y* y [[&(1 0) <$> 0]]

# even x = if x == 0 then true else odd? (x-1)
g [[=?0 [[1]] (_1 --0)]]

# odd x = if x == 0 then false else even? (x-1)
h [[=?0 [[0]] (^1 --0)]]

# merged even/odd
rec implicit-y* (g : {}h)

:test (^rec (+5)) ([[0]])
:test (_rec (+5)) ([[1]])

# n % 3
mod3 ^(implicit-y* (zero : (one : {}two)))
zero [[=?0 (+0) (_1 --0)]]
one [[=?0 (+1) (^(~1) --0)]]
two [[=?0 (+2) (^1 --0)]]

:test ((mod3 (+5)) =? (+2)) ([[1]])
3 changes: 1 addition & 2 deletions std/List/Church.bruijn
Original file line number Diff line number Diff line change
Expand Up @@ -532,7 +532,6 @@ enumerate zip (iterate ++‣ (+0)) ⧗ (List a) → (List (Pair Number a))
:test (enumerate "abc") (((+0) : 'a') : (((+1) : 'b') : {}((+2) : 'c')))

# calculates all fixed points of given functions as a list
y* [[[0 1] <$> 0] xs] ⧗ (List a) → (List b)
xs [[1 <! ([[1 2 0]] <$> 0)]] <$> 0
y* y [[&(1 0) <$> 0]]

:test (&(+5) <$> (y* ([[[=?0 true (1 --0)]]] : {}[[[=?0 false (2 --0)]]]))) (false : {}true)

0 comments on commit 8896fb6

Please sign in to comment.