# Tag Info

12

Your description of your algorithm is really too vague to evaluate it at this point. But, here are some things to consider. CPS In fact, there is a way to transform any code into a form that uses only tail-calls. This is the CPS transform. CPS (Continuation-Passing Style) is a form of expressing code by passing each function a continuation. A ...

6

In PL theory, this is known as (a variant of) the Church-encoding of pairs. The idea is the following: assume for the moment you only have a language with primitive booleans (true, false, if-then-else) and primitive (first-class) functions. Pairs are not primitive, yet they can be encoded as follows. In place of a pair $(x,y)$ we can consider the ...

6

"Old" programming languages like Fortran, Cobol and LISP arose before serious mathematical theory of programming languages was developed. They inspired the development of such theory, but are full of idiosyncracies and features which from a mathematical point of view can best be described as "warts". However, each of the old languages in essence has a ...

6

Let me try to clarify a point that seems to be confusing you: you seem to be conflating 2 related, but different concepts. The first is the concept of a proof system, which allows you to specify and prove theorems about mathematics or computer science. Dependent types are one elegant way to do this, where the types are the specification language and the ...

4

Dependent Types in Racket are being worked on by Andrew Kent at Indiana University. There is a set of slides. There is a talk. Of interest, this potentially also impacts Typed Clojure, which is strongly modeled on Typed Racket.

3

Your induction step is recorded incorrectly. You wrote: $$\frac{x^{k+1} - 1}{x - 1} + k+1$$ You should have written: $$\frac{x^{k+1} - 1}{x - 1} + x^{k+1}$$ Basically, you are proving the formula for the sum of the geometric sequence.

2

With fact, the primary problem is with f. If n is 0, then it works fine. However, for any other value of n, fact is called with an f of () => n * f(). So when the base case (n = 0) is finally encountered, f is () => n * f(). When f is invoked, f is still () => n * f(). So the call to f results in unbounded recursion with itself. With ...

1

The thing to notice here is that your function sum is defined on lists, which are inductively defined. Theoretically, the inductive definition of a list defines for every type T a term match_list :: T -> (a -> [a] -> T) -> ([a] -> T) satisfying the property match_list s t [] = s match_list s t (x::xs) = (t x xs) in addition, defining a ...

1

Given your definition, the answer is "no". JavaScript syntax is not a subset of JavaScript's literal syntax. The fact that a value a literal represents can be produced by evaluating the literal is what makes a literal a literal and is true in any language. The only real difference is JavaScript has a richer literal syntax than many common programming ...

1

The intersection rule should be derivable, but it isn't purely a subtyping rule. Basically we reason as follows (I've translated into a notation that's a bit more familiar to me): I'm presuming that subtyping says $A \cap B \subseteq A \subseteq A \cup B$ Subtyping means that $f : (A \to Y) \cap (B \to X)$ leads to both $f : A \to Y$ and $f : B \to X$ If \$f ...

1

In programming languages I 've seen, they are not the same. A procedure (or function) definition is a block of code with a header, that specifies 0 or more arguments, and a name. It allows the procedure to be called by specifying its name and a list of argument values. In many languages, anonymous functions or procedures can be defined, which have a block ...

1

OK, I found a lead. Just needed to know what to search for: https://en.wikipedia.org/wiki/CAR_and_CDR The 704 and its successors has a 36-bit word length and a 15-bit address space. These computers had two instruction formats, one of which, the Type A, had a short, 3-bit, operation code prefix and two 15-bit fields separated by a 3-bit tag. The first 15-...

1

The 16 high-speed registers of the PDP-10 ISA were addressible as locations 0-15 of physical memory, so that the code literally could run in the registers if it was short enough and you could devote a block of registers to it. Not only could it use registers for temporary storage, it could use them as a code cache as well.

1

Project Euler has nice problems for showcasing the core of a programming language. An important part of a programming language are user defined (container) data structures. Bread and butter containers include random access arrays, bidirectional lists, hash tables, and search trees. You may take the implementations from standard libraries of the languages to ...

1

You get the fib(n) running time if you only expand one invocation of fib at a time. You haven't been told the exact execution model for several reasons: It is messy. It's not important. It could depend on the implementation. You need to worry about low-level stuff such as the complexity of integer operations. The reason it's not important is that when ...

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