## Stream: Type theory

### Topic: Measuring the complexity of terms

#### Roman Bars (Feb 09 2021 at 16:02):

Consider the set of closed typeable terms whose type is a term of Type 0 (we are working within Lean's underlying type theory).

Is there some "natural" function from that to non-negative integers such that the inverse image of any non-negative integer is finite?

We don't require that judgmentally equal terms are mapped to the same integer.

We could use the length of the defining string when fully elaborated in Lean but that is pretty arbitrary.

#### Josh Chen (Feb 10 2021 at 11:15):

Going by your topic title, isn't term depth an example of such a function?

#### Roman Bars (Feb 10 2021 at 11:22):

Josh Chen said:

Going by your topic title, isn't term depth an example of such a function?

Is there a reference discussing that? I've been trying to find something but so far unsuccessfully.

#### Jannis Limperg (Feb 10 2021 at 11:35):

Your finiteness criterion is not so easy to fulfill. E.g. if you take the length of the string, you have λ x, x, λ y, y etc. all mapped to 5. This could be solved by working up to α-equality, but there may be other instances of this problem.

What do you want to do with this function?

#### Johan Commelin (Feb 10 2021 at 12:06):

Josh Chen said:

Going by your topic title, isn't term depth an example of such a function?

What is the term depth of x in

def y : nat := 37
def x : nat := y


38

#### Josh Chen (Feb 10 2021 at 12:12):

I may be thinking a lot less syntactically than the question means to ask; consider the AST depth of the normalized term (I think Lean still has normalization of closed terms?)

#### Johan Commelin (Feb 10 2021 at 12:17):

Ok... this is beyond what I know about Leans internals...

#### Eric Wieser (Feb 10 2021 at 12:19):

Are you sure its not 5, since 37 is bit1 (bit0 (bit1 (bit0 (bit0 1))))?

#### Josh Chen (Feb 10 2021 at 12:20):

Sure, if that's what the constructors are :grinning:

#### Eric Wieser (Feb 10 2021 at 12:20):

It's not what the constructors are, but it is what #check 37 prints with pp.numerals set to false

#### Eric Wieser (Feb 10 2021 at 12:21):

#reduce 37 gives the term you're expecting

#### Josh Chen (Feb 10 2021 at 12:22):

*whatever the normalized term is, which I guess is what #reduce does. I'm not very familiar with Lean's specific type theory.

#### Josh Chen (Feb 10 2021 at 12:24):

But I understand that if @Roman Bars wants to do something implementation-related you'd need to consider terms more syntactically.

#### Mario Carneiro (Feb 10 2021 at 14:56):

A less synthetic approach would be to take the depth of the typing derivation of the term. There are a finite number of finitely branching rules so the set of terms with a given depth of typing derivation is finite

#### Mario Carneiro (Feb 10 2021 at 14:57):

To handle definitions, you would also have to include the typing derivation steps involved in filling the environment with those definitions before you use them

#### Mario Carneiro (Feb 10 2021 at 14:58):

I don't think it's a good idea to rely on the result of #reduce because it doesn't always terminate

#### Jannis Limperg (Feb 10 2021 at 15:26):

There could still be trouble with user-defined types, e.g. Bool1 = true1 | false1 etc. with id1 := λ (x : Bool1), x etc. The identity functions would all have the same typing derivation depth, even if the typing derivation of Bool1 is included in the measure. If we can pretend that Lean doesn't have user-defined data types (so only sums and products or W-types or something), that might work.

(Supremely hacky solution: encode the names into the output. But then you might as well Gödel-encode the terms. :P)

#### Mario Carneiro (Feb 10 2021 at 16:11):

no, the typing derivation depth will count variables as de bruijn

#### Mario Carneiro (Feb 10 2021 at 16:11):

because the proof that de bruijn variable #n is well typed has length n

#### Mario Carneiro (Feb 10 2021 at 16:13):

Alternatively, if you want to count these alpha-equal terms as distinct, you just have to add in the construction of the name itself to the typing derivation

#### Mario Carneiro (Feb 10 2021 at 16:14):

so \lam x, x and \lam y, y will have the same typing derivation length but \lam blabla, blabla will be longer

#### Mario Carneiro (Feb 10 2021 at 16:14):

same thing for the names of constructors in an inductive data type

#### Jannis Limperg (Feb 10 2021 at 16:15):

Yes, but you can construct infinitely many distinct id_i functions with the same type derivation length, even disregarding the naming of the variable, because you can have infinitely many distinct Bool_i. If you add the name lengths, I guess that works, assuming a finite character set.

#### Mario Carneiro (Feb 10 2021 at 16:16):

you can have infinitely many distinct Bool_i.

The theory I use in the paper uses structural typing, so these types are all considered the same

#### Jannis Limperg (Feb 10 2021 at 16:17):

Okay, then that's not a problem.

#### Mario Carneiro (Feb 10 2021 at 16:17):

but if you want to recover nominal typing you can stick an index on the mu constructor and that's the measure that increases

Last updated: May 08 2021 at 21:09 UTC