Why DSL
Conclusion
We perfer to use DSLs is addressing that in model complete therory and definition of DSLs, it is a more concrete and direct way for doing modeling better, because \(iff\) a model \(M\) is model complete, it is equalize to the \(DSL\) of that Model.
DSL
There are two main schools of DSLs: \(internal\) and \(external\) DSLs[1]. The \(concrete\ syntax\) defines the notation with wihich users can express programs.
A DSL or GPL may include follow ingredients[2]:
\(abstract\ syntax\)
which is a data structure that can hold the semantically relevant information express by a program.
\(static\ semantics\)
Which Of language are the set of constraints and/or type system rules to which programs have to conform.
\(Excution Semantics\)
Which refers to the meaning of a program once it is execuded. It is realized using the \(execution\ engine\).
Modeling, and Model Complete
Modeling
There are two ways in which the term modeling can be understood: descriptive and preciptive. A descriptive model represent an existing system Thus a presciptive model is one that can be used to construct the target system. In DSL engineering, we always mean prescriptive models when we use the term model[3].
Model Complete
In model theory, a first-order theory is called model complete if every embedding of models is an elementary embedding. Equivalently, every first-order formula is equivalent to a universal formula[6].
A companion of a theory \(T\) is a theory \(T^*\) such that every model of \(T\) can be embedded in a model of \(T^*\) and vice versa.
A model companion of a theory \(T\) is a companion of \(T\) that is model complete. \(Robinson\) proved that a theory has at most one model companion.
A model completion for a theory \(T\) is a model companion \(T^*\) such that for any model \(M\) of \(T\), the theory of \(T^*\) together with the diagram of \(M\) is complete. Roughly speaking, this means every model of \(T\) is embeddable in a model of \(T^*\) in a unique way.
GPL and Turing Complete
We known that the GPL is always Turing Complete. Turing Complete is means that a GPL it can be used to simulate any single-taped Turing machine. Turing Complete is actualy a preciptive model of Turing Machine.
Domains and Model complete
When we said that a language \(l\) covers a subset of \(P\), we can simply call this subset the \(domain\) covered with \(l\). The subset of \(P\) in that domain \(P_D\) is equal to the subset of \(P\) we can express with a language \(l\) \(P_l\). So, we cannot ask a question like: “Does the language adequately cover the domain?”, since it always does, by definition.[4] And the definition can be also interept as that “DSL is always model complete, by definition”
Completeness
A DSL might be eighter incomplete-DSL or complete-DSL, is determined by Completeless which is refers and only refers to the degree to which a language \(L\) can express programs that contain all necessary information to execute them. An program express in an incomplete DSL requires additional specifications (such as configuation files or code written in a lower-level language) to make it executable.[5]
Referance
[1][2][3]DSL Engineering, Designing, Implementing and Using Domain-Specific Languages, Markus Voelter, dslbook.org, ch 2.1
[4]DSL Engineering, Designing, Implementing and Using Domain-Specific Languages, Markus Voelter, dslbook.org, ch 3.1
[5]DSL Engineering, Designing, Implementing and Using Domain-Specific Languages, Markus Voelter, dslbook.org, ch 4.5
[6] Chang, Chen Chung; Keisler, H. Jerome (1990) [1973], Model Theory, Studies in Logic and the Foundations of Mathematics (3rd ed.), Elsevier, ISBN 978-0-444-88054-3