2020-04-06 16:47:3 (GMT)
@Alexander Bentkamp : We have a terminological problem in the lambda-free sup paper with the notion of "ground".
2020-04-06 16:47:31 (GMT)
We nowhere say that "ground" implies monomorphic (unlike in the lambda-sup paper).
2020-04-06 16:47:37 (GMT)
And write things like "ground monomorphic first-order logic".
2020-04-06 16:47:58 (GMT)
But then we also talk about "totality on ground terms".
2020-04-06 16:48:16 (GMT)
Which is impossible to achieve if we have type variables.
2020-04-06 16:48:41 (GMT)
So we need to introduce the convention ground means both term-ground and type-ground, and use it consistently.
2020-04-06 16:53:33 (GMT)
Actually, we have the problem to a small extent in our JAR submission.
2020-04-06 16:53:50 (GMT)
We say "ground monomorphic" in a few places where "ground" would be enough according to our nonstandard convention.
2020-04-06 18:34:47 (GMT)
I think we are already using it consistently. Only the definition is missing. The word "monomorphic" in the phrase "ground monomorphic first-order logic" means that this logic does not even have type arguments.
2020-04-06 18:36:32 (GMT)
Oh, I also found the definition now:
A term is \emph{ground} if it is built without using type variables and
contains no term variables.
2020-04-06 18:45:7 (GMT)
Ah.
2020-04-06 18:45:44 (GMT)
As for the sentence, it's mine.
2020-04-06 18:45:53 (GMT)
I added it a couple of hours ago.
2020-04-06 18:46:10 (GMT)
But I think it can be rephrased further (it originates from lambda-sup article).
2020-04-06 18:47:12 (GMT)
Nonetheless, the two places where I changed "ground monomorphic" to "ground" were merely descriptive, not defining.
2020-04-06 18:47:45 (GMT)
E.g. in
Given a ground $\lambda$-free higher-order signature $(\Sigmaty,\{\},\Sigma,\{\})$,
we define a ground monomorphic first-order signature
2020-04-06 18:48:26 (GMT)
Although now I see that the HO signature, although ground, still has polymorphism (type args).
2020-04-06 18:48:38 (GMT)
OK, OK, I'll add back the two monomorphic (x 2 papers).
2020-04-06 18:51:0 (GMT)
Oh, it's your definition. ok :-D
2020-04-06 18:52:36 (GMT)
I'd be happier if some of these "monomorphic" said "simply typed" instead.
2020-04-06 18:52:54 (GMT)
"Ground monomorphic first-order terms" (actual citation) sounds redundant
2020-04-06 18:53:9 (GMT)
because a monomorphic term is normally defined as a term containing no type variables
2020-04-06 18:53:25 (GMT)
(see e.g. TFF1 paper, B. & Paskevic)
2020-04-06 18:53:33 (GMT)
ok, I see. Then we can change it to simply typed. Makes sense.
2020-04-06 18:53:56 (GMT)
I'll do the change. It's really just 2 or 3 places per paper. "Monomorphic" wasn't a word we used often.
2020-04-06 18:54:10 (GMT)
Argh, it doesn't quite work :S
2020-04-06 18:54:28 (GMT)
Simply typed also means, normally that there are only nullary type constructors.
2020-04-06 18:56:34 (GMT)
"ground terms of monomorphic first-order logic"?
2020-04-06 18:57:35 (GMT)
In the def of ground, why make a difference between the type and term variables? How about this: A term is \emph{ground} if it contains neither type nor term variables.