10

There is a naive algorithm for programs with bounded-size inputs: enumerate all programs in order of increasing length (or execution time, which is a bounded function of the length). If you can prove that the program is equivalent to the original, stop; otherwise keep searching. This algorithm is sound. In order for it to be complete, you need to be able to ...


8

Implicit Complexity has taught us that (some) complexity classes can be classified by type systems, in the sense that there are type systems that only accept polynomial programs, for example. One more practical-minded offshoot of this research is RAML (Resource Aware ML), a functional programming language with a type system that will give you precise ...


8

I assume you are asking whether a "reasonable" system exists that can express these functions and also also decide whether any two expressible function definitions define the same function. (An unreasonable system would be, for example, the language which has only the two function definitions above in it...) Both of functions are expressible in Buss's ...


7

In the strictest sense, there is no real difference between syntax errors and semantics errors, at least as far as language theory is concerned: the only salient difference is the complexity of the automaton required to recognize that language, with, e.g. Context-free languages only requiring pushdown automata (PDA) General recursive languages requiring ...


7

@xuq01's guess is (extremely surprisingly!) wrong. The CBV eta rule described in the question is sound in Standard ML: the value v is contextually equivalent to fn x => v x. There are two caveats to this. First, in specific implementations this equivalence might not be sound: in SML/NJ, you could use Unsafe.cast to detect physical equality of function ...


7

The COSTA tool developed by the COSTA research group does exactly what you want. Given a program (in Java bytecode format), the tool produces a cost equation based on a cost model provided by the programmer. The cost model can involve entities such as runtime, memory usage, or billable events (such as sending text messages). The runtime equation is then ...


6

One approach is described by Georgios Fourtounis and Nikolaos S. Papaspyrou. 2013. Supporting Separate Compilation in a Defunctionalizing Compiler. SLATE 2013. As @gasche mentions: A different approach at the problem would be to consider that each module can define its own "defunctionalized functions" type and dispatcher/handler. You can "link" those ...


6

One example where commutativity helps is in computing the determinant. Nisan showed that any non-commutative algebraic formula that computes the $n \times n$ determinant must have size $2^{\Omega(n)}$. On the other hand, the determinant is computable by commutative algebraic formulas of size $n^{O(\log n)}$.


4

Adding to shaunc's answer: the first program (idealized over integers rather than "machine" integers) is a linear recurrence, and it turns out there are some very general methods for solving those: http://en.wikipedia.org/wiki/Recurrence_relation#Solving Note that this is similar to a discrete version of differential equations, so things get complicated ...


4

Read the post you are linking to. It's explained there in quite some detail. It's a consequence of the C++ spec, as Neel Krishnaswami explains. The very first sentence of the blog post says "Obviously I’m not serious". That should have been a tip-off right there. The post then goes on to say "What is really going on here..." and explains what's going on....


3

I assume you're looking for ways to compute the Control Flow Graph of a given program. This graph depends (obviously) on the actual operational semantics of the language you are interested in, and so cannot be computed from the AST alone, in the sense that some knowledge of the language semantics themselves are needed. For a given language it is possible ...


3

Actually, optimizing compilers do that kind of things. I am for example thinking of the work of Robert Paige at NYU. The problem is of course to identify situations where a given type of transformation may be useful. That require identifying computational structures, and knowing some of the algebraic properties of the data being manipulated. A classical ...


3

A general approach is to automatically infer loop invariants. There are techniques for inferring loop invariants that can be expressed in Presburger arithmetic, i.e., linear expressions over the integers plus quantifiers. These typically rely upon the fact that there exist decision procedures for Presburger arithmetic, e.g., the Omega method (see also the ...


3

How can inherited attributes be simulated with synthesized ones: an example. The way of doing it is to postpone the evaluation of any attribute that uses directly or indirectly an inherited attribute, by abstracting it into a function that takes the inherited attribute as argument. There may be several such arguments. Here is a fragment of a simple example,...


2

... is not valid since we have "left recursion" (a variable that calls itself). That's not what a left recursion is. That's simply recursion. Direct left recursion is when a rule $A \to A\alpha$ exists for arbitrary $\alpha$. Indirect left recursion exists when there's a rule $A \to^* A\alpha$ for arbitrary $\alpha$. Note the star, implying possibly many ...


2

I actually thought about the same question a while ago. Here is the train of thought I had: As you said the halting problem is an issue. To avoid this we need a language which only allows programs that always halt. On the other hand our language needs to be expressive enough to deal with most common problems(e.g. it should at least capture all of the ...


2

This new version of the answer tries to take into account the changes in the question, and the information exchanged in the comments. This answer assumes that $S$ should be the set of variables that have a content that is used in some defined fragment of the program, rather than, at some point in the program, the variables with a content that will be ...


2

SML compilers do perform eta-reduction (at least SML/NJ does), but I expect most functional programming language compilers do, even those for which the eta-law does not always hold. E.g. the pointer equality of OCaml doesn't have a strictly defined semantics, which means that the compiler is free to apply eta-reduction, even though it may change the program'...


2

It is hard to say. The boundary between "syntactic errors" and "static semantic errors" can be really blurred. One appropriate example would be Curry-style (extrinsic typing) and Church-style (intrinsic typing) variants of the same programming language, say System F. Failing to include type annotations in the Church-style variant of the language would be a ...


2

In Knuth Vol II Theorem E on page 494 he presents an algorithm that can evaluate a polynomial using $\frac{n}{2} + 2$ multiplications. The theoretical minimum is $\frac{n}{2}$, assuming generic polynomials. The algorithm requires factoring polynomials. There is another algorithm from Rabin & Winograd that only requires division, but runs in $\frac{n}{2} +...


1

It's possible to do a Gödel numbering that assigns every term in System F to a unique natural number? The answer is yes, pick your favorite way of coding terms in F, simply because they are countable number of expressions. Just being able to assign numbers to expressions in a system is not useful by itself, the question is can it be done in a manner that ...


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