Re: [FRIAM] visualization of logic(s)

[Marcus Daniels]

Glen writes:


"I had a conversation with a guy the other day who claims there are more Coq 
formulations of typical (continuum) math than the other assistants he was aware 
of.  But I wouldn't know one way or the other.  I don't know if there's a 
significant difference in use cases or domains for Agda vs. Coq (or Isabelle or 
whatever).  But if the demo targeted "intuitions", then I'd want to pick an 
evaluator that posed the least amount of work (for me!) to write sentences 
(theories) representing those intuitions."


Agda and Idris look more like Haskell, and are intended to be useful for 
implementation (thus more in my wheelhouse).   Coq is more established and may 
be better suited for what you want, especially if it is true there are relevant 
formulations (I don't know).


Marcus


From: Friam <friam-boun...@redfish.com> on behalf of ┣glen┫ 
<geprope...@gmail.com>
Sent: Sunday, September 24, 2017 11:20:22 AM
To: FriAM
Subject: Re: [FRIAM] visualization of logic(s)

On 09/23/2017 12:36 PM, Frank Wimberly wrote:
> Disjunctive normal form might be useful in this visualization in that the 
> patterns of F and T might be more easily seen.

Yes, for focusing on logical sentences.  I can imagine generalizing it to any 
sort of predicate, though ... kinda like a MISD system, where the cells contain 
the instructions and the language is like the data.  Then the instructions 
could take any form and the "quick grok" would lie in however those cells were 
represented, colors, digits, alphabet, or whatever.

On 09/23/2017 09:53 PM, Marcus Daniels wrote:
> 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.

Interesting.  I did have in mind using something like Coq to evaluate the 
status of each cell.  I had a conversation with a guy the other day who claims 
there are more Coq formulations of typical (continuum) math than the other 
assistants he was aware of.  But I wouldn't know one way or the other.  I don't 
know if there's a significant difference in use cases or domains for Agda vs. 
Coq (or Isabelle or whatever).  But if the demo targeted "intuitions", then I'd 
want to pick an evaluator that posed the least amount of work (for me!) to 
write sentences (theories) representing those intuitions.

--
␦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

Re: [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-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

Re: [FRIAM] visualization of logic(s)

[Frank Wimberly]

Disjunctive normal form might be useful in this visualization in that the 
patterns of F and T might be more easily seen.


Frank C. Wimberly
140 Calle Ojo Feliz
Santa Fe, NM 87505

wimber...@gmail.com wimbe...@cal.berkeley.edu
Phone:  (505) 995-8715  Cell:  (505) 670-9918

-Original Message-
From: Friam [mailto:friam-boun...@redfish.com] On Behalf Of ?glen?
Sent: Saturday, September 23, 2017 1:12 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

Re: [FRIAM] visualization of logic(s)

[┣glen┫]

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

Re: [FRIAM] visualization of logic(s)

[Carl Tollander]

Check out John Baez's recent work on Azimuth blog

C


On Sep 22, 2017 17:50, "gⅼеɳ ☣"  wrote:

>
> Given the discussion of logic(s), I imagine a visualization where we take
> a language, maybe ZFC, come up with a set of sentences, maybe 100 or so,
> and place them on a 2D grid, where each grid point shows their truth
> value.  So, you'd have a 10x10 grid of T's and F's based on how those
> sentences evaluated in ZFC.  You also include a button or something that
> allows you to modify the language in some way.  E.g. click on the button
> and it removes the axiom of regularity and you see the grid points change
> from T to F.  I suppose you could do this with a smattering of sentences
> from first- and (first- plus) second-order logic as well.  I suppose it
> would be critical which sentences you included in the grid and their
> relationship with the underlying language.  In addition to T and F, you
> might also have something like ∞ for undefined, undecidable, or nonsense.
>
> What do you think?  Is this a silly idea?  Does something like it exist
> already?  Would it be interesting?  Useless?
>
> --
> ☣ gⅼеɳ
>
> 
> 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

Re: [FRIAM] visualization of logic(s)

[Marcus Daniels]

"Given the discussion of logic(s), I imagine a visualization where we take a 
language, maybe ZFC, come up with a set of sentences, maybe 100 or so, and 
place them on a 2D grid, where each grid point shows their truth value.  So, 
you'd have a 10x10 grid of T's and F's based on how those sentences evaluated 
in ZFC.  You also include a button or something that allows you to modify the 
language in some way. "


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?


Marcus


From: Friam <friam-boun...@redfish.com> on behalf of gⅼеɳ ☣ 
<geprope...@gmail.com>
Sent: Friday, September 22, 2017 5:50:14 PM
To: FriAM
Subject: [FRIAM] visualization of logic(s)


Given the discussion of logic(s), I imagine a visualization where we take a 
language, maybe ZFC, come up with a set of sentences, maybe 100 or so, and 
place them on a 2D grid, where each grid point shows their truth value.  So, 
you'd have a 10x10 grid of T's and F's based on how those sentences evaluated 
in ZFC.  You also include a button or something that allows you to modify the 
language in some way.  E.g. click on the button and it removes the axiom of 
regularity and you see the grid points change from T to F.  I suppose you could 
do this with a smattering of sentences from first- and (first- plus) 
second-order logic as well.  I suppose it would be critical which sentences you 
included in the grid and their relationship with the underlying language.  In 
addition to T and F, you might also have something like ∞ for undefined, 
undecidable, or nonsense.

What do you think?  Is this a silly idea?  Does something like it exist 
already?  Would it be interesting?  Useless?

--
☣ gⅼеɳ


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

[FRIAM] visualization of logic(s)

[gⅼеɳ ☣]

Given the discussion of logic(s), I imagine a visualization where we take a 
language, maybe ZFC, come up with a set of sentences, maybe 100 or so, and 
place them on a 2D grid, where each grid point shows their truth value.  So, 
you'd have a 10x10 grid of T's and F's based on how those sentences evaluated 
in ZFC.  You also include a button or something that allows you to modify the 
language in some way.  E.g. click on the button and it removes the axiom of 
regularity and you see the grid points change from T to F.  I suppose you could 
do this with a smattering of sentences from first- and (first- plus) 
second-order logic as well.  I suppose it would be critical which sentences you 
included in the grid and their relationship with the underlying language.  In 
addition to T and F, you might also have something like ∞ for undefined, 
undecidable, or nonsense.

What do you think?  Is this a silly idea?  Does something like it exist 
already?  Would it be interesting?  Useless?

-- 
☣ gⅼеɳ


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