I've been working on a formal language specification for a while, and it finally took a shape I'm satisfied with. If you like, you can take a look at Logos specification in the link below (some twenty minutes read). Logos stands for a (l)anguage (o)f (g)eneral (o)perational (s)emantics. The language represents all of the following:
- Metatheory language formalization
- Theorem prover
- Term rewriting system
- Data computing environment
It reminds of a Lisp (lisp is a usual choice for AI development), and brings some extension on s-expressions (https://en.wikipedia.org/wiki/S-expression). Logos has completely flexible syntax, ready to host *any* theory language, from logic, to lambda calculus, to different embodiments of industry programming languages.
Its syntax is very simple, but it represents a Turing complete (https://en.wikipedia.org/wiki/Turing_completeness) language:
a-expr ::= ()
| identifier
| a-expr a-expr
| ‹a-expr›
| «a-expr»
| (a-expr)
Some of implementation is already done in a form of context free grammar (https://en.wikipedia.org/wiki/Context-free_grammar) parser. Further development has something to do with Turing completeness of unrestricted grammar from Chomsky hierarchy (https://en.wikipedia.org/wiki/Chomsky_hierarchy), which is an extension of context free grammar. Logos should be a form of a higher order unrestricted grammar metalanguage.
If you are into symbolic AI, Logos could be a place to start with to collect some useful info about knowledge mining. It is aimed to be a language for manipulating formal knowledge.
Read about the project here (https://github.com/ivanvodisek/Logos).
Congratulations. O0
«(a ‹⋅› b) ‹+› (a ‹⋅› c)»
(higher (a (lower ⋅) b) (lower +) (a (lower ⋅) b) )
Why did you choose to extend the S-expression syntax?
Also, another question: are parenthesis impacted by the « » and ‹ › ? or identifiers are the only things impacted? For example,
«(f ‹[› x ‹:=› «x» ‹]›) ‹->› f»
Here square brackets are part of the expression, clearly: they are "constantified" ::)
But aren't the outer « » enough to group the left-hand side?
Sorry, I swear I'm trying real hard to get my head around it all...
Thank you, Zero for a kind word :)
«(a ‹⋅› b) ‹+› (a ‹⋅› c)»
(higher (a (lower ⋅) b) (lower +) (a (lower ⋅) b) )
actually it is:
«(a ‹⋅› b) ‹+› (a ‹⋅› c)»
higher((a (lower ⋅) b) (lower +) (a (lower ⋅) b) )
Why did you choose to extend the S-expression syntax?
To introduce a clear distinction between variables and constants. And to relate (as an implication) constants and variables denoted by the same symbol. Note that there are no keywords. Only parenthesis and single or double angle quotes.
Also, another question: are parenthesis impacted by the « » and ‹ › ? or identifiers are the only things impacted? For example,
Parenthesis and double angle quotes can be nested, but within nests they have to be both opened and closed. It is not possible to have `« ... ( ... » ... )`, like it is not possible to have ( ... « ... ) ». The same goes with all combinations of single and double angle quotes and round parenthesis.
«(f ‹[› x ‹:=› «x» ‹]›) ‹->› f»
Here square brackets are part of the expression, clearly: they are "constantified" ::)
But aren't the outer « » enough to group the left-hand side?
The purpose of outer double angle quotes is to connect the left `f` and the right `f`. `‹->›` in between (the operator is defined earlier in the specification) allows us to automatically rewrite the left side with the right side in the context of the expression.
higher((a (lower ⋅) b) (lower +) (a (lower ⋅) b) )
Weird, it feels like jumping from (f x) notation to f(x) notation. I don't get it.
And to relate (as an implication) constants and variables denoted by the same symbol.
z and «z» are related because the identifier is the same, am I correct?