FunX

FunX is a static analyzer that tells software developers what functions to write. FunX minimizes the total development time by instructing developers to implement partial functions, and telling them how to extend existing partial functions to cover a progressively larger part of their input domains.

FunX is based on an important observation: "In practice, a function will never receive its every possible input". In other words: there is always some obscure input that won't be seen by the function. This is true for every function with an infinite input domain (for example: the add function, which has an infinite input domain of pairs of natural numbers, will never see every possible pair of natural numbers).

This fundamental property allows to split a complex task into simple tasks by splitting a total function into partial functions. Partial functions are easier to implement because they have smaller input domains. FunX generates new input domains from execution statistics and the axiom of continuity (which states that the probability of seeing a new input depends on the probability of seeing a previous input that is "close to" the new input).

Definitions

• Word
• Phrase
• Type
• Dict
• Def

Algorithm

Main idea: solve a general case by solving special cases, then combining special solutions into a general solution.

Innovations:

• An algorithm for automatic generation of special cases from a general case ("partialization")
• An algorithm for automatic generation of a general solution from special solutions ("reconciliation")

The special cases are generated by the machine. The human only needs to provide partial solutions for these special cases.

1. Transform the question into a list of axioms (logical statements that describe the problem)
   1. Axioms must include axioms about the types of the variables
   2. Axioms must not include any axioms that are not directly given by the question (see why)
      1. It's possible to ask the author of the question to clarify the question (= specify additional axioms).
2. Transform the list of axioms into a generator that yields a list of lists of premises (logical statements that describe a special case of the general problem) (yes, generator yields a list of lists: every element of the top list is a special case, which is represented as a list of premises)
   1. Premises must include every axiom
   2. Premises must include at least 1 additional constraint that reduces the full question to a partial question (reduces the general case to a special case).
   3. Premises must be unique across the list (generator must filter the premises that are considered equivalent under the list of axioms).
3. Transform premises into partial solutions (1 partial solution for 1 premise)
4. Initialize the total solution to the first value from the generator of partial solutions.
5. For each partial solution from the generator:
   1. Reconcile the current total solution with a new partial solution: each

The "natural language" steps are only needed for communication with other humans who are not parsers.

Notes:

• A validator function is not needed: the question must be transformed to a list of logical statements (axioms) that completely describe the problem.

No axiom for output type

Example:

1. You are given the question: "What is the root of the square equation a*x^2 + b*x + c = 0?"
2. You are tempted to write the axiom: answer has type "real" (answer: real). However, if a = 0 and b = 0 and c != 0, the answer has type absurd (or "empty", "bottom"), because the equation reduces to c = 0, which contradicts the premise c != 0.
3. You are tempted to write the axiom: x has type "real" (x: real). However, if b = 0 and sign(a) = sign(c), then x has type complex, because the equation reduces to x = sqrt(-1 * c/a).

Therefore, it's incorrect to assume the axioms that are not given by the question (axiomatize the type of any variable, including answer).