Computer languages as examples in formal logic

  • I
  • Thread starter Stephen Tashi
  • Start date
  • Featured
  • #1
Stephen Tashi
Science Advisor
7,393
1,368

Summary:

For the purposes of teaching topics in mathematical logic, how can we make examples based on a computer language?
A computer language is not a clear example of a formal language, a formal system, or a formal logic. Can we modify the rules for a computer language to create clear examples?

My non-authoritative classification of topics in mathematical logc is:

1. Formal languages. A formal language is defined by a set of rules that define which strings of symbols are "well formed formulas" (wffs). A wff has no semantic interpretation other than being syntactically correct according the rules of the formal language. Within the context of a formal language, a wff does not represent a statement that is True or False or a mathematical function.

2. Formal systems: A formal system is a formal language plus a set of "production rules". If we write down an initial wff, the production rules describe permissible operations for "deriving" other wffs from the initial wff. Within the context of a formal system, there is no interpretation that wffs involved are True (or False), so the "derivations" are not mathematical proofs that deduce True statements from some initial statement that is assumed to be True.

3. Formal logics: A consistent formal two-valued logic is a formal system with additional requirements. The wffs must each be assigned exactly one of two possible values, either True or False. (As a matter of vocabulary, in a specific formal language, the wffs are assigned specific values. Speaking of "formal language" as a generality, it is a set of specific formal languages. The value assigned to a wff may vary between two different laguages in that set.) The production rules must have the property that (for each specific language in the formal language) if the initial wff is True, all the wffs produced from it are True.

As to turning a computer language into examples, I have the following thoughts.

Consider the C programming language.

1. Formal language: The syntax of programming languages contains the concept of various types of wffs. For example, a legal variable name is a certain type of wff. A mathematical expression is a different type. The goal of defining these types is to define a syntactically correct program. So to use the whole language as an example of a formal system, we must consider a wff to be an entire program.

2. Formal system: I don't know how to view the C programming language as a set of production rules. Within the syntax of C, there are things resembling production rules that define particular types of wffs. For example a rule could be: If <expression A> and <expression B> are each legal mathematical expressions then "<expression A> + <expression B>" is a legal mathematical expression. However, if we are using entire programs as the examples for wffs, I don't see that C has rules that define how to begin with some initial program and derive other programs.

3. Formal logic: One thought is to define a subset of C programs in which all variables must be boolean and that, in each program, all variables must be defined in terms of a set of constants A,B,C,...,Z. Constants do not change their values within a program. A constant like "A" can be assigned to be 1 in one program and 0 in a different program. The requirement is that the specific set of constants must be declared and assigned values in each program

However, that doesn't fix the problem that C is not a good example of a Formal System. So restricting it to boolean variables doesn't give us production rules.

( Discussions of mathematical logic on the forum resemble discussions about interpretations of quantum mechanics. Experts disagree. It makes me think that the rules of the game are not standardized. Maybe they aren't! )
 

Answers and Replies

  • #2
34,149
5,764
However, if we are using entire programs as the examples for wffs, I don't see that C has rules that define how to begin with some initial program and derive other programs.
Right, I don't see that a complete C program could be considered a WFF, at least to the extent that it could be used to derive other programs.
 
  • #3
449
51
I don't quite understand what your question is about. Something that seems to be (loosely) related to the question:

Suppose we fix a finite alphabet ##\Sigma## [which would usually contain all english alphabet, spaces and few more characters depending on our need]. Then considering ##\Sigma^*## [1], the set of all finite strings over ##\Sigma##. Suppose we define ##S## to be the subset of ##\Sigma^*## which represents "syntactically correct" programs (for any "reasonably described" programming language [2]). That is, a (finite) string ##s \in S## iff ##s## doesn't contain any "syntax errors".

Then the first thing to note is that ##S## is decidable (obviously). But more can be said (based on what I have read). Based on what I remember reading (it has been number of years now) is that essentially ##S## can be considered as a context free language. This is probably ignoring some exceptions [e.g. variable declarations (and perhaps more?), as I re-call reading]. More concretely, I think if you search for it you would probably find the grammar for a language like Pascal etc. I definitely remember seeing it quite some time ago. Probably, simpler examples would be more illustrative though.

My guess is that what I wrote in last paragraph is very well-known. Also note that collection of CFL's is a strict subset of the collection of r.e. (recursively enumerable) or even recursive/decidable languages. Another thing to mention is that lot of other things [subsets of strings over some finite characters] like strictly formed arithmetic expressions [3] (no missing brackets) and many other things fall into category of CFLs.


[1]
In the case that you might not have encountered this symbol before:
https://en.wikipedia.org/wiki/Kleene_star

[2]
The phrase "reasonably described" is meant to be informal.

[3]
What that means exactly is ambiguous (without specification). To be more concrete, if we fix an alphabet like ##\{a,b,c,+,∗,(,)\}##, then the following would be examples of it:
b
(a+b)
((a+b)*c)
(((a+b)*c)+a)
etc.
 
Last edited:
  • #4
Stephen Tashi
Science Advisor
7,393
1,368
I don't quite understand what your question is about.
The question is a general question about methods of teaching. How can we use computer languages to formulate examples of topics in mathematical logic?

How can I make the question clearer?

Something that seems to be (loosely) related to the question:

Suppose we fix a finite alphabet ##\Sigma## [which would usually contain all english alphabet, spaces and few more characters depending on our need]. Then considering ##\Sigma^*## [1], the set of all finite strings over ##\Sigma##. Suppose we define ##S## to be the subset of ##\Sigma^*## which represents "syntactically correct" programs (for any "reasonably described" programming language [2]). That is, a (finite) string ##s \in S## iff ##s## doesn't contain any "syntax errors".
I agree that such an example is an example of a formal language where we have chosen to call a wff a "syntactically correct" program. The viewpoint of my question is in the other direction. How do we begin with a computer language and use it as an example of a formal language. The answer appears to be equivalent - namely to say that "syntactically correct" programs are examples of wffs.

Then the first thing to note is that ##S## is decidable (obviously). But more can be said (based on what I have read).
However, my question isn't about how to discuss arbitrary examples of topics in logic. The question is how to use computer languages and modifications of them to illustrate topics in logic. So the properties of your ##S## are only relevant if we can begin by saying that some computer language or modification of it is an example of ##S## and then show how the properties of the modified compute language illustrate the properties of ##S##. For example, if you are using "decidable" in the sense of recursive (e.g. https://en.wikipedia.org/wiki/Recursive_language ) we could use examples of recursiveness in the modified computer language to illustrate the concept of decidability.
 
  • #5
449
51
The question is a general question about methods of teaching. How can we use computer languages to formulate examples of topics in mathematical logic?
Right, this can mean a lot of things.

Few things that might be of interest (these are just possible pointers ..... I don't know much about these topics). Perhaps some of these may be relevant:
------ Something like a proof assistant. Would that be related to what you are saying?

------ Something like curry-howard isomorphism. I have seen this phrase many times. Though, honestly, I don't have an idea what it really means.

------ Basic reasoning about programs in rigorous manner. I know a few basic books on this topic (but haven't read any). But nevertheless, this is an interesting topic. If you search, you would probably find some material on this topic.

For example, if you are using "decidable" in the sense of recursive (e.g. https://en.wikipedia.org/wiki/Recursive_language ) we could use examples of recursiveness in the modified computer language to illustrate the concept of decidability.
Yes, I meant in that sense.

It is not difficult to use restrictive languages exclusively to illustrate a number of basic ideas (without any skipping) such as encoding (similar or same to godel encoding), simulation/universal program etc. But normally (for theory), beyond a certain point informal sketches seem to be quicker/easier.

But I don't know if this is along the lines of what you are seeking.
 
Last edited:
  • #6
Klystron
Gold Member
698
959
For purposes of teaching formal logic consider limiting the C programming language to a minimal form that fulfills your didactic requirements while eliminating exceptions and possible contradictions. Whether this simplifed C language subset remains a realistic programming language might not matter depending on your teaching goals.

Ages ago I helped reduce a standard C language module to a significantly smaller version to meet size and run-time constraints in a dedicated environment. One modification I remember was to reduce allowed conditional and iterative (looping) constructs to the bare minimum along with limited included libraries. Data types were restricted to those required by the project eliminating, for examples, floating point and character string types.

We provided a programming manual including methods to reduce standard C routines to C-simple and to compile in this limited environment. To quote Joan Baez, "Take what you need and leave the rest.".
 
  • #7
449
51
One other example of using a more specific computation model (for a specific theoretical purpose) seems to be RAM model. I had never heard of it until very recently. It seems that it is meant to help formalize some notions w.r.t. time complexity (in cases where a finer distinction may be required).
 
  • #8
Paul Colby
Gold Member
1,203
295
I've spent some time writing language front-ends using lex and yacc. Lex defines the tokens i.e. "int" is a keyword assigned an integer value and so on. The yacc input is a system of syntactic productions forming an LALR language in terms of terminals and and tokens. Each production has an action which one might view as wff rewrite?
 
  • #9
Stephen Tashi
Science Advisor
7,393
1,368
Each production has an action which one might view as wff rewrite?
That's a good idea. Can a parser for a computer language be regarded as defining the derrivation rules for a formal system?

Compared to a system of derrivation rules, I think a parser works in reverse. Instead of derriving new wffs from given wffs, it takes a given string (an attempted program) and tries to find a way that it can be analyzed as the result of applying production rules to a set of wffs. It must discover the wffs that are inputs.

For example, to determine "A+B" is a valid expression, it must discover that the inputs "A","B" can be used to form "A + B" according to the rule: Input: <variable 1>, <variable 2> Output: <variable 1> + <variable 2>.

I can think of a parser as implicitly defining a set of derrivation rules. As a teaching example, this still leaves the problem that a wff in a computer language must be a complete program. A parser does not analyze a complete program as being composed of other programs.

There might be a computer language (or a way of regarding a language) where wff can refer to some set of things that includes programs as a proper subset. Perhaps languages that have the philosophy "Everything is an object" can be regarded that way.
 
  • #10
Stephen Tashi
Science Advisor
7,393
1,368
One other example of using a more specific computation model (for a specific theoretical purpose) seems to be RAM model.
I read the brief descripton at https://www8.cs.umu.se/kurser/TDBA77/VT06/algorithms/BOOK/BOOK/NODE12.HTM. I don't know how to fit that into an example for a formal system.

Assuming we have a formal language of certain type, where a wff must be an algorithm, the RAM model assigns a number to such an wff. So it's an example of assigning numbers to wffs - not the way Godel did, but an illustration that the general idea is not crazy.
 
  • #11
449
51
I didn't understand your question so I thought you were asking for a computation language conceived specifically for any theoretical purpose (generic).

Given what you wrote in last post, I can only add two points:
(a) The type-0 grammars (there are few names for these or equally powerful grammars) can generate any recursively enumerable language. But I suppose that you might be looking for something more specific.

(b) Lambda calculus would be related to what you are asking, I think. I am not familiar with it well-enough though.

Here are few links I found with a quick search (that seem to be of some relevance to what you are saying in last post):
link1
link2
 
  • #12
Stephen Tashi
Science Advisor
7,393
1,368
(b) Lambda calculus would be related to what you are asking, I think. I am not familiar with it well-enough though.
l don't see any relation to the question in my OP, but it's mind-expanding to read about a "non-extensional" approach to describing functions.
 
  • #13
Paul Colby
Gold Member
1,203
295
Can a parser for a computer language be regarded as defining the derrivation rules for a formal system?
My understanding is a properly formed BNF system defines a computer language while a parser validates given inputs wrt the defined system. Can the valid set of wffs be considered such? If the rules are an LALR parsable set of strings then isn't the answer yes?
 
  • #14
370
219
Summary:: For the purposes of teaching topics in mathematical logic, how can we make examples based on a computer language?
Have you heard of Prolog?

Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is intended primarily as a declarative programming language: the program logic is expressed in terms of relations, represented as facts and rules. A computation is initiated by running a query over these relations.
https://en.wikipedia.org/wiki/Prolog
 
  • Like
Likes SSequence
  • #15
9,483
2,572
Can a modern computer language implement a (conceptual) Turing Machine? Can Turing Machines be used to deduce propositions in a formal logical system (eg the predicate calculus)?

Thanks
Bill
 
  • #18
Stephen Tashi
Science Advisor
7,393
1,368
I think Turing introduced his machines to go beyond formal languages, formal systems, and formal logic and proceed to a model that gives us computers. However, I haven't seen Turing machines presented by giving a formal formal system or formal logic and then saying "here's the assumptions we add to get a Turing machine". If that were the case, a Turing machine would be an example of those formal structures.

The usual presentation of a Turing machine begins informally (by the standards of mathematical logic) and speaks of a "tape" that contains symbols and a machine that can move along and write and erase on that tape. Although the motivation may be to extend formal systems, formal logic etc, the presentation sidesteps any mention of these topics. So there is no obvious way to see that Turing machine is a specific example of any of them.

As far as the question in the OP goes, it makes sense to consider Turing machines since the OP asks about computer languages and a Turing machine is a model of a computer. However, just as in the case of a specific computer language, we need some way to fix-up a Turing machine or look at it in special way to make it into a clear example.
 
  • Like
Likes bhobba
  • #19
Stephen Tashi
Science Advisor
7,393
1,368
Have you heard of Prolog?
https://en.wikipedia.org/wiki/Prolog
Does that imply Prolog an obvious answer to the OP? - or is this a suggestion for further investigation?

Yes, I've heard of prolog and the concept of declarative programming languages, but I haven't used them. Can Prolog be used as an example of a formal language, formal system, or formal logic? How would that be done? The link say Prolog "has its roots" in first-order logic. But is Prolog or some aspect of it identical to a first-order logic?
 
  • #20
449
51
Can a modern computer language implement a (conceptual) Turing Machine? Can Turing Machines be used to deduce propositions in a formal logical system (eg the predicate calculus)?

Thanks
Bill
It would depend on specific case. But under "reasonable" circumstances, the answer is "generally" (but not always) yes [1]. Also, I am assuming that you are asking in principle. In practice, the time complexity of enumerating all proofs of certain length (provable in a given system) would be quite high practically [on the very least, no general efficient way is known I think].

For example, the theorems of PA are r.e. (recursively enumerable). Similar is the case of set theory (as formalized in ZFC as an example). The reason for theorems being r.e. here is a bit more complicated and I don't know it well enough [2]. Same is true for a lot of theories that are weaker than set theory (for example, (i) the five systems of reverse math (ii) likely some weaker fragments of set theory too ...... and what not).

[1] Taking the assumption of infinite memory available as given (I am guessing this is implicitly assumed or allowed?).

[2] Generically, in first-order-logic, there seem to few lemmas/theorems which help guarantee the recursive enumerability of theorems (if certain given conditions/pre-requisites are satisfied).


Although the motivation may be to extend formal systems, formal logic etc, the presentation sidesteps any mention of these topics. So there is no obvious way to see that Turing machine is a specific example of any of them.
This is true but there are still lot of interesting aspects that logic can provide.

As one example (among others), description of more complicated sets (than decidable) often seem to have multiple equivalent notions [including intrinsically logical descriptions] associated with them. Actually, often there seem to be two or more complementing descriptions!

Lets think about computable sets in following two ways (admittedly quite coarsely):
(1) computability (as in by a program)
(2) general recursive function (primitive recursive functions with minimalization operator)

But mathematics is not only about computable sets or c.e. sets. Many more complicated sets (even ones whose elements are only natural numbers) seem to have a number of intrinsic and equivalent descriptions: recursion based [suitable generalisation of primitive recursive functions], logic based [first-order-definitions over a structure] and infinite time computation based which complement each other. In some specific cases (specific collections of sets), some notions don't directly fall into category of either of above.

Anyway, this isn't directly related to the question, but I felt it is interesting to point this out (since this point came up).
 
Last edited:
  • Like
Likes bhobba
  • #21
Stephen Tashi
Science Advisor
7,393
1,368
My understanding is a properly formed BNF system defines a computer language while a parser validates given inputs wrt the defined system.
I like the idea of focusing on a Backus-Naur specification of language instead of focusing on a parser of those specifications. How can I relate BNF specifications to the mathematical idea of formal language- as opposed to the computer science idea of a computer language?
 
  • #22
Paul Colby
Gold Member
1,203
295
How can I relate BNF specifications to the mathematical idea of formal language- as opposed to the computer science idea of a computer language?
I haven't seen the definition of a formal language you're using. If I've missed it I apologize.
Just guessing I assume a "formal language" is a set of symbols with a set of rules to form valid strings of symbols or sentences. It's likely I'm missing something.
 
  • #23
370
219
Does that imply Prolog an obvious answer to the OP? - or is this a suggestion for further investigation?

Yes, I've heard of prolog and the concept of declarative programming languages, but I haven't used them. Can Prolog be used as an example of a formal language, formal system, or formal logic? How would that be done? The link say Prolog "has its roots" in first-order logic. But is Prolog or some aspect of it identical to a first-order logic?
I wasn't sure exactly what the goal is, but thought Prolog seemed to be the closest language I know that fits. So I guess this is a suggestion for further investigation.

Maybe this example can help.
https://www.cpp.edu/~jrfisher/www/prolog_tutorial/logic_topics/normal_forms/normal_form.html
 
Last edited:
  • #24
675
319
Summary:: For the purposes of teaching topics in mathematical logic, how can we make examples based on a computer language?

A computer language is not a clear example of a formal language, a formal system, or a formal logic. Can we modify the rules for a computer language to create clear examples?

My non-authoritative classification of topics in mathematical logc is:

1. Formal languages. A formal language is defined by a set of rules that define which strings of symbols are "well formed formulas" (wffs). A wff has no semantic interpretation other than being syntactically correct according the rules of the formal language. Within the context of a formal language, a wff does not represent a statement that is True or False or a mathematical function.

2. Formal systems: A formal system is a formal language plus a set of "production rules". If we write down an initial wff, the production rules describe permissible operations for "deriving" other wffs from the initial wff. Within the context of a formal system, there is no interpretation that wffs involved are True (or False), so the "derivations" are not mathematical proofs that deduce True statements from some initial statement that is assumed to be True.

3. Formal logics: A consistent formal two-valued logic is a formal system with additional requirements. The wffs must each be assigned exactly one of two possible values, either True or False. (As a matter of vocabulary, in a specific formal language, the wffs are assigned specific values. Speaking of "formal language" as a generality, it is a set of specific formal languages. The value assigned to a wff may vary between two different laguages in that set.) The production rules must have the property that (for each specific language in the formal language) if the initial wff is True, all the wffs produced from it are True.

As to turning a computer language into examples, I have the following thoughts.

Consider the C programming language.

1. Formal language: The syntax of programming languages contains the concept of various types of wffs. For example, a legal variable name is a certain type of wff. A mathematical expression is a different type. The goal of defining these types is to define a syntactically correct program. So to use the whole language as an example of a formal system, we must consider a wff to be an entire program.

2. Formal system: I don't know how to view the C programming language as a set of production rules. Within the syntax of C, there are things resembling production rules that define particular types of wffs. For example a rule could be: If <expression A> and <expression B> are each legal mathematical expressions then "<expression A> + <expression B>" is a legal mathematical expression. However, if we are using entire programs as the examples for wffs, I don't see that C has rules that define how to begin with some initial program and derive other programs.

3. Formal logic: One thought is to define a subset of C programs in which all variables must be boolean and that, in each program, all variables must be defined in terms of a set of constants A,B,C,...,Z. Constants do not change their values within a program. A constant like "A" can be assigned to be 1 in one program and 0 in a different program. The requirement is that the specific set of constants must be declared and assigned values in each program

However, that doesn't fix the problem that C is not a good example of a Formal System. So restricting it to boolean variables doesn't give us production rules.

( Discussions of mathematical logic on the forum resemble discussions about interpretations of quantum mechanics. Experts disagree. It makes me think that the rules of the game are not standardized. Maybe they aren't! )
There's the lambda calculus, a formal language that can in theory be used to compute. There are the various styles of Turing Machine. These were formalisms used in proofs of what is and isn't computable.

There are also non-procedural languages dedicated to solving problems in logic. You tell the system what the problem is and it computes the solutions. Prolog! That's the name. Surely it is obsolete by now.

There's Backus' FP, a functional programming language. FP has no variables and actually runs on a computer. Or at least did at one time.

My thinking is that the big difference between these and an actual programming language is that there are NO variables. Once something is given a value it never changes its value. I programmed this way insofar as is practical and found it very helpful for writing reliable programs. The only essential reason to have variables is to save memory. Theoreticians don't need to worry about that.
 
  • #25
Stephen Tashi
Science Advisor
7,393
1,368
I haven't seen the definition of a formal language you're using. If I've missed it I apologize.
Just guessing I assume a "formal language" is a set of symbols with a set of rules to form valid strings of symbols or sentences. It's likely I'm missing something.
We need expert commentary on whether my definition of formal language is correct!. In my definition, a formal language agrees with what you said. The rules for wffs aren't necessarily stated as rules for deriving new wffs from given wffs. When we have rules for derriving new wffs from given wffs, I call that case a "formal system".
 

Related Threads on Computer languages as examples in formal logic

Replies
1
Views
724
  • Last Post
Replies
6
Views
2K
Replies
14
Views
2K
Replies
7
Views
2K
Replies
0
Views
2K
Replies
3
Views
870
Replies
2
Views
927
  • Last Post
Replies
2
Views
605
  • Last Post
Replies
14
Views
3K
Top