11

If it is only the third chapter, I doubt the authors have covered dynamic programming, but I will illustrate what is going on when a for loop is used to compute the $n^\text{th}$ Fibonacci number, $F_n$. Recall the definition, $$F_n = \begin{cases} 0 & n = 0\\ 1 & n = 1\\ F_{n-1} + F_{n - 2} & \text{otherwise} \end{cases}$$ We could naively ...


10

I don't know Brainfuck so you'll have to do some translation from my pseudocode. But, assuming that Brainfuck behaves sensibly (ha!), everything below should apply. do-while is equivalent to while-do. do X while Y is equivalent to X; while Y do X and, assuming you have conditionals, while Y do X is equivalent to if Y then (do X while Y). Life is a bit ...


10

If you only have to use a for loop that iterates until it finds the n-th Fibonacci number, you could use something like this: int fib(int n) { int p = 0; int c = 1; int r = 0; // The result is initialized to 0 (undefined). for (int i = 0; i < n; i++) { r = p + c; // Produce next number in the sequence. p = c; // ...


9

If we peel off the syntactic sugar on the front and the code generation on the back and compare what happens in between when converting source to running code for imperative languages, such as C or Java with functional languages such as ML or OCaml we will generally find the following differences in what, why, and how. Mutable vs. immutable With functional ...


8

The simplest kind of state is the configuration of memory. In C this memory is accessed through variables (and arrays and pointers, but let us ignore those), so the state is the values of variables. For example, suppose we have variables x and y whose values are 23 and 42 respectively (and no other variables). Then we could write the state as $$[x \mapsto ...


8

A functional programming language is notable for what it prohibits. It prohibits modifying an existing variable or data structure. You can program in a "functional style" in some imperative programming languages, but the language won't protect you from accidentally modifying an existing variable or data structure. For example, here is a recursive, ...


7

I think what you want is essentially conversion to static single assignment (SSA) form, followed by closure conversion, followed by conversion to continuation passing style. Static single assignment form guarantees that each variable is written exactly once in the program text. That this is the key step in converting imperative to functional programs is ...


7

Your example of "functional programming" is a pretty poor one. For starters, it is not functional because it uses state (it stores something in words and behind the scenes set(words) is doing stateful stuff as well). To actually learn what functional programming is about, you should look outside an imperative language such as Python. Python often uses ...


5

Since the question does not fully describe the language, I assume the simpler case when the $\texttt{++}$ operator applies only to variables given by an identifier, for example: $\texttt{foo++}$. Short of having more examples of the way you write denotational semantic, I have to improvise a bit. In particular, I avoid lambda notation since I do not know ...


4

This trace is possible, in two separate threads T1 and T2. $state$ is $(x,y)$. T1: ... $state=(0, 4)$ T1: x = x + 1; y = y - 1 $~~state=(1, 3)$ T1: x = x + 1; y = y - 1 $~~state=(2, 2)$ T2: x == y evaluates to true, pass and then x = 0; $~~state=(0, 2)$ T1: x != y evaluates to true, x = x + 1; y = y - 1 $~~state=(1, 1)$ T2: y = 2 $~~state=(1, 2)$ T1: x != y ...


4

The real answer is that the designers of those languages chose not to include it. It's certainly technically possible. As has been said in the comments, Rust does, Java does, C# does, etc. However, there are some difficulties. The first is in the choice of impelemtation strategy. Polymorphism is easy if you're working with Lambda Calculi and looking only ...


3

Yes. There are problems where we can prove there is a $\Omega(\lg \lg n)$ factor slowdown. We also know that the slowdown is at most $O(\lg n)$ in all cases. See What classes of data structures can be made persistent?.


3

The state monad allows us to translate any stateful (you call it "mutable") program to a pure one. The changes required to the program are "local" in the sense that you only need to make superficial changes to the syntax, assuming you use Haskell-style do notation. For example, the following is the Haskell translation of your program into a pure program: do ...


3

So, it's possible, but there are certainly some barriers: What kinds of expressions are allowed in types? What does it mean for a type to have a side-effect? Can typrchecking my program perform IO? Just because dependent types are in the system doesn't mean they provide a type safe language. It may be possible to produce proofs of False if the underlying ...


3

At a high enough level and when contrasted with functional programming, sure. Turing machine models and imperative programs have in common that they start from an input and take a series of steps that change a state stored in memory, ending with some output. This contrasts with lambda calculus and functional programming which generally and loosely do not ...


3

Not that I know of, but "stateful function" is reasonably descriptive. In informal conversation, that's what I'd use, as long as I suspect the audience will understand what I mean. In formal writing, I might still use the same phrase but also provide a careful definition of what I meant by that phrase. Really, that's a large part of what "formal" writing ...


2

There isn't a single loop invariant: any property that remains true during the execution of the loop is a loop invariant. For example, “I am not the Pope” is an invariant of this loop, but it is not a useful one. A useful loop invariant is one that helps in proving some property of the program. Here, presumably, the ultimate point of the exercise is to ...


2

The triple $\{Q\}C\{X\}$ states that if $Q$ holds, then after executing $C$, the condition $X$ holds. Now suppose that $\{Q\}C\{X\}$ and that $P \Longrightarrow Q$. We will prove that $\{P\}C\{X\}$. Indeed, suppose that $P$ holds. Since $P \Longrightarrow Q$, also $Q$ holds. Hence if we execute $C$, then $X$ will hold. Altogether, we see that $\{P\}C\{X\}$ ...


2

I recommend that you translate while(c) b to def myWhile() = if (c) then (b ; myWhile()) myWhile() With this translation, the precondition of myWhile is the loop invariant of the original while loop. So, this becomes the question of how to find the loop invariant of a loop. In general, that requires manual annotation. If you do a search, you should be ...


2

There are two related concepts called "idempotence" in programming. One is the mathematical one that quicksort and Raphael talk about. Namely, given a mathematical function $f$, $f$ is idempotent if $f(f(x))=f(x)$. Or more algebraically, $f\circ f = f$. The other notion that's common in practice and particularly for distributed computations is if an ...


1

Another answer is that imperative (updatable) data structures can be used in pure functional program via monads (such as Haskell ST monad) or unique types (in Clean).


1

The state of a program is all the information that is needed at runtime to determine what each line does. Consider a simple example that needs no state: printf("%d", 1 + 1); What is the effect of this line? Obviously it prints the number 2. But what about this example: printf("%d", x + 1); Now it's not so clear what this line does. The number printed ...


1

Idempotence is a concept that applies to mathematical functions. Since functions in imperative programming languages can have side effects, the concept is not well defined. In programming languages that allow to define functions without side effects (such as purely functional languages), the definition is exactly the same as the mathematical one, i.e. $f$ ...


1

As others have pointed out, there is nothing preventing an imperative language from using something similar to the Hindley-Milner type system and providing parametric polymorphism. I should point out that something very similar can actually be done in C, through use of the _Generic keyword which provides compile-time polymorphism / type inference. In the ...


1

In the realm of functional programing, functions that give the same result when called with the same arguments are usually called pure. The Wikipedia page explicitly adds the condition that mutable variables should not be modified by the function call, though presumably they mean mutable variables that can be observed outside of the function scope which ...


1

Denotational Semantics was an answer almost intended for your question There is a huge collection of techniques that may be applicable, since the proposed task is basically a compilation process, possibly partial / incremental compilation. The target language is domain extended λ-calculus, which imply some standard transformations such as continuations or ...


Only top voted, non community-wiki answers of a minimum length are eligible