[opentheory-users] Definition of "term" (plus other issues)

[Joe Leslie-Hurd]

[cc'ing the OpenTheory mailing list]

Hi Gunter,

Thank you very much for suggesting these clarifications. It is always
useful to hear what is confusing to people reading the article
standard for the first time.

I have incorporated all of your suggestions into the standard:

http://www.gilith.com/research/opentheory/article.html

Please take a look and let me know if that would have helped you.

Cheers,

Joe

On Sun, Aug 9, 2015 at 6:10 AM, Günter Rote <rote at inf.fu-berlin.de> wrote:
> Dear Joe.
> Here is another thing which I did not learn explicitly from the
> specification but the "hard way"
>
> 1. I think the following definition is misleading, in particular the
> examples.
>
> term
>     Higher order logic terms, such as 13 and ∀x. x. Terms are
> α-equivalent if they are equal up to a consistent renaming of bound
> variables, so λx y. p x y is α-equivalent to λy x. p y x but not to λy
> x. p x y.
>
> terms are not just the expression, but they always come with a type.
> the examples might be
> 13:bool->bool
> or
> ∀x. x: bool
> or perhaps something more instructive
> λx. f x: (a->int) ->(b->int)
>
> 2. Another clarification that might be worth mentioning: (I think this
> issue has come up in the mailing list).
>
> when you write σ → τ, you are referring to the binary type operator
> with name '->', and not with name "→", (despite utf-8 input)
> (I guess in prettyprinted html output they would both be rendered
> identically?
>
> 3. in appTerm and appThm
>     Constraint: The term f must have a type of the form σ → τ, and the
> term x must have a matching type σ.
>
> I guess when you write "x must have a *matching* type σ." you just mean
> "x must have type σ." I was wondering whether "matching" could have
> been meant in some technical sense such as matching after renaming of type
> variables or even something more elaborate such as unification.
>
> (And, the resulting term f x will (obviously) have type τ.)
>
> 4. maybe you want to say something about the result type in absTerm
>
> With best regards : Günter
>