{
  "block": 35808637,
  "op": [
    "comment",
    {
      "author": "steemitboard",
      "body": "Congratulations @otaviomacedo! You received a personal award!\n\n<table><tr><td>https://steemitimages.com/70x70/http://steemitboard.com/@otaviomacedo/birthday3.png</td><td>Happy Birthday! - You are on the Steem blockchain for 3 years!</td></tr></table>\n\n<sub>_You can view [your badges on your Steem Board](https://steemitboard.com/@otaviomacedo) and compare to others on the [Steem Ranking](https://steemitboard.com/ranking/index.php?name=otaviomacedo)_</sub>\n\n\n###### [Vote for @Steemitboard as a witness](https://v2.steemconnect.com/sign/account-witness-vote?witness=steemitboard&approve=1) to get one more award and increased upvotes!",
      "json_metadata": "{\"image\":[\"https://steemitboard.com/img/notify.png\"]}",
      "parent_author": "otaviomacedo",
      "parent_permlink": "nested-types-and-function-composition",
      "permlink": "steemitboard-notify-otaviomacedo-20190823t163347000z",
      "title": ""
    }
  ],
  "op_in_trx": 0,
  "timestamp": "2019-08-23T16:33:48",
  "trx_id": "bd84a7ed4af8dc63e3115a110127ff1f54f45485",
  "trx_in_block": 3,
  "virtual_op": 0
}

{
  "block": 25325507,
  "op": [
    "comment",
    {
      "author": "steemitboard",
      "body": "Congratulations @otaviomacedo! You have received a personal award!\n\n[![](https://steemitimages.com/70x70/http://steemitboard.com/@otaviomacedo/birthday2.png)](http://steemitboard.com/@otaviomacedo)  2 Years on Steemit\n<sub>_Click on the badge to view your Board of Honor._</sub>\n\n\n**Do not miss the last post from @steemitboard:**\n[SteemitBoard and the Veterans on Steemit - The First Community Badge.](https://steemit.com/veterans/@steemitboard/steemitboard-and-the-veterans-on-steemit-the-first-community-badge)\n\n> Do you like [SteemitBoard's project](https://steemit.com/@steemitboard)? Then **[Vote for its witness](https://v2.steemconnect.com/sign/account-witness-vote?witness=steemitboard&approve=1)** and **get one more award**!",
      "json_metadata": "{\"image\":[\"https://steemitboard.com/img/notify.png\"]}",
      "parent_author": "otaviomacedo",
      "parent_permlink": "nested-types-and-function-composition",
      "permlink": "steemitboard-notify-otaviomacedo-20180823t173347000z",
      "title": ""
    }
  ],
  "op_in_trx": 0,
  "timestamp": "2018-08-23T17:33:45",
  "trx_id": "b1a72586f4884633b8378f894c7126be541581f6",
  "trx_in_block": 51,
  "virtual_op": 0
}

{
  "block": 4419709,
  "op": [
    "vote",
    {
      "author": "otaviomacedo",
      "permlink": "from-loop-invariants-to-recursion-invariants",
      "voter": "insiderq",
      "weight": 10000
    }
  ],
  "op_in_trx": 0,
  "timestamp": "2016-08-26T14:17:39",
  "trx_id": "4fab29c5b896318e6956750540c0fb48dc3b0dba",
  "trx_in_block": 6,
  "virtual_op": 0
}

{
  "block": 4365100,
  "op": [
    "vote",
    {
      "author": "otaviomacedo",
      "permlink": "nested-types-and-function-composition",
      "voter": "otaviomacedo",
      "weight": 10000
    }
  ],
  "op_in_trx": 0,
  "timestamp": "2016-08-24T16:18:57",
  "trx_id": "7af87e6c6078a29ca73b0ab4d29a28e64784eed2",
  "trx_in_block": 1,
  "virtual_op": 0
}

{
  "block": 4365100,
  "op": [
    "comment",
    {
      "author": "otaviomacedo",
      "body": "In Scala and other typed functional languages – notably Haskell – monads are structures that allow the programmer to take a sequence of computations, each defined for a certain context, and chain them together in order to produce a single result at the end. For example, suppose you have to use an API that returns values inside the context of future executions. Something like this:\n\n```scala\ndef getAddress(user: User): Future[Address]\ndef getGeolocation(address: Address): Future[LatLong]\ndef getCurrentWeather(coordinates: LatLong): Future[WeatherDetails]    \n```\n\nGiven a certain user, we would like to use this API to find out the current weather conditions at the location where he lives. So we can write a method like:\n\n    def usersWeather(user: User): Future[WeatherDetails] = {\n      for {\n        address <- getAddress(user)\n        coordinates <- getGeolocation(address)\n        weather <- getCurrentWeather(coordinates)\n      } yield weather\n    }\n\nPretty straightforward. In each generator, the value “inside” the Future is supplied as input to the next method in the sequence. Now suppose you were given a more complex API, in which the computations are wrapped inside a context of future execution which may or may not contain a value. In other words, all methods return `Future[Option[T]]`, for some type `T`. So, the methods above would become:\n\n    def getAddress(user: User): Future[Option[Address]]\n    def getGeolocation(address: Address): Future[Option[LatLong]]\n    def getCurrentWeather(coordinates: LatLong): Future[Option[WeatherDetails]]\n\nIn this case, it is not possible use our good old friend `flatMap` anymore. At least not directly, as in the first case. You cannot supply the value of each Future to the next function in the sequence because none of these methods accept an `Option[T]` as input. One possible solution to this problem is to convert these functions to other functions, lifting only their domain from `A` to `Option[A]`:\n\n    def convert[A, B](f: A => Future[Option[B]]): Option[A] => Future[Option[B]] = {\n      maybeA => maybeA map f getOrElse Future(None)\n    }\n\nwhich would allow us to put the functions back in shape to be used in a for comprehension:\n\n    for {\n      address <- convert(getAddress)(user)\n      coordinates <- convert(getGeolocation)(address)\n      weather <- convert(getCurrentWeather)(coordinates)\n    } yield weather\n\nBut we are looking for a more elegant and more general solution, which could work for a whole family of types. If, instead of `Option`, for example, we had `List` or `Either`, we would need customized versions of convert for each of these types. With the aid of typeclasses, however, we can write a single function that allow us to compose these kinds of functions in a simple and concise way.\n\n## A word about typeclasses\nIn the beginning of this article, I talked about how monads allow the programmer to chain a sequence of computations inside a context. But what we actually did was using a for comprehension, which is a syntax sugar for classes that implement the methods `map`, `flatMap`, `filter` and `foreach`.\n\nScalaz, on the other hand, is an awesome library, written in Scala, that provides a broad array of bona fide typeclasses. In particular, Scalaz provides a `Monad[F[_]]` typeclass, which is going to be the most important piece in our solution to composition of functions with nested types.\n\nSo, let’s get to it. First of all, we need to define an instance of `scalaz.Monad` for the `Future` type:\n\n    val futureMonad = new Monad[Future] {\n      override def point[A](a: => A): Future[A] = Future(a)\n \n      override def bind[A, B](fa: Future[A])(f: A => Future[B]): Future[B] =\n        fa.flatMap(f)\n    }\n\nStrictly speaking, this implementation is not a monad, since it violates the [law of left identity][2], which states that `futureMonad.point(a) bind f` should be equal to `f(a)`. While in most cases, this equality relation holds, there is a special case for which it is false. For the sake of robustness, the designers of Scala chose to implement `Future.flatMap` so that it does not throw exceptions, even if the function that was passed as a parameter to it does. So, in the presence of exceptions, this law is broken. But for most practical purposes, this is not important and we can still think of it as a monad.\n\nThe `Option` type, on the other hand, is way less controversial. Scalaz defines monad instances for it, which can be readily made available to an application with an `import`. So we are not going to spend time talking about this particular monad. `Option` is also an instance of the `Traverse` typeclass. In the Haskell documentation (in which most of scalaz was inspired), `Traverse` is defined as a “class of data structures that can be traversed from left to right, performing an action on each element.” The importance of this will become clear in a bit.\n\n## Composing the functions\nSo, with this typeclass arsenal, we can start solving our composition problem. But first, let’s state clearly what exactly is the problem and what we aim to achieve. Given two functions, `f: A => Future[Option[B]]` and `g: B => Future[Option[C]]`, we would like to define a higher-order function that takes `f` and `g` and produces a new function of type `A => Future[Option[C]]`. More formally – and more generically – we need a function `composeN` of the following type:\n\n    composeN[A, B, C, F[_], G[_]](f: A => F[G[B]], g: B => F[G[C]]): A => F[G[C]]\n\nTaking advantage of the richness of Scala’s type system, let’s start by reasoning about the types and what transformations we would need. Observe that both `f` and `composeN` are functions from `A` to `F` (of something). This sounds like monad binding. So, let’s assume we have an implicit value of type `Monad[F]` in scope. The implementation of the method would have the form of:\n\n    a => fMonad.bind(f(a)) {\n      gb => ...\n    }\n\nThe value `gb` above is of type `G[B]`. Assuming that we also have an implicit `Monad[G]` in scope, we could map over `gb`with the function `g`:\n\n    val gfgc: G[F[G[C]]] = gMonad.map(gb)(g)\n\nwhich results in a value of type `G[F[G[C]]]`. Note how the type `G` appears twice in the type declaration. That’s one time too many and we need to get rid of this extra `G`. But before that, let’s make one further assumption: that there is an implicit `Traverse[G]` in scope. This would allow us to use the sequence function of monads to swap the outermost `G` and the `F`:\n\n    val fggc: F[G[G[C]]] = fMonad.sequence(gfgc)\n\nThe last transformation is the one that will take us where we want:\n\n    val fgc: F[G[C]] = fMonad.map(fggc)(ggc => gMonad.bind(ggc)(identity))\n\nSo, the complete definition of the function is as follows:\n\n    def composeN[A, B, C, F[_], G[_]](f: A => F[G[B]], g: B => F[G[C]]): A => F[G[C]] =\n      a => fMonad.bind(f(a)) {\n        gb => fMonad.map(fMonad.sequence(gMonad.map(gb)(g))) {\n          ggc => gMonad.bind(ggc)(identity)\n        }\n      }\n    }\n\nFinally, in order to provide a syntax sugar and make the code look cleaner, we can wrap the first function inside a class (I called it `ComposeNested`, but I’m sure there is a much better name for this) and expose a method to be used as infix operator:\n\n    class ComposeNested[A, B, F[_], G[_]](f: A => F[G[B]])\n              (implicit fMonad: Monad[F], gMonad: Monad[G], gTraverse: Traverse[G]) {\n \n      def ->>[C](g: B => F[G[C]]): A => F[G[C]] = composeN(f, g)\n \n      private def composeN[C](f: A => F[G[B]], g: B => F[G[C]]): A => F[G[C]] = ...\n\nBack to our original example: how can we compose those three functions, chaining the computation through them in a specified order, while preserving their semantics while reducing (or rather hiding) the code noise? Let’s use the operator `->>` we just defined:\n\n    object Demo extends App {\n      val usersWeather = getAddress ->> getGeolocation ->> getCurrentWeather\n \n      val futureWeather = usersWeather(User(\"John Doe\"))\n \n      futureWeather onFailure {\n        case e: Exception => \n          println(s\"Computation failed with the message: ${e.getMessage}\")\n      }\n \n      futureWeather onSuccess {\n        case result => println(s\"Computation result: $result\")\n      }\n \n      Thread.sleep(500)\n    }\n\nThe complete implementation can be found in my [github repository][1].\n\n[1]: https://github.com/otaviomacedo/nested-composition\n[2]: https://wiki.haskell.org/Monad_laws",
      "json_metadata": "{\"tags\":[\"programming\",\"monads\",\"scala\"],\"links\":[\"https://github.com/otaviomacedo/nested-composition\"]}",
      "parent_author": "",
      "parent_permlink": "programming",
      "permlink": "nested-types-and-function-composition",
      "title": "Nested types and function composition"
    }
  ],
  "op_in_trx": 0,
  "timestamp": "2016-08-24T16:18:57",
  "trx_id": "7af87e6c6078a29ca73b0ab4d29a28e64784eed2",
  "trx_in_block": 1,
  "virtual_op": 0
}

{
  "block": 4364596,
  "op": [
    "vote",
    {
      "author": "otaviomacedo",
      "permlink": "from-loop-invariants-to-recursion-invariants",
      "voter": "pedrosgali",
      "weight": 10000
    }
  ],
  "op_in_trx": 0,
  "timestamp": "2016-08-24T15:53:45",
  "trx_id": "75c415e188199241acb23af7bc76b58f9755be48",
  "trx_in_block": 0,
  "virtual_op": 0
}

{
  "block": 4360500,
  "op": [
    "vote",
    {
      "author": "otaviomacedo",
      "permlink": "from-loop-invariants-to-recursion-invariants",
      "voter": "rodolfo.mendes",
      "weight": 10000
    }
  ],
  "op_in_trx": 0,
  "timestamp": "2016-08-24T12:28:45",
  "trx_id": "8a7d1b39a424f35d103998cc1fc73ea6319cb75b",
  "trx_in_block": 0,
  "virtual_op": 0
}

{
  "block": 4355842,
  "op": [
    "comment",
    {
      "author": "otaviomacedo",
      "body": "![Ouroboros](https://upload.wikimedia.org/wikipedia/commons/f/fa/Ouroboros.png)\n\nUntil very recently, the major commercial programming languages were based on the idea of update in place. C, C++, Pascal, Java etc presuppose that the way to solve a programming problem is to have procedures that read and write values to memory locations, be it directly visible to the programmer (by means of pointers) or not.\n\nOther languages, like Lisp, are based on a different assumption: that a computation is best expressed as a set of functions over immutable values. So, in order to produce any kind of repetitive computation, recursion is essential. This assumption has strong roots in lambda calculus and related mathematical formalisms.\n\nProbably due to the popularity of the procedural paradigm, most programmers find it easier to reason about loops than about recursion. But in order to reason effectively about a program, the functional model is far superior. This is what I intend to show in this post.\n\nProgramming models\n-----------------------------\nThe programming model behind procedural code is that of a machine that crunches data for some time and eventually stops. When it stops, we take a look at whatever came up from all this crunching and accept it as the result of the procedure. In some sense, this is the most natural model, since the underlying implementation of the algorithm runs on a real machine that does exactly that.\n\nThe problem is that it would be desirable to conduct some kind of formal reasoning about the code at hand. The same kind we use in mathematics, for example. But the machine model relies heavily on mutation of the contents of chunks of memory over time, which is not exactly amenable to a mathematical analysis.\n\nA neat solution to this problem is the use of loop invariants (cf. [“Introduction to Algorithms”][1]). A loop invariant is a logical predicate that we ascribe to an algorithm. That predicate remains true from the beginning to the end of the algorithm execution, including all the loops that are run, despite the fact that those loops might be changing things. Loop invariants have to take time into account (not clock time, but the discrete time defined by the sequence of operations made by the algorithm) and the values of the variables at each point in time.\n\nBinary search – iterative version\n-------------------------------------------\nLet’s take a simple and common example to illustrate the point: binary search. Given a sorted array and an element, the binary search algorithm returns the index of the element in the array, or -1 if the element is not found. Intuitively, what the algorithm does is: at each iteration, it cuts down the search space to a half, always looking at the element in the middle. The size of the search space tends to zero as the algorithm runs. So, either the element is eventually found or the search space becomes empty and the element can be declared not found. Here is an implementation of the algorithm in Scala:\n\n    def search[T <% Ordered[T]](a: Array[T], elem: T): Int = {\n      var start = 0\n      var end = a.length - 1\n      while (start <= end) { \n        val mid = (start + end) / 2\n        if (elem == a(mid)) return mid \n        else if (elem > a(mid)) start = mid + 1\n        else end = mid - 1\n      }\n      -1\n    }\nWe can prove the intuition behind binary search using loop invariants. The property that remains true throughout its execution is:\n\n> The subarray a(start..end) contains elem if, and only if, a contains elem. (P1)\n\nNote that we are abusing the Scala notation a bit here, when we use `a(i..j)` to indicate a subarray of a from `i` to `j`, inclusive on both ends.\n\n### Proof\n\nLoop invariants have to be proved in three main sections: *initiation* (the initial values assigned to the variables satisfy the property), *maintenance* (at the beginning of each loop, the property is satisfied) and *termination* (when the algorithm stops, what it returns matches up with the expected result). So, here are the three sections for the iterative version of the binary search algorithm:\n\n**Initiation**: lines 2 and 3 define an interval that comprises the whole array, which is equivalent to say that `a` contains `elem` if, and only if, `a` contains `elem`. So, (P1) is trivially satisfied.\n\n**Maintenance**: to prove the maintenance, we have to prove two things: a) that if `a` contains `elem` then `a(start..end)` also contains `elem`; and b) that if `a` does not contain `elem`, neither does `a(start..end)`. It is easy to see that part b) is true, because no matter what values we assign to start or end, they will define a subarray of `a`, even if that subarray is empty. So if `elem` is not in `a`, it cannot be in any subarray of `a`.\n\nPart a) is slightly more complex. For there to be a loop in the first place, the condition in line 6 has to be false (more on this in the next paragraph). In other words, `elem` is either greater than, or less than, the element in the middle (recall that the array is sorted). If it is greater, start will be updated to `mid + 1`, effectively dropping the first half of the array, so that, when line 4 is evaluated again, the interval will consist of the second half of the array. And it is at this point that the loop invariant is maintained. The first half of the array could not possibly contain `elem`, so if it is in the original array, it will also be in the second half, defined by the new values of start and end, satisfying (P1). For the case where `elem` is less than `a(mid)`, the proof is analogous.\n\n**Termination**: there are two possible situations in which the procedure stops: when condition in line 4 is false or condition in line 6 is true. Let’s start with the former. `start <= end` being false implies an empty array. By definition, empty arrays do not contain any element and, in particular, do not contain `elem`. So it will return -1, which is the correct result in this case. In the latter case, `elem == a(mid)` means that we have actually found the element we were looking for, and the result in this case is `mid`.\n\nEven though loop invariant proofs are mathematically precise techniques to show the correctness of an algorithm, they are somewhat cumbersome to work with, for two main reasons:\n\n 1. Time is not readily visible in the code. At some point in time, a set of variables may have some value and then in the next point in time, the *same* set of variables may have a different value.\n 2. Since variables are mutable, you have to keep track of all the updates these variables might go through, everywhere they are used. And if there is concurrency involved, you also have to keep track of how different threads or processes might interact when updating them, which may be unfeasible at scale.\n\n## Binary search – recursive version\nNow let’s look at a recursive version of the same algorithm:\n\n\tdef search[T <% Ordered[T]](a: Array[T], elem: T): Int = { \n\t  def doSearch(start: Int, end: Int): Int =\n\t    if (start > end) -1\n\t    else {\n\t      val mid = (start + end) / 2\n\t      if (elem == a(mid)) mid\n\t      else if (elem > a(mid)) doSearch(mid + 1, end)\n\t      else doSearch(start, mid - 1)\n\t    }\n\t  doSearch(0, a.length - 1)\n\t}\n\nIt is the same algorithm, with the same runtime complexity and even the same actual running time. What is different is the programming model. Instead of a machine that changes data in place, we can think of this function as a kind of generator of an immutable sequence of immutable states. The states, in this case, are the tuples (not in the sense of a Scala syntax construct, but in the more general sense of an ordered list of elements) that make up the function’s list of parameters. The function, in this case, is `doSearch()`.\n\nFor example, suppose you call the recursive function with these parameters:\n\n    val a = Array(4, 9, 28, 37, 40, 50, 52, 57, 60, 61, 68, 71, 74, 76, 82, 87, 92, 98)\n    val elem = 61\n    search(a, elem)\n\nThe sequence of states that comprise the execution of the algorithm for the input above is:\n\n(0, 17) → (9, 17) → (9, 12) → (9, 9)\n\nThe arrow represents a recursive call, that yields the next state. And every state in that sequence satisfies the property (P1). What we have here, then, is a *recursion invariant*, that is, an invariant property that is guaranteed to be preserved between recursive calls. The way to prove a recursion invariant is basically the same as we would a loop invariant: initiation, maintenance and termination. But instead of thinking in terms of how a loop changes certain variables, we think of states and the relationship between consecutive states.\n\nIn particular, we are interested in the first state (the initiation), the last state (the termination, which can be straightforwardly transformed to the final result) and the inductive step of generating a new state from the current state, assuming that the current one satisfies the invariant. No mutation of variables and no notion of time to worry about; just the sequence of states.\n\nAnd it gets even better: we don’t even need to think about the sequence itself. It suffices to establish the relationship between input and output. In terms of code, we have to establish the relationship between the first and second parameters in line 2 with the first and second parameters in lines 7 and 8.\n\nTo sum up, the next time you write code to solve some problem, try to think about what property your algorithm keeps throughout its execution. And, if possible, try to develop a (tail) recursive version of it, so that you can prove that it works with much more elegance and simplicity. The key to understand how an algorithm changes things is to observe what it *does not* change (more on this on a future post).\n\n[1]:  http://books.google.com.br/books?hl=en&lr=&id=NLngYyWFl_YC",
      "json_metadata": "{\"tags\":[\"mathematics\",\"algorithms\",\"functional-programming\",\"computer-science\"],\"links\":[\"http://books.google.com.br/books?hl=en&amp;lr=&amp;id=NLngYyWFl_YC\"]}",
      "parent_author": "",
      "parent_permlink": "computer-science",
      "permlink": "from-loop-invariants-to-recursion-invariants",
      "title": "From loop invariants to recursion invariants"
    }
  ],
  "op_in_trx": 0,
  "timestamp": "2016-08-24T08:34:42",
  "trx_id": "5dd6009af47b05d416d7238a656dfcdae506cdd9",
  "trx_in_block": 2,
  "virtual_op": 0
}

{
  "block": 4355836,
  "op": [
    "comment",
    {
      "author": "otaviomacedo",
      "body": "![Ouroboros](https://upload.wikimedia.org/wikipedia/commons/f/fa/Ouroboros.png)\n\nUntil very recently, the major commercial programming languages were based on the idea of update in place. C, C++, Pascal, Java etc presuppose that the way to solve a programming problem is to have procedures that read and write values to memory locations, be it directly visible to the programmer (by means of pointers) or not.\n\nOther languages, like Lisp, are based on a different assumption: that a computation is best expressed as a set of functions over immutable values. So, in order to produce any kind of repetitive computation, recursion is essential. This assumption has strong roots in lambda calculus and related mathematical formalisms.\n\nProbably due to the popularity of the procedural paradigm, most programmers find it easier to reason about loops than about recursion. But in order to reason effectively about a program, the functional model is far superior. This is what I intend to show in this post.\n\nProgramming models\n-----------------------------\nThe programming model behind procedural code is that of a machine that crunches data for some time and eventually stops. When it stops, we take a look at whatever came up from all this crunching and accept it as the result of the procedure. In some sense, this is the most natural model, since the underlying implementation of the algorithm runs on a real machine that does exactly that.\n\nThe problem is that it would be desirable to conduct some kind of formal reasoning about the code at hand. The same kind we use in mathematics, for example. But the machine model relies heavily on mutation of the contents of chunks of memory over time, which is not exactly amenable to a mathematical analysis.\n\nA neat solution to this problem is the use of loop invariants (cf. [“Introduction to Algorithms”][1]). A loop invariant is a logical predicate that we ascribe to an algorithm. That predicate remains true from the beginning to the end of the algorithm execution, including all the loops that are run, despite the fact that those loops might be changing things. Loop invariants have to take time into account (not clock time, but the discrete time defined by the sequence of operations made by the algorithm) and the values of the variables at each point in time.\n\nBinary search – iterative version\n-------------------------------------------\nLet’s take a simple and common example to illustrate the point: binary search. Given a sorted array and an element, the binary search algorithm returns the index of the element in the array, or -1 if the element is not found. Intuitively, what the algorithm does is: at each iteration, it cuts down the search space to a half, always looking at the element in the middle. The size of the search space tends to zero as the algorithm runs. So, either the element is eventually found or the search space becomes empty and the element can be declared not found. Here is an implementation of the algorithm in Scala:\n\n    def search[T <% Ordered[T]](a: Array[T], elem: T): Int = {\n      var start = 0\n      var end = a.length - 1\n      while (start <= end) { \n        val mid = (start + end) / 2\n        if (elem == a(mid)) return mid \n        else if (elem > a(mid)) start = mid + 1\n        else end = mid - 1\n      }\n      -1\n    }\nWe can prove the intuition behind binary search using loop invariants. The property that remains true throughout its execution is:\n\n> The subarray a(start..end) contains elem if, and only if, a contains elem. (P1)\n\nNote that we are abusing the Scala notation a bit here, when we use `a(i..j)` to indicate a subarray of a from `i` to `j`, inclusive on both ends.\n\n### Proof\n\nLoop invariants have to be proved in three main sections: *initiation* (the initial values assigned to the variables satisfy the property), *maintenance* (at the beginning of each loop, the property is satisfied) and *termination* (when the algorithm stops, what it returns matches up with the expected result). So, here are the three sections for the iterative version of the binary search algorithm:\n\n**Initiation**: lines 2 and 3 define an interval that comprises the whole array, which is equivalent to say that `a` contains `elem` if, and only if, `a` contains `elem`. So, (P1) is trivially satisfied.\n\n**Maintenance**: to prove the maintenance, we have to prove two things: a) that if `a` contains `elem` then `a(start..end)` also contains `elem`; and b) that if `a` does not contain `elem`, neither does `a(start..end)`. It is easy to see that part b) is true, because no matter what values we assign to start or end, they will define a subarray of `a`, even if that subarray is empty. So if `elem` is not in `a`, it cannot be in any subarray of `a`.\n\nPart a) is slightly more complex. For there to be a loop in the first place, the condition in line 6 has to be false (more on this in the next paragraph). In other words, `elem` is either greater than, or less than, the element in the middle (recall that the array is sorted). If it is greater, start will be updated to `mid + 1`, effectively dropping the first half of the array, so that, when line 4 is evaluated again, the interval will consist of the second half of the array. And it is at this point that the loop invariant is maintained. The first half of the array could not possibly contain `elem`, so if it is in the original array, it will also be in the second half, defined by the new values of start and end, satisfying (P1). For the case where `elem` is less than `a(mid)`, the proof is analogous.\n\n**Termination**: there are two possible situations in which the procedure stops: when condition in line 4 is false or condition in line 6 is true. Let’s start with the former. `start <= end` being false implies an empty array. By definition, empty arrays do not contain any element and, in particular, do not contain `elem`. So it will return -1, which is the correct result in this case. In the latter case, `elem == a(mid)` means that we have actually found the element we were looking for, and the result in this case is `mid`.\n\nEven though loop invariant proofs are mathematically precise techniques to show the correctness of an algorithm, they are somewhat cumbersome to work with, for two main reasons:\n\n 1. Time is not readily visible in the code. At some point in time, a set of variables may have some value and then in the next point in time, the *same* set of variables may have a different value.\n 2. Since variables are mutable, you have to keep track of all the updates these variables might go through, everywhere they are used. And if there is concurrency involved, you also have to keep track of how different threads or processes might interact when updating them, which may be unfeasible at scale.\n\n## Binary search – recursive version\nNow let’s look at a recursive version of the same algorithm:\n\n\tdef search[T <% Ordered[T]](a: Array[T], elem: T): Int = { \n\t  def doSearch(start: Int, end: Int): Int =\n\t    if (start > end) -1\n\t    else {\n\t      val mid = (start + end) / 2\n\t      if (elem == a(mid)) mid\n\t      else if (elem > a(mid)) doSearch(mid + 1, end)\n\t      else doSearch(start, mid - 1)\n\t    }\n\t  doSearch(0, a.length - 1)\n\t}\n\nIt is the same algorithm, with the same runtime complexity and even the same actual running time. What is different is the programming model. Instead of a machine that changes data in place, we can think of this function as a kind of generator of an immutable sequence of immutable states. The states, in this case, are the tuples (not in the sense of a Scala syntax construct, but in the more general sense of an ordered list of elements) that make up the function’s list of parameters. The function, in this case, is `doSearch()`.\n\nFor example, suppose you call the recursive function with these parameters:\n\n    val a = Array(4, 9, 28, 37, 40, 50, 52, 57, 60, 61, 68, 71, 74, 76, 82, 87, 92, 98)\n    val elem = 61\n    search(a, elem)\n\nThe sequence of states that comprise the execution of the algorithm for the input above is:\n\n(0, 17) → (9, 17) → (9, 12) → (9, 9)\n\nThe arrow represents a recursive call, that yields the next state. And every state in that sequence satisfies the property (P1). What we have here, then, is a *recursion invariant*, that is, an invariant property that is guaranteed to be preserved between recursive calls. The way to prove a recursion invariant is basically the same as we would a loop invariant: initiation, maintenance and termination. But instead of thinking in terms of how a loop changes certain variables, we think of states and the relationship between consecutive states.\n\nIn particular, we are interested in the first state (the initiation), the last state (the termination, which can be straightforwardly transformed to the final result) and the inductive step of generating a new state from the current state, assuming that the current one satisfies the invariant. No mutation of variables and no notion of time to worry about; just the sequence of states.\n\nAnd it gets even better: we don’t even need to think about the sequence itself. It suffices to establish the relationship between input and output. In terms of code, we have to establish the relationship between the first and second parameters in line 2 with the first and second parameters in lines 7 and 8.\n\nTo sum up, the next time you write code to solve some problem, try to think about what property your algorithm keeps throughout its execution. And, if possible, try to develop a (tail) recursive version of it, so that you can prove that it works with much more elegance and simplicity. The key to understand how an algorithm changes things is to observe what it *does not* change (more on this on a future post).\n\n[1]:  http://books.google.com.br/books?hl=en&lr=&id=NLngYyWFl_YC",
      "json_metadata": "{\"tags\":[\"mathematics\",\"computer-science\",\"algorithms\",\"functional-programming\"],\"links\":[\"http://books.google.com.br/books?hl=en&amp;lr=&amp;id=NLngYyWFl_YC\"]}",
      "parent_author": "",
      "parent_permlink": "computer-science",
      "permlink": "from-loop-invariants-to-recursion-invariants",
      "title": "From loop invariants to recursion invariants"
    }
  ],
  "op_in_trx": 0,
  "timestamp": "2016-08-24T08:34:24",
  "trx_id": "91b29270267ac35307cb015196929030568d5276",
  "trx_in_block": 1,
  "virtual_op": 0
}

{
  "block": 4355808,
  "op": [
    "comment",
    {
      "author": "otaviomacedo",
      "body": "@@ -4379,17 +4379,19 @@\n that if \n-a\n+%60a%60\n  contain\n@@ -4939,17 +4939,8 @@\n her \n-strictly \n grea\n@@ -4957,27 +4957,20 @@\n or less \n-or equal to\n+than\n , the el\n@@ -5524,19 +5524,12 @@\n ess \n-or equal to\n+than\n  %60a(\n@@ -5638,15 +5638,13 @@\n ure \n-to \n stop\n+s\n : wh\n@@ -5744,16 +5744,17 @@\n %60start %3C\n+=\n  end%60 be\n@@ -5877,20 +5877,22 @@\n contain \n+%60\n elem\n+%60\n . So it \n@@ -7705,16 +7705,61 @@\n ameters.\n-\n \n+ The function, in this case, is %60doSearch()%60.\n %0A%0AFor ex\n@@ -8653,16 +8653,20 @@\n lar, we \n-\n \n+are \n interest\n@@ -9588,17 +9588,16 @@\n ith much\n-o\n \n+\n  more el\n",
      "json_metadata": "{\"tags\":[\"computer-science\",\"algorithms\",\"functional-programming\"],\"links\":[\"http://books.google.com.br/books?hl=en&lr=&id=NLngYyWFl_YC\"]}",
      "parent_author": "",
      "parent_permlink": "computer-science",
      "permlink": "from-loop-invariants-to-recursion-invariants",
      "title": "From loop invariants to recursion invariants"
    }
  ],
  "op_in_trx": 0,
  "timestamp": "2016-08-24T08:33:00",
  "trx_id": "95854a289c5357d4ec7658092e8d29008f98bf08",
  "trx_in_block": 3,
  "virtual_op": 0
}

{
  "block": 4336210,
  "op": [
    "vote",
    {
      "author": "otaviomacedo",
      "permlink": "from-loop-invariants-to-recursion-invariants",
      "voter": "stevo",
      "weight": 10000
    }
  ],
  "op_in_trx": 0,
  "timestamp": "2016-08-23T16:06:51",
  "trx_id": "cf7d2bb83d026d610f1740120ee88dd9f0dbe824",
  "trx_in_block": 2,
  "virtual_op": 0
}

{
  "block": 4335915,
  "op": [
    "comment",
    {
      "author": "otaviomacedo",
      "body": "@@ -1,8 +1,89 @@\n+!%5BOuroboros%5D(https://upload.wikimedia.org/wikipedia/commons/f/fa/Ouroboros.png)%0A%0A\n Until ve\n",
      "json_metadata": "{\"tags\":[\"computer-science\",\"algorithms\",\"functional-programming\"],\"links\":[\"http://books.google.com.br/books?hl=en&lr=&id=NLngYyWFl_YC\"]}",
      "parent_author": "",
      "parent_permlink": "computer-science",
      "permlink": "from-loop-invariants-to-recursion-invariants",
      "title": "From loop invariants to recursion invariants"
    }
  ],
  "op_in_trx": 0,
  "timestamp": "2016-08-23T15:51:57",
  "trx_id": "3669bb5ec25cb4a5fa038776f98e22d6d03a88a5",
  "trx_in_block": 1,
  "virtual_op": 0
}

{
  "block": 4335755,
  "op": [
    "vote",
    {
      "author": "otaviomacedo",
      "permlink": "from-loop-invariants-to-recursion-invariants",
      "voter": "otaviomacedo",
      "weight": 10000
    }
  ],
  "op_in_trx": 0,
  "timestamp": "2016-08-23T15:43:54",
  "trx_id": "d0403d79b9cb013114ef3c68b2606eb898267bec",
  "trx_in_block": 0,
  "virtual_op": 0
}

{
  "block": 4335755,
  "op": [
    "comment",
    {
      "author": "otaviomacedo",
      "body": "Until very recently, the major commercial programming languages were based on the idea of update in place. C, C++, Pascal, Java etc presuppose that the way to solve a programming problem is to have procedures that read and write values to memory locations, be it directly visible to the programmer (by means of pointers) or not.\n\nOther languages, like Lisp, are based on a different assumption: that a computation is best expressed as a set of functions over immutable values. So, in order to produce any kind of repetitive computation, recursion is essential. This assumption has strong roots in lambda calculus and related mathematical formalisms.\n\nProbably due to the popularity of the procedural paradigm, most programmers find it easier to reason about loops than about recursion. But in order to reason effectively about a program, the functional model is far superior. This is what I intend to show in this post.\n\nProgramming models\n-----------------------------\nThe programming model behind procedural code is that of a machine that crunches data for some time and eventually stops. When it stops, we take a look at whatever came up from all this crunching and accept it as the result of the procedure. In some sense, this is the most natural model, since the underlying implementation of the algorithm runs on a real machine that does exactly that.\n\nThe problem is that it would be desirable to conduct some kind of formal reasoning about the code at hand. The same kind we use in mathematics, for example. But the machine model relies heavily on mutation of the contents of chunks of memory over time, which is not exactly amenable to a mathematical analysis.\n\nA neat solution to this problem is the use of loop invariants (cf. [“Introduction to Algorithms”][1]). A loop invariant is a logical predicate that we ascribe to an algorithm. That predicate remains true from the beginning to the end of the algorithm execution, including all the loops that are run, despite the fact that those loops might be changing things. Loop invariants have to take time into account (not clock time, but the discrete time defined by the sequence of operations made by the algorithm) and the values of the variables at each point in time.\n\nBinary search – iterative version\n-------------------------------------------\nLet’s take a simple and common example to illustrate the point: binary search. Given a sorted array and an element, the binary search algorithm returns the index of the element in the array, or -1 if the element is not found. Intuitively, what the algorithm does is: at each iteration, it cuts down the search space to a half, always looking at the element in the middle. The size of the search space tends to zero as the algorithm runs. So, either the element is eventually found or the search space becomes empty and the element can be declared not found. Here is an implementation of the algorithm in Scala:\n\n    def search[T <% Ordered[T]](a: Array[T], elem: T): Int = {\n      var start = 0\n      var end = a.length - 1\n      while (start <= end) { \n        val mid = (start + end) / 2\n        if (elem == a(mid)) return mid \n        else if (elem > a(mid)) start = mid + 1\n        else end = mid - 1\n      }\n      -1\n    }\nWe can prove the intuition behind binary search using loop invariants. The property that remains true throughout its execution is:\n\n> The subarray a(start..end) contains elem if, and only if, a contains elem. (P1)\n\nNote that we are abusing the Scala notation a bit here, when we use `a(i..j)` to indicate a subarray of a from `i` to `j`, inclusive on both ends.\n\n### Proof\n\nLoop invariants have to be proved in three main sections: *initiation* (the initial values assigned to the variables satisfy the property), *maintenance* (at the beginning of each loop, the property is satisfied) and *termination* (when the algorithm stops, what it returns matches up with the expected result). So, here are the three sections for the iterative version of the binary search algorithm:\n\n**Initiation**: lines 2 and 3 define an interval that comprises the whole array, which is equivalent to say that `a` contains `elem` if, and only if, `a` contains `elem`. So, (P1) is trivially satisfied.\n\n**Maintenance**: to prove the maintenance, we have to prove two things: a) that if a contains `elem` then `a(start..end)` also contains `elem`; and b) that if `a` does not contain `elem`, neither does `a(start..end)`. It is easy to see that part b) is true, because no matter what values we assign to start or end, they will define a subarray of `a`, even if that subarray is empty. So if `elem` is not in `a`, it cannot be in any subarray of `a`.\n\nPart a) is slightly more complex. For there to be a loop in the first place, the condition in line 6 has to be false (more on this in the next paragraph). In other words, `elem` is either strictly greater than, or less or equal to, the element in the middle (recall that the array is sorted). If it is greater, start will be updated to `mid + 1`, effectively dropping the first half of the array, so that, when line 4 is evaluated again, the interval will consist of the second half of the array. And it is at this point that the loop invariant is maintained. The first half of the array could not possibly contain `elem`, so if it is in the original array, it will also be in the second half, defined by the new values of start and end, satisfying (P1). For the case where `elem` is less or equal to `a(mid)`, the proof is analogous.\n\n**Termination**: there are two possible situations in which the procedure to stop: when condition in line 4 is false or condition in line 6 is true. Let’s start with the former. `start < end` being false implies an empty array. By definition, empty arrays do not contain any element and, in particular, do not contain elem. So it will return -1, which is the correct result in this case. In the latter case, `elem == a(mid)` means that we have actually found the element we were looking for, and the result in this case is `mid`.\n\nEven though loop invariant proofs are mathematically precise techniques to show the correctness of an algorithm, they are somewhat cumbersome to work with, for two main reasons:\n\n 1. Time is not readily visible in the code. At some point in time, a set of variables may have some value and then in the next point in time, the *same* set of variables may have a different value.\n 2. Since variables are mutable, you have to keep track of all the updates these variables might go through, everywhere they are used. And if there is concurrency involved, you also have to keep track of how different threads or processes might interact when updating them, which may be unfeasible at scale.\n\n## Binary search – recursive version\nNow let’s look at a recursive version of the same algorithm:\n\n\tdef search[T <% Ordered[T]](a: Array[T], elem: T): Int = { \n\t  def doSearch(start: Int, end: Int): Int =\n\t    if (start > end) -1\n\t    else {\n\t      val mid = (start + end) / 2\n\t      if (elem == a(mid)) mid\n\t      else if (elem > a(mid)) doSearch(mid + 1, end)\n\t      else doSearch(start, mid - 1)\n\t    }\n\t  doSearch(0, a.length - 1)\n\t}\n\nIt is the same algorithm, with the same runtime complexity and even the same actual running time. What is different is the programming model. Instead of a machine that changes data in place, we can think of this function as a kind of generator of an immutable sequence of immutable states. The states, in this case, are the tuples (not in the sense of a Scala syntax construct, but in the more general sense of an ordered list of elements) that make up the function’s list of parameters.\n\nFor example, suppose you call the recursive function with these parameters:\n\n    val a = Array(4, 9, 28, 37, 40, 50, 52, 57, 60, 61, 68, 71, 74, 76, 82, 87, 92, 98)\n    val elem = 61\n    search(a, elem)\n\nThe sequence of states that comprise the execution of the algorithm for the input above is:\n\n(0, 17) → (9, 17) → (9, 12) → (9, 9)\n\nThe arrow represents a recursive call, that yields the next state. And every state in that sequence satisfies the property (P1). What we have here, then, is a *recursion invariant*, that is, an invariant property that is guaranteed to be preserved between recursive calls. The way to prove a recursion invariant is basically the same as we would a loop invariant: initiation, maintenance and termination. But instead of thinking in terms of how a loop changes certain variables, we think of states and the relationship between consecutive states.\n\nIn particular, we interested in the first state (the initiation), the last state (the termination, which can be straightforwardly transformed to the final result) and the inductive step of generating a new state from the current state, assuming that the current one satisfies the invariant. No mutation of variables and no notion of time to worry about; just the sequence of states.\n\nAnd it gets even better: we don’t even need to think about the sequence itself. It suffices to establish the relationship between input and output. In terms of code, we have to establish the relationship between the first and second parameters in line 2 with the first and second parameters in lines 7 and 8.\n\nTo sum up, the next time you write code to solve some problem, try to think about what property your algorithm keeps throughout its execution. And, if possible, try to develop a (tail) recursive version of it, so that you can prove that it works with mucho more elegance and simplicity. The key to understand how an algorithm changes things is to observe what it *does not* change (more on this on a future post).\n\n[1]:  http://books.google.com.br/books?hl=en&lr=&id=NLngYyWFl_YC",
      "json_metadata": "{\"tags\":[\"computer-science\",\"algorithms\",\"functional-programming\"],\"links\":[\"http://books.google.com.br/books?hl=en&amp;lr=&amp;id=NLngYyWFl_YC\"]}",
      "parent_author": "",
      "parent_permlink": "computer-science",
      "permlink": "from-loop-invariants-to-recursion-invariants",
      "title": "From loop invariants to recursion invariants"
    }
  ],
  "op_in_trx": 0,
  "timestamp": "2016-08-23T15:43:54",
  "trx_id": "d0403d79b9cb013114ef3c68b2606eb898267bec",
  "trx_in_block": 0,
  "virtual_op": 0
}

{
  "block": 4335341,
  "op": [
    "account_create",
    {
      "active": {
        "account_auths": [],
        "key_auths": [
          [
            "STM8e8o2NLAgTB6e4LMAdVETJuZRphY893miuyjbVkDzXExSX8WjJ",
            1
          ]
        ],
        "weight_threshold": 1
      },
      "creator": "steem",
      "fee": "3.000 STEEM",
      "json_metadata": "",
      "memo_key": "STM5gj8gocRxXTRMhZ4rZtLDAoZss6tPxyAiCLaLPcKQKxxfPCMY1",
      "new_account_name": "otaviomacedo",
      "owner": {
        "account_auths": [],
        "key_auths": [
          [
            "STM6FtGn6U18byMBZczwCg13ynHEWKeAodoPbnRQPdSv5ruYgMt2M",
            1
          ]
        ],
        "weight_threshold": 1
      },
      "posting": {
        "account_auths": [],
        "key_auths": [
          [
            "STM7SE8DcdLXPwvNXCKmS6ewbwLKwTqr1eDB24cGcSLyiUvDMqbba",
            1
          ]
        ],
        "weight_threshold": 1
      }
    }
  ],
  "op_in_trx": 0,
  "timestamp": "2016-08-23T15:23:00",
  "trx_id": "ab1a43f574c228e4cc92850880f4980ddb210b4c",
  "trx_in_block": 0,
  "virtual_op": 0
}