{"id":496,"date":"2018-11-18T09:14:19","date_gmt":"2018-11-18T09:14:19","guid":{"rendered":"https:\/\/books.compclassnotes.com\/elementarycomputing\/?page_id=496"},"modified":"2018-11-18T09:14:19","modified_gmt":"2018-11-18T09:14:19","slug":"formal-notation","status":"publish","type":"page","link":"https:\/\/books.compclassnotes.com\/elementarycomputing\/formal-notation\/","title":{"rendered":"Formal Notation"},"content":{"rendered":"<p>The last step in this section is to formalise what we&#8217;ve been doing. This is useful because it helps us describe the precise steps that were taken in a reduction sequence, which is very valuable when we need to share our work with someone else.<\/p>\n<p>We&#8217;ve been using\u00a0\\(\\beta\\) reductions for a while now, so let&#8217;s give them a formal description:<\/p>\n\\( (\\lambda x. E)\\; a\\; \\overrightarrow\\beta \\; E\\; [a\/x]\\)\n<p>All this means is that we want to replace all the\u00a0<strong>free<\/strong> occurrences of\u00a0<strong>x<\/strong> with\u00a0<strong>a<\/strong> in the expression\u00a0<strong>E<\/strong>. Remember, we&#8217;ve been doing this for a while now, so there&#8217;s nothing new here, we&#8217;re just giving a name to something we&#8217;re already familiar with. Here&#8217;s a simple example:<\/p>\n<p><strong>(\u03bbq.\u00a0 + q q) 3<\/strong><\/p>\n<p>A\u00a0\u00a0\\(\\beta\\) reduction will perform a\u00a0\u00a0\\(\\beta\\)\u00a0<em>conversion<\/em> of\u00a0<strong>q<\/strong> by replacing all free occurrences of it in the body <strong>(+ q q)\u00a0<\/strong>with\u00a0<strong>3.<\/strong> So, in this case:<\/p>\n<ul>\n<li><strong>E\u00a0<\/strong>is\u00a0<strong>(+ q q)<\/strong><\/li>\n<li><strong>x\u00a0<\/strong>is\u00a0<strong>q\u00a0<\/strong>(it&#8217;s the thing being replaced)<\/li>\n<li><strong>a\u00a0<\/strong>is\u00a0<strong>3\u00a0<\/strong>(it&#8217;s the thing bring brought in)<\/li>\n<\/ul>\n<p>And that&#8217;s it! Yes, it looks highly mathematical, but it&#8217;s actually nice and straightforward and is something we&#8217;ve done so much we can virtually do it in our sleep.<\/p>\n<p>Another process that we&#8217;ve been doing all along, this time without even naming it, is \\(\\delta\\) conversion. This is the process of applying a built-in operator (such as\u00a0<strong>+<\/strong>,\u00a0<strong>*<\/strong>, etc.) to its arguments, such as\u00a0<strong>(* 4 3)<\/strong> giving 12. It usually follows a\u00a0\\(\\beta\\) reduction, as that&#8217;s typically when all the arguments are available. If we started with\u00a0<strong>(\u03bbx. ( &#8211; x 1)) 3<\/strong>, for example, we would do the following:<\/p>\n<ul>\n<li>\\(\u00a0 \\overrightarrow\\beta (-\\; 3\\; 1) \\)<\/li>\n<li>\\(\u00a0 \\overrightarrow\\delta 2 \\)<\/li>\n<\/ul>\n<p>\\(\\beta\\) reduction brings the values in and \\(\\delta\\) reductiion evaluates them. The result after full evaluation is said to be in\u00a0<strong>Normal Form<\/strong>, meaning that there are no more redexes left.<\/p>\n<p>We&#8217;ll do one final formal notation. This one isn&#8217;t an operation we have used yet, but it should make sense. This one is \\(\\alpha\\) conversion, and it changes the name of a variable as in:<\/p>\n<p><strong>(\u03bba.\u00a0 +\u00a0 a a) \\(\\overleftrightarrow\\alpha\\)(\u03bbb.\u00a0 +\u00a0 b b)<\/strong><\/p>\n<p>Notice that this is a\u00a0<strong>bidirectional\u00a0<\/strong>arrow, meaning that this is a two way process, so we can go from\u00a0<strong>(\u03bba.\u00a0 +\u00a0 a a)\u00a0<\/strong>to\u00a0<strong>(\u03bbb.\u00a0 +\u00a0 b b)\u00a0<\/strong>and back again. The reason for this is that these are the same function &#8212; yes, the names are different, but the operation is the same, because each takes a single parameter and doubles it. This is another example of syntax versus semantics; we can change the names of the variables without changing the meaning of the function.<\/p>\n<p>We can&#8217;t just arbitrarily change names, though. Consider\u00a0<strong>(\u03bbx. ( +\u00a0 x y))<\/strong> which as\u00a0<strong>x\u00a0<\/strong>as a bound variable and\u00a0<strong>y\u00a0<\/strong>as a free variable. If we perform on \\(\\alpha\\) conversion on\u00a0<strong>x\u00a0<\/strong>to change it to\u00a0<strong>y\u00a0<\/strong>the result is\u00a0<strong>(\u03bby. ( +\u00a0 y y))\u00a0<\/strong>which is not the same function, because now we can&#8217;t tell which y is which. However, how about this one:<\/p>\n<p><strong>(\u03bbx. +\u00a0 x (\u03bby. +\u00a0 y 1) 2)<\/strong><\/p>\n<p>If we \\(\\alpha\\) convert on\u00a0<strong>x\u00a0<\/strong>to change it to\u00a0<strong>y\u00a0<\/strong>we get\u00a0\u00a0<strong>(\u03bby. +\u00a0 y (\u03bby. +\u00a0 y 1) 2)<\/strong>, which, although there are two variables called\u00a0<strong>y<\/strong>, we can easily tell them apart because we know which is bound by which lambda. That is, the\u00a0<em>inner<\/em> y [the\u00a0<strong>(\u03bby. +\u00a0 y 1)<\/strong>] is bound to the inner lambda, while the outer y is bound to the outer lambda.<\/p>\n<p>Let&#8217;s formalise this in the same way we did the other processes:<\/p>\n<p>\\( (\\lambda x. E)\\; \\overleftrightarrow\\alpha \\;(\\lambda y. E)\\; [y\/x]\\) IF y does not already exist free in\u00a0<strong>E<\/strong>.<\/p>\n<p>All this means is that it is okay to change the name of\u00a0<strong>x<\/strong> to\u00a0<strong>y\u00a0<\/strong>as long as\u00a0<strong>y<\/strong> doesn&#8217;t appear free in the function body, which is how we ensure we don&#8217;t get stuck in a situation where we have two different variables with the same name.<\/p>\n<p>Here&#8217;s an example of where we might want to use \\(\\alpha\\) conversion. We have this function:\u00a0<strong>(\u03bbf.\u00a0(\u03bbx. f (f x))<\/strong>. This will accept a function for the parameter\u00a0<strong>f<\/strong>, pass it into its nested function, which then takes a value for its parameter\u00a0<strong>x\u00a0<\/strong>and then applies\u00a0<strong>f\u00a0<\/strong>to\u00a0<strong>x.\u00a0<\/strong>Nothing too mysterious there, but look at what happens if we try to apply this to a variable\u00a0<strong>x<\/strong>.<\/p>\n<p>&nbsp;<\/p>\n<p><strong>(\u03bbf.\u00a0(\u03bbx. f (f x)) x<\/strong><\/p>\n<p>\\(\u00a0 \\overrightarrow\\beta\\) <strong>(\u03bbx. x (x x))<\/strong><\/p>\n<p>Well, that&#8217;s all gone horribly wrong, hasn&#8217;t it? Now we have two different variables called\u00a0<strong>x<\/strong><strong>.\u00a0<\/strong>If we underline the ones brought in during the\u00a0\\(\\beta\\) reduction it is a bit clearer:\u00a0<strong>(\u03bbx. <span style=\"text-decoration: underline\">x<\/span> (<span style=\"text-decoration: underline\">x<\/span> x))<\/strong>, but the problem is that there is no way to tell which is which. If we instead perform an\u00a0\\(\\alpha\\) conversion on the inner lambda, things would be a lot clearer:<\/p>\n<p><strong>(\u03bbf.\u00a0(\u03bbx. f (f x)) x\u00a0<\/strong>\\(\\overleftrightarrow\\alpha\\)\u00a0<strong>(\u03bbf.\u00a0(\u03bby. f (f y)) x<\/strong><\/p>\n<p>\\(\\overleftrightarrow\\beta\\)\u00a0<strong>(\u03bby. x (x y)<\/strong><\/p>\n","protected":false},"excerpt":{"rendered":"<p>The last step in this section is to formalise what we&#8217;ve been doing. This is useful because it helps us describe the precise steps that were taken in a reduction sequence, which is very valuable when we need to share <span class=\"readmore\"><a href=\"https:\/\/books.compclassnotes.com\/elementarycomputing\/formal-notation\/\">Continue Reading<\/a><\/span><\/p>\n","protected":false},"author":4,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-496","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/books.compclassnotes.com\/elementarycomputing\/wp-json\/wp\/v2\/pages\/496","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/books.compclassnotes.com\/elementarycomputing\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/books.compclassnotes.com\/elementarycomputing\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/books.compclassnotes.com\/elementarycomputing\/wp-json\/wp\/v2\/users\/4"}],"replies":[{"embeddable":true,"href":"https:\/\/books.compclassnotes.com\/elementarycomputing\/wp-json\/wp\/v2\/comments?post=496"}],"version-history":[{"count":14,"href":"https:\/\/books.compclassnotes.com\/elementarycomputing\/wp-json\/wp\/v2\/pages\/496\/revisions"}],"predecessor-version":[{"id":510,"href":"https:\/\/books.compclassnotes.com\/elementarycomputing\/wp-json\/wp\/v2\/pages\/496\/revisions\/510"}],"wp:attachment":[{"href":"https:\/\/books.compclassnotes.com\/elementarycomputing\/wp-json\/wp\/v2\/media?parent=496"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}