{"id":3161,"date":"2015-05-13T20:52:34","date_gmt":"2015-05-14T00:52:34","guid":{"rendered":"http:\/\/www.goodmath.org\/blog\/?p=3161"},"modified":"2015-05-21T09:55:50","modified_gmt":"2015-05-21T13:55:50","slug":"expressions-and-arity-part-1","status":"publish","type":"post","link":"http:\/\/www.goodmath.org\/blog\/2015\/05\/13\/expressions-and-arity-part-1\/","title":{"rendered":"Expressions and Arity (part 1)"},"content":{"rendered":"

In the last post, we started looking at expressions. In this post, we’re going to continue doing that, and start looking at a simple form of expression typing called arity<\/em>.<\/p>\n

Before we can do that, we need to introduce a couple of new formalisms to complete our understanding of the elements that form expressions. The reason we need another formalism is because so far, we’ve defined the meaning of expressions in terms of function calls. But we’ve still got some ambiguity about our function calls – specifically, how do parameters work?<\/p>\n

Suppose I’ve got a function, f. Can I call it as f(x)? Or f(x,y)? Both? Neither? It depends on exactly what function calls mean, and what it means to be a valid parameter to a function.<\/p>\n

There are several approaches that you can take:<\/p>\n

    \n
  1. You can say that a function application expression takes an arbitrary number of arguments. This is, roughly, what we do in dynamically typed programming languages like Python. In Python, you can write f(x) + f(x,y) + f(x, y, z, a, b, c)<\/code>, and the language parser will accept it. (It’ll complain when you try to execute it, but at the level of expressions, it’s a perfectly valid expression.)<\/li>\n
  2. You can say that every function takes exactly one argument, and that a multi-argument function like f(x, y, z) is really a shorthand for a curried call sequence f(x)(y)(z) – and thus, the “application” operation really takes exactly 2 parameters – a function, and a single value to apply that function to. This is the approach that we usually take in lambda calculus. <\/li>\n
  3. You can say that application takes two arguments, but the second one can be a combination<\/em> of multiple objects – effectively a tuple. That’s what we do in a lot of versions of recursive function theory, and in programming languages like SML.<\/li>\n<\/ol>\n

    In the theory of expressions, Martin-Löf chose the third approach. A function takes a single parameter, which is a combination<\/em> of a collection of other objects. If a, b, c, and d are expressions, then a, b, c, d is an expression called the combination<\/em> of its four elements. This is very closely related to the idea of cartesian products<\/em> in set theory, but it’s important to realize that it’s not the same thing. We’re not defining elements of a set here: we’re defining a syntactic construct of a pseudo-programming language, where one possible interpretation of it is cartesian products.<\/p>\n

    In addition to just multi-parameter functions, we’ll use combinations for other things. In type theory, we want to be able to talk about certain mathematical constructs as first-class objects. For example, we’d like to be able to talk about orderings<\/em>, where an ordering is a collection of objects A combined with an operation \\le. Using combinations, we can write that very naturally as A,\\le.<\/p>\n

    For combinations to be useful, we need to be able to extract the component values from them. In set theory, we’d do that by having projection functions associated with the cross-product. In our theory of expressions, we have selection expressions<\/em>. If x=(a, b, c, d) is a combination with four elements, then x.1 is a selection expression which extracts the first element from x.<\/p>\n

    In programming language terms, combinations give us a way of writing tuple values. Guess what’s next? Record types! Or rather, combinations with named elements. We can write a combination with names: x = (a: 1, b:2), and then write selection expressions using the names, like x.a.<\/p>\n

    Now we can start getting to the meat of things. <\/p>\n

    In combinatory logic, we’d just start with a collection of primitive constant values, and then build whatever we wanted with them using abstractions, applications, combinations, and selections. Combinatory logic is the parent of computation theory: why can’t we just stick with that foundation?<\/p>\n

    There are two answers to that. The first is familiar to programming language people: if you don’t put any restrictions on things, then you lose type safety. You’ll be able to write “valid” expressions that don’t mean anything – things like 1.x, even though “1” isn’t a combination, and so calling a selector on it makes no sense. Or you’d be able to call a function like factorial(27, 13)<\/code>, even though the function only takes one parameter.<\/p>\n

    The other answer is equality. One thing that we’d really like to be able to do in our theory of expressions is determine when two expressions are the same. For example, we’d really like to be able to do things like say that ((x)e)(x) == e. But without some form of control, we can’t really do that: the problem of determining whether or not two expressions are equal can become non-decidable. (The canonical example of this problem involves y combinator: ((x)x(x))((x)x(x)). If we wanted to try to work out whether an expression involving this was equivilant to another expression, we could wind up in an infinite loop of applications.)<\/p>\n

    The way that Martin-Löf worked around this is to associate an arity<\/em> with an expression. Each arity<\/em> of expressions is distinct, and there are rules about what operations can be applied to an expression depending on its arity. You can’t call .2 on “1+3”, because “1+3” is a single<\/em> expression, and selectors can only be applied to combined<\/em> expressions.<\/p>\n

    To most of us, arity sounds like it should be a numeric value. When we we talk about the arity of a function in a program, what we mean is how many parameters it takes. In Martin-Löf expressions, arity is more expressive than that: it’s almost the same thing as types in the simply typed lambda calculus. <\/p>\n

    There are two dimensions to arity: single\/combined and saturated\/unsaturated. <\/p>\n

    Single<\/em> expressions are atomic values, where you can’t extract other values from them by selection; multiple<\/em> expressions are combinations of multiple other expressions.<\/p>\n

    Saturated expressions are expressions that have no holes in them that can be filled by other expressions – that is, expressions with no free variables. Unsaturated expressions have open holes – which means that they can be applied<\/em> to other expressions.<\/p>\n

    Saturated single expressions have arity 0. An expression of arity 0 can’t be applied, and you can’t be the target of selection expressions.<\/p>\n

    An unsaturated expression has an arity (\\alpha \\twoheadrightarrow \\beta), where both \\alpha and \\beta are arities. For example, the integer addition function has arity (0 \\otimes 0 \\twoheadrightarrow 0). (Erik Eidt pointed out that I made an error here. I originally wrote addition as 0 \\twoheadrightarrow 0, where it should have been 0 \\otimes 0 \\twoheadrightarrow 0.)<\/em><\/p>\n

    A combined expression (e_0, e_1, ..., e_n) has arity (\\alpha_1 \\otimes \\alpha_2 \\otimes ... \\otimes \\alpha_n), where each of the \\alpha_is are the arities of the expression e_i.<\/p>\n

    Sadly, I’m out of time to work on this post, so we’ll have to stop here. Next time, we’ll look at the formal rules for arities, and how to use them to define equality of expressions.<\/p>\n","protected":false},"excerpt":{"rendered":"

    In the last post, we started looking at expressions. In this post, we’re going to continue doing that, and start looking at a simple form of expression typing called arity. Before we can do that, we need to introduce a couple of new formalisms to complete our understanding of the elements that form expressions. The […]<\/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-3161","post","type-post","status-publish","format-standard","hentry","category-type-theory"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-OZ","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3161","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=3161"}],"version-history":[{"count":3,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3161\/revisions"}],"predecessor-version":[{"id":3182,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3161\/revisions\/3182"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=3161"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=3161"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=3161"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}