diff options
| author | Marvin Borner | 2023-07-08 18:32:20 +0200 |
|---|---|---|
| committer | Marvin Borner | 2023-07-08 18:32:20 +0200 |
| commit | 4f4910abbbc154c4cf0e0a021fd8a90bff785622 (patch) | |
| tree | 3973c3b781074bb4ffaadd9e12604e31cedf12b6 /std/List.bruijn | |
| parent | 92251c29d6c171d40b14c238b7f73d65185ab86a (diff) | |
Added variadic y combinator
Diffstat (limited to 'std/List.bruijn')
| -rw-r--r-- | std/List.bruijn | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/std/List.bruijn b/std/List.bruijn index 1e9426e..9018137 100644 --- a/std/List.bruijn +++ b/std/List.bruijn @@ -165,7 +165,7 @@ snoc [[1 ++ {}0]] ⧗ (List a) → a → (List a) :test (empty ; (+1)) ({}(+1)) :test ({}(+1) ; (+2)) ((+1) : {}(+2)) -# generates a variadic variation of a list-based function +# generates a variadic box-based function from a list-based function # TODO: Find a solution that does not require boxed terms variadic [[y [[[[rec]]]] 1 0 [[0]]]] ⧗ ((List a) → b) → ((Box a)* → (Box c) → b) rec B.∅?1 (2 0) [4 3 0 (1 ; (B.get i 2))] @@ -173,7 +173,7 @@ variadic [[y [[[[rec]]]] 1 0 [[0]]]] ⧗ ((List a) → b) → ((Box a)* → (Box :test (variadic reverse B.<>(+1) B.<>(+2) B.<>(+3) B.empty) ((+3) : ((+2) : {}(+1))) # constructs list out of boxed terms, ended with an empty box -list variadic i ⧗ (Box a)* → (List a) +list variadic i ⧗ (Box a)* → (Box b) → (List a) :test (list B.<>(+2) B.<>(+3) B.empty) ((+2) : {}(+3)) :test (^(list B.<>(+2) B.<>(+3))) ((+2) : {}(+3)) @@ -461,3 +461,8 @@ iterate z [[[rec]]] ⧗ (a → a) → a → (List a) :test (take (+5) (iterate i (+4))) (take (+5) (repeat (+4))) :test (take (+0) (iterate ++‣ (+0))) (empty) +# calculates all fixed points of a given function as a list +y* [[[0 1] <$> 0] xs] ⧗ a → (List b) + xs [[1 <! ([[1 2 0]] <$> 0)]] <$> 0 + +:test ([0 (+5)] <$> (y* ([[[=?0 true (1 --0)]]] : {}[[[=?0 false (2 --0)]]]))) (false : {}true) |