Zulip Chat Archive

Stream: Type theory

Topic: Measuring the complexity of terms


view this post on Zulip 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.

view this post on Zulip Josh Chen (Feb 10 2021 at 11:15):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Josh Chen (Feb 10 2021 at 12:11):

38

view this post on Zulip 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?)

view this post on Zulip Johan Commelin (Feb 10 2021 at 12:17):

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

view this post on Zulip Eric Wieser (Feb 10 2021 at 12:19):

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

view this post on Zulip Josh Chen (Feb 10 2021 at 12:20):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 10 2021 at 12:21):

#reduce 37 gives the term you're expecting

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Feb 10 2021 at 16:11):

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

view this post on Zulip Mario Carneiro (Feb 10 2021 at 16:11):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 10 2021 at 16:14):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Jannis Limperg (Feb 10 2021 at 16:17):

Okay, then that's not a problem.

view this post on Zulip 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