Flexibile GEO Syntax

[thedotmatrix]

Right now, Razor only excepts it's special geometric theories (positive existential formulas). I believe that it is best for the core of Razor to be able to assume that this is the one and only language it will be operating over.

However, if not now then soon, other specifications / programming languages / tools may be interacting with Razor. These tools will have to translate their input into Razor's expected language / syntax. We also may want to display parts of the theory back to the user in some form. Having an interface to define how to go from/to the plugin language would:

1. Allow us to better help the user resolve syntax / other issues with their input PEF theory.
2. Enable things such as provenance information to be displayed in the plugin language, versus something that was generated / foreign to the end user.

[dandougherty]

This is an important long conversation we three need to have. Beyond the
UI implications it has foundational
implications. Let's remember to talk about this once things slow down a
little (ie after the 22nd)

On Tue, Dec 9, 2014 at 11:40 PM, Ryan Danas notifications@github.com
wrote:

Right now, Razor only excepts it's special geometric theories (positive
existential formulas). I believe that it is best for the core of Razor to
be able to assume that this is the one and only language it will be
operating over.

However, if not now then soon, other specifications / programming
languages / tools may be interacting with Razor. These tools will have to
translate their input into Razor's expected language / syntax. We also may
want to display parts of the theory back to the user in some form. Having
an interface to define how to go from/to the plugin language would:

1. Allow us to better help the user resolve syntax / other issues with
   their input PEF theory.
2. Enable things such as provenance information to be displayed in the
   plugin language, versus something that was generated / foreign to the end
   user.

Reply to this email directly or view it on GitHub
#57.

[salmans]

I agree. This is a very important issue that we need to talk about. Having said that, I really like the current geometric syntax and I think we should promote thinking in geometric logic for specification languages ((c) Steve Vickers!) instead of downplaying it.

[thedotmatrix]

Copying from not git issue emails...

But we have to get past this draconian formatting we impose on the users, if we are going to have the tool adopted for real use.

At a minimum we should allow inputs of the form
alpha => beta and
alpha <=> beta
when alpha and beta are arbitrary PEFs-with-negation

[thedotmatrix]

Supporting arbitrary FOL or other specification languages is very far on the horizon... maybe only in the rewrite.

However, supporting some syntatic sugar of geometric theories is something we can tackle now. Adding bi-implication support, negation removal, conversion to DNF (assuming quantifiers won't cause issues), etc... can happen soon.

[tnelson]

What is the thing that makes full FOL hard to support? (Maybe I'm misunderstanding?)

[thedotmatrix]

As far as I know, the concern is about clausification, and translating provenance information to the original input syntax.

[tnelson]

I have to admit I view input flexibility and provenance-translation as
separate. Without input flexibility nobody is using your tool, so nobody
cares about provenance-translation. Razor should be so lucky as to have
people complaining that their models have incomprehensible provenance info!
:-)

On Fri, Jul 17, 2015 at 1:49 PM, Ryan Danas notifications@github.com
wrote:

As far as I know, the concern is about clausification, and translating
provenance information to the original input syntax.

—
Reply to this email directly or view it on GitHub
#57 (comment).

[dandougherty]

[folding in Shriram. Tim asked a question, the answer to which you may
have interest in]

There are two questions that could be asked:

1. Does Razor support a language that is as powerful as unrestricted
   FOL?

2. Does Razor require the user to enter their theory in a
   syntactically restricted form?

The answer to both of these questions is "yes". (NB: just like Alloy)

Obviously we would like the answer to (2) to be "no". And it's not hard
to see how to do this, indeed I hope Ryan will get this done this
coming year.

I suspect, Tim, that your original question was essentially: why is
the answer to (2) currently "no"? Ryan was partially right in his
answer, but let me elaborate to give you a fuller picture.

• at the start of this project the essential experiment was using the
  Chase for building minimal models and associated provenance. The
  Chase requires "geometric logic". At the beginning I hadn't yet
  worked out how to work with arbitrary FOL theories, that is to say,
  how arbitrary theories T have geometric "companions" T' that enable
  us to find minimal models for the original T. So that generality
  isn't yet reflected in the current Razor.
• Ryan is right that the difference between the original T and
  geometric-form T' represents a user-interface challenge when it
  comes to provenance. But that isn't the reason we don't allow
  arbitrary FOL input syntax.

Dan,
looking at a toucan, I swear to god.

On Fri, Jul 17, 2015 at 1:51 PM, Tim Nelson notifications@github.com
wrote:

I have to admit I view input flexibility and provenance-translation as
separate. Without input flexibility nobody is using your tool, so nobody
cares about provenance-translation. Razor should be so lucky as to have
people complaining that their models have incomprehensible provenance info!
:-)

On Fri, Jul 17, 2015 at 1:49 PM, Ryan Danas notifications@github.com
wrote:

As far as I know, the concern is about clausification, and translating
provenance information to the original input syntax.

—
Reply to this email directly or view it on GitHub
#57 (comment).

—
Reply to this email directly or view it on GitHub
#57 (comment).

[dandougherty]

Thanks, Dan. I'll push back a bit, though: Alloy's language isn't
restricted in the same sense as Razor's---I can write an arbitrary
first-order formula in Alloy without anything more than a bit of
boilerplate and a direct token-to-token translation. Converting to geo form
is much more onerous.

I don't mean that Razor should accept a bunch of spec languages like Alloy
right now. But if I have a first-order spec in mind, having to convert
manually to geo isn't just error-prone, it's a barrier to entry that sends
me back to Alloy, TLA+, and other languages. Barriers to entry are bad
because they prevent you from getting users, and without users you have
nobody challenging your assumptions about what the tool does/should do. If
even we have trouble converting specs, IMO that points to a serious problem.

On Fri, Jul 17, 2015 at 7:54 PM, Dan Dougherty dd@cs.wpi.edu wrote:

[folding in Shriram. Tim asked a question, the answer to which you may
have interest in]

There are two questions that could be asked:

1. Does Razor support a language that is as powerful as unrestricted
   FOL?

2. Does Razor require the user to enter their theory in a
   syntactically restricted form?

The answer to both of these questions is "yes". (NB: just like Alloy)

Obviously we would like the answer to (2) to be "no". And it's not hard
to see how to do this, indeed I hope Ryan will get this done this
coming year.

I suspect, Tim, that your original question was essentially: why is
the answer to (2) currently "no"? Ryan was partially right in his
answer, but let me elaborate to give you a fuller picture.

• at the start of this project the essential experiment was using the
  Chase for building minimal models and associated provenance. The
  Chase requires "geometric logic". At the beginning I hadn't yet
  worked out how to work with arbitrary FOL theories, that is to say,
  how arbitrary theories T have geometric "companions" T' that enable
  us to find minimal models for the original T. So that generality
  isn't yet reflected in the current Razor.
• Ryan is right that the difference between the original T and
  geometric-form T' represents a user-interface challenge when it
  comes to provenance. But that isn't the reason we don't allow
  arbitrary FOL input syntax.

Dan,
looking at a toucan, I swear to god.

On Fri, Jul 17, 2015 at 1:51 PM, Tim Nelson notifications@github.com
wrote:

I have to admit I view input flexibility and provenance-translation as
separate. Without input flexibility nobody is using your tool, so nobody
cares about provenance-translation. Razor should be so lucky as to have
people complaining that their models have incomprehensible provenance
info!
:-)

On Fri, Jul 17, 2015 at 1:49 PM, Ryan Danas notifications@github.com
wrote:

As far as I know, the concern is about clausification, and translating
provenance information to the original input syntax.

—
Reply to this email directly or view it on GitHub
#57 (comment).

—
Reply to this email directly or view it on GitHub
#57 (comment).

[dandougherty]

Sure, but it looks like you are pushing back at my 3-word parenthetical
remark "just like Alloy". Which is fine, I'll take your point there.
The main thrust of my message is that there is no essential obstacle to
handling arbitrary FOL in an approach like Razor's. The current version
doesn't do that, just because it is a first version.

Dan

On Mon, Jul 20, 2015 at 10:52 AM, Tim Nelson tbnelson@gmail.com wrote:

Thanks, Dan. I'll push back a bit, though: Alloy's language isn't
restricted in the same sense as Razor's---I can write an arbitrary
first-order formula in Alloy without anything more than a bit of
boilerplate and a direct token-to-token translation. Converting to geo form
is much more onerous.

I don't mean that Razor should accept a bunch of spec languages like Alloy
right now. But if I have a first-order spec in mind, having to convert
manually to geo isn't just error-prone, it's a barrier to entry that sends
me back to Alloy, TLA+, and other languages. Barriers to entry are bad
because they prevent you from getting users, and without users you have
nobody challenging your assumptions about what the tool does/should do. If
even we have trouble converting specs, IMO that points to a serious problem.

On Fri, Jul 17, 2015 at 7:54 PM, Dan Dougherty dd@cs.wpi.edu wrote:

[folding in Shriram. Tim asked a question, the answer to which you may
have interest in]

There are two questions that could be asked:

1. Does Razor support a language that is as powerful as unrestricted
   FOL?

2. Does Razor require the user to enter their theory in a
   syntactically restricted form?

The answer to both of these questions is "yes". (NB: just like Alloy)

Obviously we would like the answer to (2) to be "no". And it's not hard
to see how to do this, indeed I hope Ryan will get this done this
coming year.

I suspect, Tim, that your original question was essentially: why is
the answer to (2) currently "no"? Ryan was partially right in his
answer, but let me elaborate to give you a fuller picture.

• at the start of this project the essential experiment was using the
  Chase for building minimal models and associated provenance. The
  Chase requires "geometric logic". At the beginning I hadn't yet
  worked out how to work with arbitrary FOL theories, that is to say,
  how arbitrary theories T have geometric "companions" T' that enable
  us to find minimal models for the original T. So that generality
  isn't yet reflected in the current Razor.
• Ryan is right that the difference between the original T and
  geometric-form T' represents a user-interface challenge when it
  comes to provenance. But that isn't the reason we don't allow
  arbitrary FOL input syntax.

Dan,
looking at a toucan, I swear to god.

On Fri, Jul 17, 2015 at 1:51 PM, Tim Nelson notifications@github.com
wrote:

I have to admit I view input flexibility and provenance-translation as
separate. Without input flexibility nobody is using your tool, so nobody
cares about provenance-translation. Razor should be so lucky as to have
people complaining that their models have incomprehensible provenance
info!
:-)

On Fri, Jul 17, 2015 at 1:49 PM, Ryan Danas notifications@github.com
wrote:

As far as I know, the concern is about clausification, and translating
provenance information to the original input syntax.

—
Reply to this email directly or view it on GitHub
#57 (comment).

—
Reply to this email directly or view it on GitHub
#57 (comment).