{"id":3166,"date":"2015-05-18T07:48:52","date_gmt":"2015-05-18T11:48:52","guid":{"rendered":"http:\/\/www.goodmath.org\/blog\/?p=3166"},"modified":"2015-05-18T07:48:52","modified_gmt":"2015-05-18T11:48:52","slug":"expressions-and-arity-part-2-equivalence","status":"publish","type":"post","link":"http:\/\/www.goodmath.org\/blog\/2015\/05\/18\/expressions-and-arity-part-2-equivalence\/","title":{"rendered":"Expressions and Arity (Part 2): Equivalence"},"content":{"rendered":"

Continuing where I left off: we were talking about arity<\/em> in Martin-Löf’s theory of expressions. There are two basic problems that arity solves: it makes certain kinds of impossible-to-evaluate expressions be invalid in the theory; and it helps enable some way of comparing expressions for equality. Arity solves both of those problems by imposing a simple type system over expressions.<\/p>\n

At the end of the last post, I started giving a sketch of what arities look like. Now we’re going to dive in, and take a look at how to determine the arity of an expression. It’s a fairly simple system of rules.<\/p>\n

Before diving in, I want to stress the most important thing about the way that these rules work is that the expressions are totally syntactic and static. This is something that confused me the first time I tried to read about expression theory. When you see an expression, you think about how it’s evaluated. But expression theory is a purely syntactic theory: it’s about analyzing expressions as syntactic entities<\/em>. There are, deliberately, no evaluation rules. It’s about understanding what the notations mean, and how to determine when two expressions are equivalent. <\/p>\n

If, under the rules of Martin-Löf’s expression theory, two expressions are equivalent, then if you were to chose a valid set of evaluation rules, the two expressions will evaluate to the same value. But expression equivalence is stronger: expressions are equivalent only if you can prove their equivalence from their syntax.<\/p>\n

That clarified, let’s start by looking at the rules of arity in expressions.<\/p>\n

\n
Variables and Constants<\/em><\/dt>\n
Every variable and every primitive constant has a pre-defined arity; if x is a variable or primitive constant with arity \\alpha, then the expression x has arity \\alpha.<\/dd>\n
Definitions<\/em><\/dt>\n
In a definition D := e, the arity of the defined name D is the same as the arity of the expression e.<\/dd>\n
Applications<\/em><\/dt>\n
If a is an expression of arity \\alpha \\twoheadrightarrow \\beta, and b is a expression of arity \\alpha, then a(b) is an expression of arity \\beta.<\/dd>\n
Abstractions<\/em><\/dt>\n
If e is an expression of arity \\beta and x is a variable of arity \\alpha, then (x)e is an expression of arity \\alpha \\twoheadrightarrow \\beta.<\/dd>\n
Combinations<\/em><\/dt>\n
If e_1 is an expression af arity \\alpha_1, e_2 is an expression of arity \\alpha_2, …, and e_n is an expression of arity \\alpha_n, then a combination expression e_1, e_2, ..., e_n is an expression of arity \\alpha_1 \\otimes \\alpha_2 \\otimes \\ldots \\otimes \\alpha_n.<\/dd>\n
Selections<\/em><\/dt>\n
If e is an expression of arity \\alpha_1 \\otimes \\alpha_2 \\otimes \\ldots \\otimes \\alpha_n where n \\ge 2, then (e).i is an expression af arity e_i.<\/dd>\n<\/dl>\n

Let’s try working through an example: x^2 + 3x + 7. <\/p>\n

    \n
  1. As we saw in this post<\/a>, this is equivalent to the simple AST-form: (x)+(+(*(x,x), *(3, x)),7).<\/li>\n
  2. “x” is a variable of arity 0; “3” and “7” are constants of arity 0; “+” and “*” are constants of arity (0 \\otimes 0) \\twoheadrightarrow 0. <\/li>\n
  3. From the combination rule, since x and 3 both have arity 0, (x, x) and (3, x) each have arity 0 \\otimes 0. <\/li>\n
  4. Since (x, x) has arity 0 \\otimes 0, and * has arity (0 \\otimes 0) \\twoheadrightarrow 0, *(x, x) has arity 0. The same thing works for *(3, x).<\/li>\n
  5. Since the arities of the *(x, x) and *(3, x) are both 0, the combination of the pair (the arguments to the inner “+”) are 0 \\otimes 0, and the arity of the inner sum expression is thus 0.<\/li>\n
  6. Since 7 has arity 0, the combination of it with the inner sum is 0 \\otimes 0, and the arity of the outer sum is 0.<\/li>\n
  7. Since x is a variable of arity 0, and outer sum expression has arity 0, the abstract has arity 0 \\twoheadrightarrow 0.<\/li>\n<\/ol>\n

    If you’re familiar with type inference in the simply typed lambda calculus, this should look pretty familiar; the only real difference is that the only thing that arity really tracks is applicability and parameter counting.<\/p>\n

    Just from this much, we can see how this prevents problems. If you try to compute the arity of 3.1 (that is, the selection of the first element from 3), you find that you can’t: there is no arity rule that would allow you to do that. The selection rule only works on a product-arity, and 3 has arity 0. <\/p>\n

    The other reason we wanted arity was to allow us to compare expressions. Intuitively, it should be obvious that the expression e and the expression (x)e(x) are in some sense equal. But we need some way of being able to actually precisely define that equality.<\/p>\n

    The kind of equality that we’re trying to get at here is called definitional equality<\/em>. We’re not<\/em> trying to define equality where expressions a and b evaluate to equal values – that would be easy. Instead, we’re trying to get at something more subtle: we want to capture the idea that the expressions are different ways of writing the same thing.<\/p>\n

    We need arity for this, for a simple reason. Let’s go back to that first example expression: (x)+(+(*(x,x), *(3, x)),7). Is that equivalent to (y)+(+(*(y,y), *(3, y)),7)? Or to 8x+1? If we apply them to the value 3, and then evaluate them using standard arithmetic, then all three expressions evaluate to 25. So are they all equivalent? We want to be able to say that the first two are equivalent expressions, but the last one isn’t. And we’d really like to be able to say that structurally – that is, instead of saying something evaluation-based like “forall values of x, eval(f(x)) == eval(g(x)), therefore f == g”, we want to be able to do something that says f \\equiv g because they have the same structure. <\/p>\n

    Using arity, we can work out a structural definition of equivalence for expressions. <\/p>\n

    In everything below, we’l write a: \\alpha to mean that a has arity \\alpha, and a \\equiv b : \\alpha to mean that a and b are equivalent expressions of arity \\alpha. We’ll define equivalence in a classic inductive form by structure:<\/p>\n

    \n
    Variables and Constants<\/em><\/dt>\n
    If x is a variable or constant of arity \\alpha, then x \\equiv x : alpha. This is the simplest identity rule: variables and constants are equivalent to themselves.<\/dd>\n
    Definitions<\/em><\/dt>\n
    If a := b is a definition, and b: \\alpha, then a \\equiv b : \\alpha. This is a slightly more complex form of an identity rule: if there’s a definition of b as the value of a, then a and b are equivalent. <\/dd>\n
    Application Rules<\/em><\/dt>\n
    \n
      \n
    1. If a \\equiv a and b \\equiv b, then a(b) \\equiv a. If an applyable expression a is equivalent to another applyable expression a, then applying a to an expression b is equivalent to applying a to an expression b if the argument b is equivalent to the argument b. That’s a mouthful, but it’s simple: if you have two function application expressions, they’re equivalent if both the function expressions and the argument expressions are equivalent.<\/li>\n
    2. If x is a variable of arity \\alpha, and a is an expression of arity \\alpha and b is an expression of arity \\beta, then ((x)b)(a) b[x := a]: \\beta. This is arity’s version of the classic beta rule of lambda calculus: applying an abstraction to an argument means substituting the argument for all references to the abstracted parameter in the body of the abstraction. <\/li>\n<\/ol>\n<\/dd>\n
      Abstraction Rules<\/em><\/dt>\n
      \n
        \n
      1. If x is a variable of arity \\alpha, and b \\equiv b: \\beta, then (x)b \\equiv (x)b: \\alpha \\twoheadrightarrow \\beta. If two expressions are equivalent, then two abstractions using the same variable over the same expression is equivalent.<\/li>\n
      2. If x and y are both variables of arity \\alpha, and b is an expression of arity \\beta, then (x)b \\equiv (y)(b[x := y]): \\alpha \\twoheadrightarrow \\beta, provided y is not free in b.
        \n Basically, the renaming variables in abstractions don’t matter, as long as you aren’t using the variable in the body of the abstraction. So (x)(3+4y) is equivalent to (z)(3+4y), but it’s not equivalent to (y)(3+4y), because y is a free variable in 3+4y, and the abstraction would create a binding for y.<\/p>\n<\/li>\n
      3. \n

        This is arities version of the eta-rule from lambda calculus: If x is a variable of arity \\alpha, and b is an expression of arity \\alpha \\twoheadrightarrow \\beta, then (x)(b(x)) \\equiv b: \\alpha \\twoheadrightarrow \\beta. This is a fancy version of an identity rule: abstraction and application cancel.\n <\/ol>\n<\/dd>\n

        Combination Rules<\/em><\/dt>\n
        \n
          \n
        1. If a_1 \\equiv a_1, a_2 \\equiv a_2, …, a_n \\equiv a_n, then a_1, a_2, ..., a_n \\equiv a_1. This one is simple: if you have two combination expressions with the same arity, then they’re equivalent if their elements are equivalent.<\/li>\n
        2. If e: \\alpha_1 \\otimes \\alpha_2 \\otimes ... \\otimes \\alpha_n, then e.1, e.2, ..., e.n \\equiv: e : \\alpha_1 \\otimes \\alpha_2 \\otimes ... \\otimes \\alpha_n. Another easy one: if you take a combination expression, and you decompose it using selections, and then recombine those selection expressions into a combination, it’s equivalent to the original expression.<\/li>\n<\/ol>\n<\/dd>\n
          Selection Rules<\/em><\/dt>\n
          \n
            \n
          1. If a \\equiv a, then a.i \\equiv a. This is the reverse of combinations rule one: if you have two equivalent tuples, then their elements are equivalent.<\/li>\n
          2. If a_1: \\alpha_1, a_2: \\alpha_2, ..., a_n: \\alpha_n, then (a_1, a_2, ..., a_n).i \\equiv a_i. An element of a combination is equivalent to itself outside of the combination.<\/li>\n<\/ol>\n<\/dd>\n
            Symmetry<\/em><\/dt>\n
            If a: \\alpha, then a \\equiv a: \\alpha.<\/dd>\n
            Symmetry<\/em><\/dt>\n
            If a \\equiv b: \\alpha, then b \\equiv a: \\alpha.<\/dd>\n
            Transitivity<\/em><\/dt>\n
            If a \\equiv b: \\alpha, and b \\equiv c: \\alpha, then a \\equiv c: \\alpha.<\/dd>\n<\/dl>\n

            Jumping back to our example: Is x^2 + 3x + 7 equivalent to x^2 + 3x + 7? If we convert them both into their canonical AST forms, then yes. They’re identical, except for one thing: the variable name in their abstraction. By abstraction rule 2, then, they’re equivalent.<\/p>\n","protected":false},"excerpt":{"rendered":"

            Continuing where I left off: we were talking about arity in Martin-Löf’s theory of expressions. There are two basic problems that arity solves: it makes certain kinds of impossible-to-evaluate expressions be invalid in the theory; and it helps enable some way of comparing expressions for equality. Arity solves both of those problems by imposing a […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":true,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[292],"tags":[],"class_list":["post-3166","post","type-post","status-publish","format-standard","hentry","category-type-theory"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-P4","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3166","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/comments?post=3166"}],"version-history":[{"count":7,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3166\/revisions"}],"predecessor-version":[{"id":3175,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3166\/revisions\/3175"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=3166"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=3166"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=3166"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}