4

Two-dimensional arrays are stored as one-dimensional arrays. Your first array is stored as $$ A[1,1], A[1,2], A[2,1], A[2,2], A[3,1], A[3,2], $$ so the offset of $A[x,y]$ is $2x+y-3$. In contrast, the third array is stored as $$ A[1,1], A[1,2], A[1,3], A[2,1], A[2,2], A[2,3], $$ so the offset of $A[x,y]$ is $3x+y-4$. Multiplying by 2 could be faster than ...


3

If you regard the output of a program as a function of its input then matrices can be used to represent some programs, namely those where the output is a linear function of the input. So a program that takes two arguments $a$ and $b$ and returns $a+b$ and $a-b$ could be represented by the matrix $\begin{pmatrix} 1 & 1 \\ 1 & -1 \end{pmatrix}$ But ...


3

Unfortunately I don't have a copy of TAPL with me, so I can't figure out exactly what the author intends. But there is a point we should make, that types are something which classifies terms or values, even if there are other pieces that are related to the type. As such, classes and interfaces are not literally types themselves in Java or C++. Rather, each ...


2

I'm not confident enough about the later questions, but I hope I can give a partial answer, since this hasn't been given much love. Yes Yes There is nothing in particular, since first-order logic quantifies over non-logical objects, but a priori there are no non-logical objects we're reasoning about for the lambda calculus. There is a similar-sounding type ...


2

As an example where unbounded loops are needed: I can write an emulator for any machine, running in a loop. With unbounded loops, that emulator can run forever. With bounded loops, I must calculate beforehand how long that emulator runs. That calculation might return "the simulator will run for one trillion trillion trillion years", which in theory makes a ...


2

Real world computers are not Turing complete (they have a finite amount of memory) and are equiparable to Linear Bounded Automata. So the easiest way to design a non-Turing-complete language is to design a language that has only a limited amount of memory (the memory can also be a function of the input length) and don't worry about other restrictions. But ...


1

By being corecursive between the types, you indeed get a representation of a grammar, and it does have binding. But now you've sort of "baked in" the unembedding by making it "definitionally id". (This is similar to the Place constructor in Fegaras and Sheard). So you can evaluate to Value. But what if you want to evaluate to anything else? You can't, ...


1

Yes, in that context Hindley-Milner polymorphism is let-polymorphism, since such language uses $\sf let$ to introduce polymorphic functions. In the untyped lambda calculus, we can consider a (non recursive) ${\sf let}\ x = e \ {\sf in}\ t$ to be syntactic sugar for $(\lambda x.t)e$. In System F, where polymorphism is introduced by explicit $\Lambda \alpha$ ...


1

Consider the following program: f1(); f2(); If local variables are allocated statically, there's a space in memory that's reserved for the local variables of f1, and a separate space for the local variables of f2. If f1 needs $n_1$ bytes of memory for its local variables and f2 needs $n_2$ bytes, the program above needs $n_1 + n_2$ bytes. If local ...


1

There is just nothing that you can generalise. Every language is different. A class describes what instances of the class (objects) look like. In Java, a class is also an object in its own right. All classes are instances of a class named "class", which allows the programmer to ask the class for example "what is your name", "what are the instance variables ...


1

Perhaps, a model checker may be helpful. http://alloytools.org/documentation.html Alloy is a model checker. A nice presentation explaining the concept of model checking using Alloy: https://www.youtube.com/watch?v=FvNRlE4E9QQ In the same family of tools comes 'property-based testing', they all try to find a counter-example for the given specification ...


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