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-boun...@redfish.com> on behalf of ┣glen┫
<geprope...@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
============================================================
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
