In logic and linguistics, a metalanguage (https://en.wikipedia.org/wiki/Metalanguage) is a language used to make statements about statements in another language (the object language).
What is Metafigure?
Metafigure is a programming language for defining other languages and theories. As for languages, it allows their syntax definition. As for theories, it also allows definition of dependencies between theory segments. Metafigure is equipped with mechanisms that can be used for a variety of data related tasks from data analysis and language translation to theorem proving and finding unknown general rules that hold for analyzed data.
With Metafigure it is possible to describe a variety of theories for different systems held in the Universe. Metafigure acts as an arbitrary complexity level state machine that can reflect the dynamic nature of the data. When we know enough data about a system, we can predict its state changes and derive answers about the system. In fact, that is what is Metafigure primarily about: to serve as a foundation for forming conclusions about the Universe.
Metafigure is closely related to scientific theories about theories, but it exhibits flexible syntax and semantic definitions in precision in which computer programmers are used to. With Metafigure one can define different sciences like logic, mathematics, chemistry and others, but the one is asked for detailed formalism like in regular computer programming languages. In spite of its very explicit layers of constructs, Metafigure manages to maintain a high level of abstraction in direction of once defined theories.
Basic symbol constructs
Symbols are the most basic Metafigure particles that are used to hold data. When writing down an actual symbol, its name should start with a letter and continue with any combination of letters, numbers or underscore. Let’s take a look at our first example, we will define an arbitrary symbol “Xâ€:CodeX <- @Integer {25}
Here we noted that symbol “X†has a type “@Integer†and a value “25“. We used operator “<-†which is read “follows formâ€, to denote the type of “Xâ€. Type “@Integer†is actually a reference to another symbol and references are denoted with “@†prefix. We also say that “X†is a parent of its type. Curly braces serve as containers for actual data, in our case “25“.
Note that as Metafigure is a typed language, its symbols can accept only values that have the right type. That means if a symbol is eg. of a type @Integer, its value has to be an integer.
“Follows†from operator can be chained and it associates to the right.
We can also define a range of types that some symbol can hold. We do it by using choice operator like in following example:CodeBool <- (True | False)
Choice operator is denoted by “|†sign and we used round braces to group choice elements because “follows from†operator has a precedence over choice operator. We can have any number of choices under a parent symbol, each delimited by “|â€. Here we actually have built a type Bool which we can later use as:CodeB <- @Bool {True}
Complementary to choice operator is a tuple operator “,â€. A tuple denotes a list of values of which all belong to a certain symbol. Using a tuple, we can define input parameters of any function. Let’s see how an input of a function “And" would look like:CodeAnd <- (Left <- @Bool, Right <- @Bool)
Again, we can have any number of tuple elements, each delimited by “,†and we used round braces to override default operator precedence. We apply parameters to our partial “And†definition in a following way using curly braces:CodeA <- @And {Left {True}, Right {False}}
We used nested curly braces to apply specific values to “Left†and “Right†parameters, using a comma delimiter.
Metafigure expressions can be spanned over multiple lines, so the previous example can be written in the following way without changing the meaning:CodeA <- @And {
Left {True},
Right {False}
}
Wherever an optional whitespace appears in our expressions, a new line can be introduced instead. Multiple line spanning becomes very handy with more complex types. It is used to increase readability of types and values.
We can combine “follows from†operator, choices and tuples to build complex symbol types out of basic symbols. For the end of this section let’s build a more complete possible definition of Boolean constants and operator parameters. Note that for Boolean operators there are defined just parameters. Actual Boolean operator results will be defined through functions and will be introduced in following sections.CodeBooleanExpression <- (
Bool <- (True | False) |
And <- (Left <- @Bool, Right <- @Bool) |
Or <- (Left <- @Bool, Right <- @Bool) |
Not <- (@Bool)
)
Symbol pattern matching and text parsing
Assigning values in Metafigure, beside explicit notation, can also be made through symbol pattern matching and parsing arbitrary textual expressions. Symbol pattern matching together with parsing is an advanced property that reveals the real power of Metafigure programming language.
Symbol pattern matching enables automatic recognition of symbols against a list of values. Let’s consider an example of a type of integers:CodeInteger <- (
Digit <- (‘0‘ | ‘1‘ | ‘2‘ | ‘3‘ | ‘4‘ | ‘5‘ | ‘6‘ | ‘7‘ | ‘8‘ | ‘9’),
Next <- (@Integer | @Null)
}
To denote a value of 856 we could write:CodeX <- @Integer {
Digit {‘8’},
Next {
Integer {
Digit {‘5’},
Next {
Integer {
Digit {‘6‘},
Next {Null}
}
}
}
}
}
Instead of writing this complex expression symbol pattern matching allows us to write:CodeX <- @Integer {‘8‘, ‘5‘, ‘6’}
Values ‘8‘, ‘5‘ and ‘6' are arranged over the “@Integer†type, automatically inferring what symbols assertions are needed to encode the number. Internally, the number is memorized like in the example before the last one, but we do not have to explicitly denote it in assignment expression. Symbol “@Null†is one of internal symbols and is automatically inferred after the last digit as a given possibility. We can arbitrary choose a method of assigning values, whether it is explicit assignment or symbol pattern matching, and Metafigure automatically detects what we want to do.
It would be odd if we ought to write integers with quoted digits and commas. That is why Metafigure implements expression parsing. If we want to denote a symbol that should be parsed, we write “!†as a suffix to the symbol like in following example:CodeInteger! <- (
Digit <- (‘0‘ | ‘1‘ | ‘2‘ | ‘3‘ | ‘4‘ | ‘5‘ | ‘6‘ | ‘7‘ | ‘8‘ | ‘9’),
Next <- (@Integer | @Null)
}
When we defined “Integer†symbol as a parsed expression with "!" suffix, we can write our number in the following way:CodeX <- @Integer {856}
where digits would be automatically arranged over “@Integer†type symbols like it was the case with symbol pattern matching. When we denote a symbol as a parsed expression, we exclude the possibility to write it in regular Metafigure symbol assignment manner, which means that we have to explicitly choose whether we want it to be later assigned in parsed or non-parsed manner. “!†sign is inherited over the symbol’s child symbols, meaning that all child symbols are also treated as parsed expressions. We can override it with “?†suffix in the child symbol we want to be treated as non-parsed expression. “!†and “?†suffixes on symbol definitions allow mixing parsed and non-parsed styles, as we find necessary.
Beside generic Metafigure syntax for noting values in explicit or symbol pattern matching style, expression parsing makes it possible to define symbols that accept values in any syntax notation. That way we can write symbols representing syntaxes for specific expressions, domain specific languages, whole programming languages or theories which we can later combine in other value expressions.
A word about lists
One of the important topics in defining knowledge is lists. Among other uses, lists are useful in defining arbitrary length enumeration of parameters. There is a lot of possible list definitions and the common technique to define them is by recursion. Probably the most understandable recursive list definition is:CodeList <- (
Item <- (...),
Next <- (@List | @Null)
)
There are other list definitions that include associative methods. Left associative version looks this way:CodeList <- (
Item <- (...) |
Association <- (@List, @Item)
)
and right associative version looks this way:CodeList <- (
Item <- (...) |
Association <- (@Item, @List)
)
Associative methods are useful for defining operator precedence like in simple math expressions. In the following simplified example we use nested lists to achieve this behavior:CodeSum! <- (
Fact <- (
Primary <- (
(@WhiteSpace | @Null),
Value <- (
@Integer |
Braces <- ('(', Infix <- @Sum, ')')
),
(@WhiteSpace | @Null)
) |
MulDiv <- (Left <- @Fact, Infix <- ('*' | '/'), Right <- @Primary)
) |
AddSub <- (Left <- @Sum, Infix <- ('+' | '-'), Right <- @Fact)
)
Previous parsed expression example allows us to write expressions like the following one:CodeM <- @Sum {1 + 2 * (3 - 4) / 5}
while associating “MulDiv" expressions at higher priority regarding to “AddSub" expressions (of course, braces override this behavior). Actual calculation of results of expressions like these is a matter of using functions which we will explain in the next chapter.
Defining functions
Functions in Metafigure are symbols that calculate some result from their parameters. Function types are also built from “follows from†operator, together from specific result values that depend on specific parameters. To explain this, let us analyze following example:Code01 BoolExp <- (
02 Bool <- (True | False) |
03
04 (
05 @Bool <- (
06 And <- (Left <- @Bool, Right <- @Bool)
07 )
08 ) {
09 True {True, True};
10 False {False, True};
11 False {True, False};
12 False {False, False}
13 }
14 )
The example above shows possible partial definition of Boolean expressions. We defined Boolean constants in line 2 and a type of Boolean operator “And†in lines 5-7. Lines 9-12 contain a semantic table of values of operator “Andâ€. Each of those lines contains a pair of a result and parameters from which the result follows. These pairs actually correspond to pairs on the left and on the right side of “follows from†operator which forms the function type. The right sides of those pairs are symbol pattern matched to “And†calling structure (from line 6), while the left sides belong to “@Bool†result (from line 5). As to values of “@Bool†result and “And†function, pattern matching automatically recognizes symbols and automatically asserts them in the following way:Code{Bool {True}} {And {Left {Bool {True}}, Right {Bool {True}}}};
{Bool {False}} {And {Left {Bool {True}}, Right {Bool {False}}}};
{Bool {False}} {And {Left {Bool {False}}, Right {Bool {True}}}};
{Bool {False}} {And {Left {Bool {False}}, Right {Bool {False}}}}
In shown expanded expression, we used curly braces as a utility for grouping value pairs and for optional decorator of our expressions (for “Bool†values).
We see another new thing in “And†function example, and that is noting multiple values under the same symbol. Among other uses, this allows us to note semantic tables for later call-by-pattern.
Symbols in Metafigure actually can contain multiple values at the same time and they are noted delimited by a semicolon.
Now we can call our function in the following way:CodeResult <- @And {True, False}
and the symbol “Result “ is automatically being attached by the following value, calculated from “And†operator semantic table:CodeResult {Bool {False}}
When calling a function, Metafigure seeks for a pattern passed by parameters, so it can assign a result to a caller. This is known as call-by-pattern behavior. As we will see later, It will allow us to write complex functions.
We saw how functions are defined by “follows from†operator analogous to the standard symbol definition. The only difference is in the availability of noting result values that depend on some parameters, and the symbol pattern matcher does the magic at the time of calling function. To look somewhat further, as a deduction is just a function from premises to conclusions, functions will make available definition of deduction rules too.
A <-[define] B //classic <- operator
A <-[reduce] B //this would replace assigning values
A <-[tag] B
A <-[check] B
*And <-[define] ( //from now on "[define]" is inherited where "<-" is noted
(
Bool <- (*Left <- Bool, *Right <- Bool)
) <-[reduce] ( //from now on "[reduce]" is inherited where "<-" is noted
True <- (Left <- True, Right <- True) |
False <- (Left <- False, Right <- True) |
False <- (Left <- True, Right <- False) |
False <- (Left <- False, Right <- False)
)
)(
*Clock <- (
*hour <- Integer (
Case (
pHour (init);
(
hour + 1 (hour < 24);
0 (hour == 24)
) (Timer (60 * 60 * 1000))
)
),
*min <- Integer (
Case (
pMin (init);
(
min + 1 (min < 60);
0 (min == 60)
) (Timer (60 * 1000))
)
),
*sec <- Integer (
Case (
pSec (init);
(
sec + 1 (sec < 60);
0 (sec == 60)
) (Timer (1000))
)
)
)
) <- (*pHour <- Integer, *pMin <- Integer, *pSec <- Integer) c <- Clock (14, 30, 20)*hour <- Integer (
Case (
(
pHour (pHour);
(
hour + 1 (hour < 24);
0 (hour == 24)
) (Timer (60 * 60 * 1000))
) (pHour)
)
)*Case <- (
Case <- Bool |
@Result
)01 *BoolExp <= (
02 *Bool <= (*True | *False) |
03
04 *And <= (
05 Bool <= (Bool, Bool)
06 ) <- (
07 True <- (True, True) |
08 False <- (False, True) |
09 False <- (True, False) |
10 False <- (False, False)
11 )
12 )
01 *CExp <= (
02 *TExp <= (
03 *FExp <= (
04 *SExp <= (
05 *Exp <= (
06 (WhiteSpace | Null),
07 *Value <= (
08 Number |
09 String |
10 <<MF.Exp <- <<Symbol>>>> <= (
11 *Symbol <= (
12 *Keyword <= ("parsed' | Null),
13 *Mod <= ('*' | '@' | Null),
14 SymbolName
15 )
16 ) |
17 In <= (*Bra <= ('(', *In <= TExp, ')'))
18 ),
19 (@WhiteSpace | @Null)
20 ) |
21 *SpecifiesFrom <= (
22 (Left <- Right) <= (*Left <= Exp, '<-', *Right <= Left)
23 )
24 ) |
25 *FollowsFrom <= (
26 (Left <= Right) <= (*Left <= SExp, '<=', *Right <= FExp)
27 )
28 ) |
29 *Tuple <= (
30 (Left, Right) <= (*Left <= FExp, ',', *Right <= TExp)
31 )
32 ) |
33 *Choice <= (
34 (Left | Right) <= (*Left <= TExp, '|', *Right <= CExp)
35 )
36 )RegExp <= (
Union <= (@SimpleRE, '|', @RegExp) |
SimpleRE <= (
Concatenation <= (@BasicRE, @SimpleRE) |
BasicRE <= (
OneOrMore <= (@ElementaryRE, ('+?' | '+')) |
ZeroOrMore <= (@ElementaryRE, ('*?' | '*')) |
ZeroOrOne <= (@ElementaryRE, '?') |
NumberedTimes <= (
'{',
In <= (
Exactly <= @Integer |
AtLeast <= (@Integer, ',') |
AtLeastNotMore <= (@Integer ',', Integer)
),
('}?' | '}')
) |
ElementaryRE <= (
Group <= ('(', @RegExp, ')' |
Any <= '.' |
Eos <= '$' |
Bos <= '^' |
Char <= (
@NonMetaCharacter |
'\\', (
@MetaCharacter |
't' | 'n' | 'r' | 'f' | 'd' | 'D' | 's' | 'S' | 'w' | 'W' |
@Digit, @Digit, @Digit
)
) |
Set <= (
PositiveSet <= ('[', @SetItems, ']') |
NegativeSet <= ('[^', @SetItems, ']')
) <~ (
SetItems <= (
SetItem <= (
Range <= (@Char, '-', @Char) |
@Char
) |
@SetItem, @SetItems
)
)
)
)
)
) ChExp <= (
Choice <= (@ConExp, '|', @ChExp) |
ConExp <= (
Concatenation <= (@WExp, @ConExp) |
WExp <= (
Without <= (QExp, '!', @WExp) |
QExp <= (
OneOrMore <= (@GExp, '+') |
ZeroOrMore <= (@GExp, '*') |
ZeroOrOne <= (@GExp, '?') |
NumberedTimes <= (@GExp, '{', @Integer, '}') |
GExp <= (
Group <= ('(', @ChExp, ')') |
Exp <= (
Any <= '.' |
Range <= (@Char, '-', @Char) |
Char <= (
@NonMetaCharacter |
'\\', (
@MetaCharacter |
't' | 'n' | 'r' | 'f' |
'0x', @HEXDigit, @HEXDigit, @HEXDigit, @HEXDigit, @HEXDigit, @HEXDigit
)
)
)
)
)
)
)
A metatheory or meta-theory is a theory whose subject matter is some theory. All fields of research share some meta-theory, regardless whether this is explicit or correct. In a more restricted and specific sense, in mathematics and mathematical logic, metatheory means a mathematical theory about another mathematical theory.
The following is an example of a meta-theoretical statement:
“ Any physical theory is always provisional, in the sense that it is only a hypothesis; you can never prove it. No matter how many times the results of experiments agree with some theory, you can never be sure that the next time the result will not contradict the theory. On the other hand, you can disprove a theory by finding even a single observation that disagrees with the predictions of the theory. â€
Meta-theoretical investigations are generally part of philosophy of science. Also a metatheory is an object of concern to the area in which the individual theory is conceived.