search

salmans / Razor

5 stars 0 forks source link

Flexibile GEO Syntax #57

Open thedotmatrix opened 9 years ago

thedotmatrix commented 9 years ago

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 commented 9 years ago

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 https://github.com/salmans/Razor/issues/57.

salmans commented 9 years ago

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 commented 9 years ago

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 commented 9 years ago

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 commented 9 years ago

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

thedotmatrix commented 9 years ago

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

tnelson commented 9 years ago

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 https://github.com/salmans/Razor/issues/57#issuecomment-122355139.

dandougherty commented 9 years ago

[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.

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 https://github.com/salmans/Razor/issues/57#issuecomment-122355139.

— Reply to this email directly or view it on GitHub https://github.com/salmans/Razor/issues/57#issuecomment-122355670.

dandougherty commented 9 years ago

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 https://github.com/salmans/Razor/issues/57#issuecomment-122355139.

— Reply to this email directly or view it on GitHub https://github.com/salmans/Razor/issues/57#issuecomment-122355670.

dandougherty commented 9 years ago

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 https://github.com/salmans/Razor/issues/57#issuecomment-122355139.

— Reply to this email directly or view it on GitHub https://github.com/salmans/Razor/issues/57#issuecomment-122355670.