From 8896fb6d8507f28708699e54a4fd03288b05d5b3 Mon Sep 17 00:00:00 2001 From: Marvin Borner Date: Sun, 8 Sep 2024 14:34:34 +0200 Subject: [PATCH] Fun new tupling technique --- samples/fun/goldbach.bruijn | 2 +- .../variadic_fixed-point_combinator.bruijn | 77 +++++++++++++++++-- std/List/Church.bruijn | 3 +- 3 files changed, 71 insertions(+), 11 deletions(-) diff --git a/samples/fun/goldbach.bruijn b/samples/fun/goldbach.bruijn index 8f2a235..feaf1ee 100644 --- a/samples/fun/goldbach.bruijn +++ b/samples/fun/goldbach.bruijn @@ -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]]]])] diff --git a/samples/rosetta/variadic_fixed-point_combinator.bruijn b/samples/rosetta/variadic_fixed-point_combinator.bruijn index cf50875..f5d6ec8 100644 --- a/samples/rosetta/variadic_fixed-point_combinator.bruijn +++ b/samples/rosetta/variadic_fixed-point_combinator.bruijn @@ -1,10 +1,13 @@ +:import std/Combinator . :import std/Number . :import std/List . -y* [[[0 1] <$> 0] ([[1 0)]] <$> 0)] +# --------------- +# explicit Church +# --------------- -# --- example usage --- -# mutual recurrence relation of odd?/even? +# passes all functions explicitly +explicit-y* [[[0 1] <$> 0] ([[1 0)]] <$> 0)] # even x = if x == 0 then true else odd? (x-1) g [[[=?0 [[1]] (1 --0)]]] @@ -12,11 +15,69 @@ 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]]) diff --git a/std/List/Church.bruijn b/std/List/Church.bruijn index c17988c..4b1470d 100644 --- a/std/List/Church.bruijn +++ b/std/List/Church.bruijn @@ -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 0)]] <$> 0 +y* y [[&(1 0) <$> 0]] :test (&(+5) <$> (y* ([[[=?0 true (1 --0)]]] : {}[[[=?0 false (2 --0)]]]))) (false : {}true)