visualization of logic(s)
Locked
 
|
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
uǝʃƃ ⊥ glen
|
Re: 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. "
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 <[hidden email]> on behalf of gⅼеɳ ☣ <[hidden email]>
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 |
|
|
In reply to this post by gepr
Check out John Baez's recent work on Azimuth blog.... C On Sep 22, 2017 17:50, "gⅼеɳ ☣" <[hidden email]> wrote:
============================================================ 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 |
|
|
In reply to this post by Marcus G. Daniels
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
uǝʃƃ ⊥ glen
|
Re: visualization of logic(s)
|
|
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 [hidden email] [hidden email] Phone: (505) 995-8715 Cell: (505) 670-9918 -----Original Message----- From: Friam [mailto:[hidden email]] 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: visualization of logic(s)
|
|
In reply to this post by gepr
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. Agda also has this in its standard library.
Marcus From: Friam <[hidden email]> on behalf of ┣glen┫ <[hidden email]>
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 |
|
|
In reply to this post by Frank Wimberly-2
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
uǝʃƃ ⊥ glen
|
Re: visualization of logic(s)
|
|
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 <[hidden email]> on behalf of ┣glen┫ <[hidden email]>
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 |
«
Return to Friam
|
1 view|%1 views
| Free forum by Nabble | Edit this page |