[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-bounces at redfish.com> on behalf of ┣glen┫ <gepropella at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://redfish.com/pipermail/friam_redfish.com/attachments/20170924/6f0c44d1/attachment.html>