TPTP <comment>s: a minor proposal

[Michael Rawson]

Hi TPTPers,

Something I noticed while working with TPTP is that the BNF says
"comments may occur between any two tokens", but in practice I only
ever see comments in the header section or (rarely) occurring between
<TPTP_input>s. For example:

%%%%%%%%%%%%%%%%%
% header section
% more headers
%%%%%%%%%%%%%%%%%

% this is a really useful formula
fof(...)
/* this one too! */
fof(...)

% include those pesky axioms
include(...)

But I never see:

fof(
% this is the conjecture
show_this,
% o rly?
conjecture,
% ya rly
p(/* no wai! */c)
).

I do note that _whitespace_ between tokens is very common, and maybe
even required (?), but are any of you aware of any problems/systems
that have/support/require <comment>s within <TPTP_input>s? Geoff says
'no' and that his parsers won't actually parse such inputs.

For me it would significantly improve the performance of my TPTP parser
if comments were only permitted outside of <TPTP_input>s. I'd also like
to support including (defined, system) comments in syntax trees, but
it's a big ask if they can occur anywhere!

I propose that we change the wording from

"comments may occur between any two tokens"

to

"comments may occur between any two <TPTP_input>s"*

to match what appears to be accepted practice and save lexerless
parsers like mine a few cycles. Any objections, suggestions?

It's worth mentioning that if your (lexer?) parser already accepts
<comment>s anywhere as per the current spec, I doubt anyone will mind
the extra flexibility so you wouldn't have to change anything.

Happy new year!

Michael

*Geoff suggested this wording but with <annotated_formula>s instead -
sorry Geoff! I don't have a strong opinion either way but presumably we
don't want to forbid comments between include() directives?

[Alexander Steen]

Hi Michael,

Leo-III actually accepts comments between any tokens (I have never seriously tested the extent of it, but it should allow pretty much everything in this regard).

For example, the following input is perfectly fine for Leo-III:

/* comment */
thf(a_type, type /* hello */, a: /* should I choose $i? */ $i) /* even here */. /* EOL */
/* comment */
thf(/* pick a better name soon*/ c, conjecture, /* yeaha */ a =  /* take this, geoff! */ a). /* EOL */
/* comment */

Currently, this works because the lexer/tokenizer already throws away every comment input before the actual parsing. I guess it becomes uglier if you want to be able to process/parse the comments themselves.

I don't see any downsides in restricting the comments as you proposed; I've never seen this flexibility used anywhere.

Best, Alex

PS. Happy new year to all!

[Stephan Schulz]

Hi!

> On 5 Jan 2022, at 13:26, Alexander Steen <alx....@gmail.com> wrote:
>
> Hi Michael,
>
> Leo-III actually accepts comments between any tokens (I have never seriously tested the extent of it, but it should allow pretty much everything in this regard).
> For example, the following input is perfectly fine for Leo-III:
>
> /* comment */
> thf(a_type, type /* hello */, a: /* should I choose $i? */ $i) /* even here */. /* EOL */
> /* comment */
> thf(/* pick a better name soon*/ c, conjecture, /* yeaha */ a = /* take this, geoff! */ a). /* EOL */
> /* comment */
>
> Currently, this works because the lexer/tokenizer already throws away every comment input before the actual parsing. I guess it becomes uglier if you want to be able to process/parse the comments themselves.

E also allows comments anywhere. Essentially, the lexer treats comments like
white space. If I want to process the comments, the lexer has an option to
either pass them through or, more usefully, to accumulate them. The collected
comments can then be attached to the parse tree at the TPTP input level.

>
> I don't see any downsides in restricting the comments as you proposed; I've never seen this flexibility used anywhere.

I find the flexibility useful, in particular to stick illuminating
comments at the end of the line. But it’s no big deal to me.

Bye,

Stephan

> Best, Alex
>
> PS. Happy new year to all!

Indeed! ;-)

> --
> You received this message because you are subscribed to the Google Groups "TPTP World" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tptp-world+...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tptp-world/1ece7396-7578-472b-a16a-3c2ffea3b70an%40googlegroups.com.


--
------------------------------ It can be done! ---------------------------------
Please email me as sch...@eprover.org (Stephan Schulz)
--------------------------------------------------------------------------------

[Simon Cruanes]

Similarly, Zipperposition has a lexer that skips comments, so they can
appear anywhere. Like Stephan says it's useful at the end of lines, or
before a tricky sub-formula potentially.

--
Simon Cruanes

[Claudia Schon]

Hi,

>>
>> I don't see any downsides in restricting the comments as you proposed; I've never seen this flexibility used anywhere.
>
> I find the flexibility useful, in particular to stick illuminating
> comments at the end of the line. But it’s no big deal to me.

I fully agree that the ability to leave comments on formulas or subformulas can be quite useful.

Recently, I actually looked in the TPTP for formula sets in which formulae or subformulae contain comments that describe in natural language what the formulae say.
My idea was to learn sentence embedding on such comments.
Unfortunately, I didn't really find what I was looking for.

Best,
Claudia

> To view this discussion on the web visit https://groups.google.com/d/msgid/tptp-world/D9653ADD-04C4-470A-85D8-50E8F4BFF303%40eprover.org.

[Michael Rawson]

It appears there's quite a few people who like and/or use comments-in-
formulae! That's OK - I rescind my criticism of inline <comment>s (that
nobody uses them) and it looks like Geoff has some parsers to fix. ;-)

Thank you everyone for the input.

Michael

> > https://groups.google.com/d/msgid/tptp-world/D9653ADD-04C4-470A-85D8-50E8F4BFF303%40eprover.org
> > .

[Geoff Sutcliffe]

Hi all,

Having comments between tokens is easy if you just show them away, or at least don't need to remember where they are. Michael and I both need to spit them out again, in my case for pretty-printing TPTP files. So, we'll leave it as possible to put between tokens, but that will never happen in any TPTP file. Happily, I won't have to fix my parser :-)

Cheers,

Geoff