THF and arithmetic operators

[Michael Rawson]

Dear TPTP THF users,

Currently it is technically permitted to partially apply arithmetic
operators and pass them around as first-class objects, like this:

thf(define_sum_of_list, definition, sum_list = zipWith @ $sum).

This is tricky. One cannot tell locally what the type of the term $sum
is, as it is ad-hoc polymorphic for each of $int/$rat/$real. We propose
changing the grammar of TPTP to ensure that arithmetic functions must be
treated as a special form and fully applied. This does not lead to any
loss in expressive power as a partially applied function can still be
written expanded:

thf(define_sum_of_list, definition, sum_list = zipWith @ (^[X : $int, Y
: $int]: $sum(X, Y))).

...but it is admittedly a little noisier. What do you think?

M

[Christoph Benzmueller]

Hi Michael,

to me this makes much sense.

Best, C.

--
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 visit https://groups.google.com/d/msgid/tptp-world/26996f53-68dc-429b-b7ab-ccad8686bdc9%40rawsons.uk.

--

Univ.Prof. Dr. Christoph Benzmüller

Chair for AI Systems Engineering (AISE), Otto-Friedrich-Universität Bamberg (https://www.uni-bamberg.de/aise/)

Prof. (apl.) at Dep. of Mathematics and Computer Science, FU Berlin (http://christoph-benzmueller.de/)   

[Alexander Steen]

Hi Michael, all,

can't you infer the type instance of $sum in TH0 because you have to specify the type of sum_list/zipWith first, or am I overlooking something? Regardless, I remember quite well I struggled with this ad-hoc polymorphism in Leo-III, so I'm all for it.

In TH1, you could also write "$sum @ $int" if $sum gets a proper polymorphic type signature.

Best, Alex

To view this discussion visit https://groups.google.com/d/msgid/tptp-world/CADQSQfHLzaVza6uuhQ_R2136kb26AmXtppmeEwZnz-JvXAAttg%40mail.gmail.com.

[Stephan Schulz]

Hi all,

I’m all for it, but don’t we have the same problem with equality?

I get the feeling that the practical syntax for HOL is less well
thought out than the one for FOL - maybe because the theoretical
syntax is so much freer..

Greeting from the trans-alp-bicyle route,

Stephan

> To view this discussion visit https://groups.google.com/d/msgid/tptp-world/a3d334bc-6f76-4e2f-b8cd-93e8d37d6f18%40gmail.com.

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

[Geoff Sutcliffe]

Hi all,

> > can't you infer the type instance of $sum in TH0 because you have to specify
the type of sum_list/zipWith first, or am I overlooking something? Regardless, I
remember quite well I struggled with this ad-hoc polymorphism in Leo-III, so I'm
all for it.

> > In TH1, you could also write "$sum @ $int" if $sum gets a proper polymorphic
type signature.

That's what we have for equality, as Stephan asked ...

> I'm all for it, but don't we have the same problem with equality?

There is the @= in TH1 ...
    ? [B: bird] : ( (@= @ bird) @ tweety @ B )
... but that was not extended to the arithmetic functions/predicates.

> >> Currently it is technically permitted to partially apply arithmetic
> >> operators and pass them around as first-class objects, like this:
> >>
> >> thf(define_sum_of_list, definition, sum_list = zipWith @ $sum).
> >>
> >> This is tricky. One cannot tell locally what the type of the term $sum
> >> is, as it is ad-hoc polymorphic for each of $int/$rat/$real. We propose
> >> changing the grammar

I would prefer to no change the grammar, but instead make it a semantic
constraint. Changing the grammar can have far-reaching impacts. Also, it
allows weirdos to ignore the constraint in their own use of the TPTP
grammar.

> >> of TPTP to ensure that arithmetic functions must be
> >> treated as a special form and fully applied. This does not lead to any
> >> loss in expressive power as a partially applied function can still be
> >> written expanded:
> >>
> >> thf(define_sum_of_list, definition, sum_list = zipWith @ (^[X : $int, Y
> >> : $int]: $sum(X, Y))).
> >>
> >> ...but it is admittedly a little noisier. What do you think?

A middle ground would be to allow partial application, but not no-application,
e.g., allow ($sum @ 2) but not plain $sum. The partial application tells you
the type. But that's getting messy.

Cheers,

Geoff

[Stephan Schulz]

> On 21 Aug 2025, at 18:31, Geoff Sutcliffe <geoffgeo...@gmail.com> wrote:
>
>
>
> A middle ground would be to allow partial application, but not no-application,
> e.g., allow ($sum @ 2) but not plain $sum. The partial application tells you
> the type. But that's getting messy.

That’s special pleading and will break down if we ever get a polymorphic
function with a type not fully defined by the first argument...

Bye,

Stephan

[Michael Rawson]

> I would prefer to no change the grammar, but instead make it a semantic
> constraint. Changing the grammar can have far-reaching impacts. Also, it
> allows weirdos to ignore the constraint in their own use of the TPTP
> grammar.

I freely admit I don't see the (functional) difference, so let's call it
a semantic constraint. :-)

M