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
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 ...
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 ...
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 modelled 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
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
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
