From 7b6cb64548d3eaf9d4bd39a8239d8f14f18ff460 Mon Sep 17 00:00:00 2001 From: giles Date: Fri, 8 May 2026 11:36:14 +0000 Subject: [PATCH] =?UTF-8?q?mk:=20not-membero=20=E2=80=94=20relational=20"x?= =?UTF-8?q?=20is=20not=20in=20l"?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Mirrors the structure all-distincto already uses internally: walk the list, ensure each element is not equal to x via nafc, recurse on tail. Useful as a constraint-style filter: (membero x (list 1 2 3 4 5)) (not-membero x (list 2 4)) -> x in {1, 3, 5} 4 new tests, 382/382 cumulative. --- lib/minikanren/relations.sx | 10 +++++++++- lib/minikanren/tests/not-membero.sx | 29 +++++++++++++++++++++++++++++ plans/minikanren-on-sx.md | 4 ++++ 3 files changed, 42 insertions(+), 1 deletion(-) create mode 100644 lib/minikanren/tests/not-membero.sx diff --git a/lib/minikanren/relations.sx b/lib/minikanren/relations.sx index 6423a759..b04768d7 100644 --- a/lib/minikanren/relations.sx +++ b/lib/minikanren/relations.sx @@ -50,6 +50,14 @@ ((fresh (d) (conso x d l))) ((fresh (a d) (conso a d l) (membero x d)))))) +(define + not-membero + (fn + (x l) + (conde + ((nullo l)) + ((fresh (a d) (conso a d l) (nafc (== a x)) (not-membero x d)))))) + (define reverseo (fn @@ -82,6 +90,7 @@ ((nullo l) (nullo p)) ((fresh (a d perm-d) (conso a d l) (permuteo d perm-d) (inserto a perm-d p)))))) + (define flatteno (fn @@ -97,7 +106,6 @@ (appendo hf tf flat))) ((nafc (nullo tree)) (nafc (pairo tree)) (== flat (list tree)))))) - (define rembero (fn diff --git a/lib/minikanren/tests/not-membero.sx b/lib/minikanren/tests/not-membero.sx new file mode 100644 index 00000000..8952f79e --- /dev/null +++ b/lib/minikanren/tests/not-membero.sx @@ -0,0 +1,29 @@ +;; lib/minikanren/tests/not-membero.sx — relational "not in list". + +(mk-test + "not-membero-absent" + (run* q (not-membero 99 (list 1 2 3))) + (list (make-symbol "_.0"))) +(mk-test + "not-membero-present" + (run* q (not-membero 2 (list 1 2 3))) + (list)) +(mk-test + "not-membero-empty" + (run* q (not-membero 1 (list))) + (list (make-symbol "_.0"))) + +(mk-test + "not-membero-as-filter" + (run* + q + (fresh + (x) + (membero + x + (list 1 2 3 4 5)) + (not-membero x (list 2 4)) + (== q x))) + (list 1 3 5)) + +(mk-tests-run!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index 9f5749a6..733eaea6 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -173,6 +173,10 @@ _(none yet)_ _Newest first._ +- **2026-05-08** — **not-membero**: relational "x is not a member of l". + Uses `nafc + ==` per element (the same skeleton all-distincto uses). + Useful as a constraint-style filter: `(membero x dom) (not-membero x + excluded)`. 4 new tests, 382/382 cumulative. - **2026-05-08** — **repeato + concato**: repeato builds a list of n copies (Peano n); concato is fold-appendo over a list of lists. Both run forward and backward — repeato can recover the count from a uniform list. 10 new