How to implement succesor and addition functions?

[ELC]

Is there a way to implement the successor function and the add function using pure relations and kanren?

[brandonwillard]

Yes, here's one example: https://github.com/TheReasonedSchemer2ndEd/CodeFromTheReasonedSchemer2ndEd/blob/master/trs2-arith.scm

[ELC]

Is there a Python-equivalent or something built with the kanren Python library?

[brandonwillard]

I'm not aware of one. Regardless, the conversion from Scheme should be fairly direct, so it might not be difficult to do.

[ELC]

Now the file linked has 380 lines, is all of that needed to implement simple successor and addition? I was expecting something around 10 lines max

[brandonwillard]

It seems like addero is the relation you want, but you'll need its dependencies (e.g. gen-addero, full-addero, etc.) Also, because those relations are using a binary/bit encoding, you'll need a Python equivalent of build-num to perform the conversion from decimal.

In general, you can use any encoding you want. For instance, you could use a set theoretic encoding based on tuple/lists and the existing conso and appendo relations.