Measuring the complexity of terms

Stream: Type theory

[Roman Bars]

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]

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

[Roman Bars]

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]

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]

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

[Josh Chen]

38

[Josh Chen]

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]

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

[Eric Wieser]

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

[Josh Chen]

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

[Eric Wieser]

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

[Eric Wieser]

#reduce 37 gives the term you're expecting

[Josh Chen]

*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]

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

[Mario Carneiro]

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]

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]

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

[Jannis Limperg]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Jannis Limperg]

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]

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]

Okay, then that's not a problem.

[Mario Carneiro]

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