Data types with Negation (never heard of Chu space before this)

Data types with Negation by Bob Atkey

This notes Chu spaces which is new to me and so might be of interest to others here.


Personal notes (Click triangle to expand)

Guide to Papers on Chu Spaces
Introduction to Channel Theory

Thanks for information. It is known that Chu space and Barwise and Seligiman’s Channel theory are close, and once I worked for the latter, though I don’t remember details for now. I think a couple of weeks is enough for me to recover the technical details of both theories. After successful recovery, I would like to post something which I am currently interested and relevant hopefully to this forum.

EDIT 2023/01/25

I posted around July 2022 something like this.

Around 2015 I wrote a piece of codes for cgi on “Information Flow” inspired by the book:
Information Flow - The Logic of Distributed Systems
Jon Barwise, Jerry Seligman
Cambridge University Press
1997.
It was a private prototyping project with unclear plan and goal. Leaving codes untouched for a long time, I found the codes did not work. I reviewed and revised at minimum. Now the cgi works as at 2015. Converts a theory to a classification. The output classification is the most general classification satisfying the theory.

This cgi page, given a distributed system of classifications and informorphisms, computes the core classifications. The core means the colimit of the distributed systems in category theory. I have made no progress and information for recent reserach on the channel theory. Any information on recent channel theory is appreciated.

Now (23 Jan. 2023 ) am reading Gupta’s thesis on Chu Spaces: A Model Of Concurrency. As the chu space and the classification is close at least in formal definition, there should be some interesting bridge between the two theories. So far I got only a vague figure of the bridge.
END EDIT

1 Like

The counterfactual A > B is quite a challenge, to use it
in a top-level. Since after A > B succeeds the dynamic database
would have the state as before, since the idea is to

only temporarily perform a modification. So how would I
do dynamic database changes? The logic programming
language Lolli had a funny solution. Lets say one could use push

to enter a new toplevel, where a change would be seen.
And pop to leave the new toplevel again, with the effect that
the change is rolled back:

?- a > push.
true.

?- a.
true.

?- pop.

?- a.
fail.

Some Prolog systems have similar remains, like the “break”
command. But they cannot rollback states so easily. And even
if they have rollback, its not integrated into the top-level.

Edit 03.02.2023
Ok, this works in SWI-Prolog:

/* SWI-Prolog 9.1.2 */
?- snapshot((assertz(p(a)),prolog)).
% Break level 1
[1]  ?- p(X).
X = a.

[1]  ?- 

% Exit break level 1
true.

?- p(X).
false.

Interesting post, though I understand only partially your idea.

Being inspired, here is a belief-revision sample .

?- assert((fly(tweety) :-  !,   fail).
?- snapshot((asserta(fly(tweety)), prolog)).
?- fly(tweety).
true
[1]  ?- ^D
% Exit break level 1
true.
?- fly(tweety).
false.

I think it coud, and I have reasons to think so. As I posted recently, the codes ifmap.pl in my package pac/prolog/util/ifmap.pl was started for that direction. (B&S Channel theory and Chu space theory are indeed intimiate friends each other). I regret to say it was stopped to develop the codes since long time ago, but now I am going to resume with newly possible help from ZDD technology at some tecnical point.