[FRIAM] visualization of logic(s)

[Marcus Daniels]

Glen writes:


< Yes, to some extent. E.g. like changing "/" to mod ("%"), which changes the algebra from a field to a ring, where sentences like {x>y→x/y<1}, would move from T to F (or ∞ for undefined). But more like removing things like excluded middle or commutativity, etc. >


I wonder about people who work on stuff like this<http://relmics.mcmaster.ca/RATH-Agda/>.   Agda also has this<https://github.com/agda/agda-stdlib/tree/master/src/Algebra> in its standard library.


Marcus


________________________________
From: Friam <friam-bounces at redfish.com> on behalf of ┣glen┫ <gepropella at gmail.com>
Sent: Saturday, September 23, 2017 1:11 PM
To: FriAM
Subject: Re: [FRIAM] visualization of logic(s)

Yes, to some extent. E.g. like changing "/" to mod ("%"), which changes the algebra from a field to a ring, where sentences like {x>y→x/y<1}, would move from T to F (or ∞ for undefined). But more like removing things like excluded middle or commutativity, etc.  The sentences would stay the same.  But the underlying language rules would change, thereby changing the truth status of each sentence.  A 2D grid of sentences to evaluate is just the first thing to pop into my head ... kinda like a cellular automata, except rather than a fixed rule set with changing states, it would be a changing ruleset with fixed "states" (the "state" being the sentence to evaluate).

The simplest example I can imagine would be something like this.  Start with a "language" where the + and - operators are commutative.  So, the grid sentences could be:  {x+y=y+x, x-y=y-x}, which would render as {T, T}.  Then click a button making + and - non-commutative and it would render {F, F}.

Such a system might even be helpful in deciding whether an algorithm is appropriate for a particular context, like showing how some solution methods aren't appropriate if certain conditions aren't satisfied.

The point would be to quickly demonstrate how the underlying rules of the logic can render the inferences different or nonsensical.  It's the "quickly" that I'm looking for ... something to give an instant "Oh, wow, that's REALLY different now", without implying the visualization is an exact, decodable, encoding like Azimuth's wiring diagrams or the trees you're thinking of.  (Is that what you were referring to Carl?  ... the operads over wiring diagrams?)


On 09/22/2017 06:05 PM, Marcus Daniels wrote:
> So you are talking about, say, swapping conjunctions and disjunctions, but you're not concerned with how terms are shared?   I think of logic languages as being strictly (search) tree structures, where a relatively fancy optimization is to do backjumps to avoid uninteresting intermediate searches.   A concurrent systems could expand opportunistically around certain predicates and work forward or backward.   One frustrating thing in a logic program is when one establishes some bad backbone that is a partial solution and then only find out much later it is involved in an impossible solution.   That is, the backtracking ends up very deep.    What is the significance of it being 2D or of some particular width/height?


--
␦glen?

============================================================
FRIAM Applied Complexity Group listserv
Meets Fridays 9a-11:30 at cafe at St. John's College
to unsubscribe http://redfish.com/mailman/listinfo/friam_redfish.com
FRIAM-COMIC http://friam-comic.blogspot.com/ by Dr. Strangelove
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://redfish.com/pipermail/friam_redfish.com/attachments/20170924/5f1a4cd0/attachment.html>