0

It is not so difficult to conceive an appartness relation for Peano numbers. Its even possible to make a reified eq/3 predicate like here.

Question is now, whether we can push the boundary and also implement Scheme equal? predicate in a pure and reified manner? Problem would be for example to realize this reductions, also known as δ-rule (see Chapter 6 Extensions here):

δxx ~~> T 
δxy ~~> F if x and y are not identical

In case terms are represented with deBruijn indexes. This would incorporate alpha conversion into the equal? predicate besides handling lists (trees). Pure can mean intrinsically pure or operational pure, as defined in the logical purity tag.

Test case is pure intersection with lists (trees), instead only Peano numbers.

  • Can you add some test cases in Scheme proper? – MWB Dec 24 '20 at 00:25
  • equal? is explained here: https://stackoverflow.com/a/17719745/502187 –  Dec 24 '20 at 00:27
  • What's your "pure Prolog", precisely? (Note that [my Q](https://stackoverflow.com/questions/65425800/) was about "almost pure" Prolog) – MWB Dec 24 '20 at 00:28
  • Pure can mean intrinsically pure or operational pure, as defined in the logical purity tag. –  Dec 24 '20 at 16:02

0 Answers0