Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > sci.physics > #894090

Julio: How to sort rational trees in Prolog? (Was: How to formalize dependent setoid morphisms?)

Show all headers | View raw

Hi,

Some people like Juglio post references to
wonderful meandering along terminology like:

 > If X has decidable equality and negation
 > of equality is an apartness relation, then
 > the negation of equality is a (in fact the
 > unique) decidable tight apartness relation
 > on X, and any function from X to any set
 > Y with a tight apartness relation on Y
 > must be strongly extensional.
https://ncatlab.org/nlab/show/strongly+extensional+function#examples

Still they are clueless how to sort rational
trees in Prolog. I am pretty sure such people
don't know how to do it practically in a Prolog system.

Bye

Julio Di Egidio schrieb:
 > In fact, how to constructive mathematics a la Bishop.
 >
 > I haven't got to the bottom of it, it turns out to be
 > a long term project in itself, for both theoretical and
 > technical reasons, but here are few notes and mainly the
 > references that I have managed to collect.
 >
 > "How to formalize dependent setoid morphisms?"
 > <https://discourse.rocq-prover.org/t/2759>
 >
 > To be continued...
 >
 > -Julio

Back to sci.physics | Previous | Next | Find similar | Unroll thread

Thread

Julio: How to sort rational trees in Prolog? (Was: How to formalize dependent setoid morphisms?) Mild Shock <janburse@fastmail.fm> - 2025-07-20 23:23 +0200

csiph-web