Computer languages as examples in formal logic

  • I
  • Thread starter Stephen Tashi
  • Start date
  • Featured
  • #26
Paul Colby
Gold Member
1,216
298
Summary:: For the purposes of teaching topics in mathematical logic, how can we make examples based on a computer language?

I don't see that C has rules that define how to begin with some initial program and derive other programs.
What about code optimizers? Granted, these are typically applied after the code has been translated into some intermediate form. For example changing, "a = b + c + e;", into a series of machine op codes acting on selected registers. Basically, a different wff in a different language. During this process the optimizer may note that a previously computed sum, say c + e, is used in 20 other expressions and decides reusing this computed value is cheaper. It then changes the code using rules that guarantee the result of the new code doesn't change.
 
  • Like
Likes Klystron and Stephen Tashi
  • #28
449
51
When we have rules for derriving new wffs from given wffs, I call that case a "formal system".
What about these:
https://en.wikipedia.org/wiki/Unrestricted_grammar

I already mentioned them in post#11. Wouldn't these closely correspond to what you are calling formal system.


P.S.
I have also been a bit vague about the term "formal system" in the past. Normally when I have used the term in the past I have meant it in the following sense: a program which prints a recursively enumerable subset (say S) of following set:
0, 0', 1, 1', 2,', 3, 3', 4, 4', 5, 5', 6, 6', 7, 7', 8, 8', 9, 9', 10, 10',............................

Each number x in the set {0,1,2,3,4,5,6,......} is supposed to correspond to some question/statement [from a selected/agreed domain of problems]. The number x' is supposed to correspond to negation of the statement (which corresponds to number x). So when x∈S, it means that S proves the sentence corresponding to x. When x'∈S, it means S disproves the sentence corresponding to x (i.e. proves sentence corresponding to x'). When x∉S, it means the sentence corresponding to x is independent of S (i.e. S neither proves nor disproves it).


In some sense, it would make sense to call the set S (along with the statements encoded) as a "logical theory". But that would be an overloading of similar terms (and cause some confusion).

Nevertheless, while this kind of representation has many limitations [some which I understand, and many which I don't], it is reasonably useful an initial guide (and sometimes later too).

It does help understand some aspects like consistency and numbering of sentences. [it also helps a bit in seeing (the outline) how halting problem would imply the first incompleteness theorem (soundness version) ....... though the specific corollary of incompleteness theorem is different]
 
Last edited:
  • #29
Stephen Tashi
Science Advisor
7,412
1,386
What about these:
https://en.wikipedia.org/wiki/Unrestricted_grammar

I already mentioned them in post#11. Wouldn't these closely correspond to what you are calling formal system.
I'll have to think about that. But this widens the topic. My main question is how to form examples in mathematical logic based on things familiar to people who program computers, but have not necessarily taken courses in Computer Science.

People who take theoretical courses in computer science know about Turing machines and other abstract structures. That type of person can appreciate an example where a Turing machine or an abstract model of computation is involved.
 
  • #30
449
51
My main question is how to form examples in mathematical logic based on things familiar to people who program computers, but have not necessarily taken courses in Computer Science.
As I mentioned in post#5, just having some familiarity with notion of a "program" is enough to understand elementary (but also important) theorems in recursion theory.

I don't know whether this helps or not, but here is an implementation of a universal program I wrote four years ago or so (the upload date is about two years later). Maybe someone would find it useful. For example, I have seen some discussions whether a full implementation should be used in a basic course or not. I don't know about that. However one thing to mention is that even though it looks quite long, but it didn't take me more than two weeks or so to write all of this (because if you read it carefully, you will notice that it is simple).

Now it doesn't seem to me that this teaches any "real world programming" of course [or at least, I am no good at it in any case], but that wouldn't be the purpose either. Now one might say, why not have lists already included in basic constructs? Well it is arguable of course.

Please note that there are probably a few (minor quite likely) mistakes in the detailed implementation. I did check and correct a lot of mistakes (a few still remain I think), but I haven't taken a look at it for few years now.

description
implementation

==============================

The computational model for which universal program is written is defined by following commands:
temporary variables: t1,t2,t3,t4,......
input variables: x1,x2,x3,x4,......
output variable: y

commands (v,w below are variables):
v=0
v=v+1
while(v!=w)
End

!= simply means "not equal". End is just a replacement for (ending) brackets. Also = means assignment (":=" that is).

==============================

Now the program model above is sufficiently strong to calculate any partial computable k-ary function ##\mathbb{N}^k \rightarrow \mathbb{N}##. The reason why further features can be simulated in this basic program is simply due to variable re-naming [along with an understanding what segment of commands will be enough to replace every occurrence of some new construct ...... I went through it quite briefly for most additional constructs].

There are some conventions I used implicitly (without explaining). Every variable is assumed to be local to the specific function it used in by default (so there is no possibility of a variable referring to anything else outside the specific function it is used in). Initial declaration for variables are skipped i.e. not required/allowed. Default initial values for variables are 0. The naming conventions for input and output variables remain the same for every function [x,x1,x2,.... etc. for input and y for output]. Also, in the "description" document (in A3), I used the phrase "call hierarchy". But a more suitable description one would be "call dependence in text of program".

The universal program was written in a computation model with facility of sub-routines/functions added (along with conditionals and one or two more additions) [the constructs in A7 aren't used in the implementation]. One difference is that instead of prime-factorization for encoding, I used repeated applications of an "encode" function [of course this is also a well-known alternative method].

For example, the encode function (of two variables) can be visualized as follows:

90919293949596979899
7273747576777879
80
89
565758
59
6061626371
88
424344454647485570
87
303132333435
41
546986
202122232429405368
85
12131415192849526784
6
7
8111827385166
83
235
10
172637506582
0149162536496481

e.g. we have:
encode(0,0)=0, first(0)=0, second(0)=0
encode(1,0)=1, first(1)=1, second(1)=0
encode(0,1)=2, first(2)=0, second(2)=1
encode(1,1)=3, first(3)=1, second(3)=1
encode(2,4)=22, first(22)=2, second(22)=4
and so on......



Note:
If we choose to, we can also work with strings (with the character set being the same as one in which we write our programs). Then if we think of an arbitrary program as calculating a function ##S^n \rightarrow S## [##S## is set of all finite strings over the given characters and ##n## is a positive natural number] then a universal program for program computing functions of one variable has a very natural definition.

The universal program (from ##S^2## to ##S##) simply takes the text of any program computing a unary function (from ##S## to ##S##) along with the input string and simulates it exactly. So it halts iff the original program halts on same input and gives the same output upon halting.

It could also work in the same way as above (as described for natural numbers). We first define a very basic model with few commands. And then the universal program can be built using a computational model with few basic features added (for ease and to avoid repetition) on top of the primitive one.
 
Last edited:
  • Like
Likes Jarvis323
  • #31
109
30
Summary:: For the purposes of teaching topics in mathematical logic, how can we make examples based on a computer language?
I more than suspect that I'm way out of my league here, but did you consider functional languages like for instance Miranda? I'd expect such languages to convey mathematics and logic better than a messy "structured" language like C.
Regards.
 
  • #32
Stephen Tashi
Science Advisor
7,412
1,386
I don't know whether this helps or not, but here is an implementation of a universal program
I'm not familiar with the terminology "universal program". Does that mean an implementation of a "universal Turing machine"?
 
  • #33
449
51
Yes, pretty much. So, for example, I considered the universal program for the "primitive model" I described (with four basic commands) [described in a model where few extra things like macros/conditionals were added for better readability and to avoid too much repetition].
 
  • #34
strangerep
Science Advisor
3,162
996
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?
Are you familiar with Z and Object-Z? They are formal specification languages, built upon the mathematical concepts of sets and mappings. But they're not executable, afaik.
 
  • #35
.Scott
Homework Helper
2,638
965
Summary:: For the purposes of teaching topics in mathematical logic, how can we make examples based on a computer language?
I'm not sure. But let's start out with the recognition that the statements at the core of computer programs are imperative. In contrast, logical statements are declarative. Thus the C statement "A = A && B;" specifies an operation on variable A. Whereas the logical statement "A = A ^ B" is either true or false and is equivalent to "B -> A".

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 logic 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.
It seems to me that by this definition, computer programming languages are "wffs". When the compiler or interpreter processes the symbol string, it will recognize proper syntax or issue an error message. There might be some wiggle room for interpreted languages - because the interpreter might never attempt to fully parse some sections of the code. But in the case of a compiled language, the compiler will either generate object code or issue error messages - an unambiguous indication of whether the syntax has been followed.

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.
I won't claim to be entirely clear on what you are describing, but I believe that we can describe a computer program this way. The notion of true or false is being introduced - it was not mentioned in your definition of "Formal Languages".
As I said before, computer programs are not declarative - they are imperative. When applied to a machine, they cause that machine to yield a result. Starting with a specific computer program (a wff), we can apply specific rules to transform that program into equivalent programs (other wff symbol sets) that will yield those same results. So given that a specific wff is "true", it can be transformed into other wffs that are also "true".

In fact, this operation is routinely performed on computer programs. If you start with a C program and compile it, several operations of this type are performed. First, the programming logic is parsed, categorically tabulated, and analyzed - a process which involves a major change in syntax and potentially changes to the wff imperatives themselves. Then optimizations are applied. This is a very explicit process of transforming the wff into a different but equivalent set of instructions - so a different wff has been formed with rules that assure that this new wff is just as "true" as the original. This optimized code is then provided in a variety of syntactical renditions - a buildable object module, an executable, and perhaps marco-assembly source.

So I would suggest that a computer language - especially in conjunction with functional compilers - could be considered a "Formal System" by your definition.

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 languages 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.
Given how I applied "Formal System" to a computer programing (above), all that needs to be done to meet your "Formal Logic" standard is to introduce the notion of whether a program is "true" or "false". In the case above, I simply presumed the original program (wff) to be True or False. But I believe that extending this to your definition of a "Formal System" leads to the introduction of the concept of "requirements". Given a set of requirements, a computer program can be said to be true (produces the required results) or false (fails to produce the required results). So if the required result is to produce the sequence of numbers that are the first 10,000 prime numbers, then a formal system is defined where any wff can be determined to be either true or false. Similarly, any other well-formed requirements would constitute a new "Formal System".

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.
I agree. C is not a Formal System. It is only a syntax.
 
  • #36
Stephen Tashi
Science Advisor
7,412
1,386
I'm not sure. But let's start out with the recognition that the statements at the core of computer programs are imperative. In contrast, logical statements are declarative. Thus the C statement "A = A && B;" specifies an operation on variable A. Whereas the logical statement "A = A ^ B" is either true or false and is equivalent to "B -> A".
I agree that the nature of imperative statements sets computer languages apart from the types of formal systems that were invented before computers were common.

It seems to me that by this definition, computer programming languages are "wffs".
We have to distinguish between parsers of computer languages versus things related to the execution of their instructions. The terminology "computer language" usually includes both.


When the compiler or interpreter processes the symbol string, it will recognize proper syntax or issue an error message. There might be some wiggle room for interpreted languages - because the interpreter might never attempt to fully parse some sections of the code. But in the case of a compiled language, the compiler will either generate object code or issue error messages - an unambiguous indication of whether the syntax has been followed.
This brings up the distinction between interpreters and compliers. Parsers for compilers recognize only one version of a wff. That version is a complete program. On the way to parsing code for a program they may check that segments of code form special kinds of wffs, such a variable declarations. However, it's hard to make a correspondence between the notion of the many special types of wffs used in parsers with the notion of a single type of wff that is used in formal systems.

The parsing used by interpreters uses a definition of wff that is a more interesting analogy to a formal language than the parsing used by a compiler. I'm glad you brought up interpreters.

I won't claim to be entirely clear on what you are describing, but I believe that we can describe a computer program this way. The notion of true or false is being introduced - it was not mentioned in your definition of "Formal Languages".
Yes, formal languages do not contain any definitions related to the "states" of wffs. There is no requirement that wff can be evaluated as being True or False - or as being 37.6 or the declaration of object.

Formal Systems also don't contain any rules about the "states" of wffs. They contain rules for producing new wffs from given wffs, but they don't contain rules saying how to use a given a"True" wff to produce another "True" wff. The concept of a "True" wff doesn't apply. The notion of "True" has to do with the state of a wff, which is not defined.


Given how I applied "Formal System" to a computer programing (above), all that needs to be done to meet your "Formal Logic" standard is to introduce the notion of whether a program is "true" or "false".
In the case above, I simply presumed the original program (wff) to be True or False. But I believe that extending this to your definition of a "Formal System" leads to the introduction of the concept of "requirements". Given a set of requirements, a computer program can be said to be true (produces the required results) or false (fails to produce the required results). So if the required result is to produce the sequence of numbers that are the first 10,000 prime numbers, then a formal system is defined where any wff can be determined to be either true or false. Similarly, any other well-formed requirements would constitute a new "Formal System".
I'll state the analogy differently.

A parser for a computer language can be regarded as implicitly defining a formal language. I suppose it's the technical documentation for a parser that actually defines the formal language - not the executable code for the parser. In a parser for a compiler, a wff is a valid program. In a parser for an interpreter, a wff is any text that defines an operation the interpreter can execute.

An optimizer for code implicitly defines rules for deriving one valid program in machine code from another valid program in machine code. So the technical description of an optimizer is an example of a Formal System. Similary, a code "clean-up" program that converts valid text for a program in some computer language to valid text for it in the same language implicitly defines a formal system.

If we define a computer program to be "True" if it's execution satisfies some requirements and "False" otherwise, then optimizers and code clean-up programs implicitly define Formal Logics.
 
  • #37
Stephen Tashi
Science Advisor
7,412
1,386
But let's start out with the recognition that the statements at the core of computer programs are imperative. In contrast, logical statements are declarative.
What about this for an aphorism?:

Abstract math deals with "may" and computer programs deal with "must".

Which is to say that mathematics offers many possible ways to proceed from some given inputs. (e.g. from a given wff we may produce another wff, from a given premise we may deduce a particular conclusion.) The executable for a computer program defines how a machine must proceed from a given input. This is true even for computer programs that use pseudo-randomness.
 
  • #38
Stephen Tashi
Science Advisor
7,412
1,386
Are you familiar with Z and Object-Z? They are formal specification languages, built upon the mathematical concepts of sets and mappings. But they're not executable, afaik.
I'm not familiar with Z - or with specification languages in general. Can we make analogy between specification languages and topics that arise in the foundations of math, such as formal logics?
 
  • #39
strangerep
Science Advisor
3,162
996
I'm not familiar with Z - or with specification languages in general. Can we make analogy between specification languages and topics that arise in the foundations of math, such as formal logics?
That's not something I can answer in a short post. Probably best if you google "Introduction to Z". :oldsmile:
 
  • #41
.Scott
Homework Helper
2,638
965
What about this for an aphorism?:

Abstract math deals with "may" and computer programs deal with "must".

Which is to say that mathematics offers many possible ways to proceed from some given inputs. (e.g. from a given wff we may produce another wff, from a given premise we may deduce a particular conclusion.) The executable for a computer program defines how a machine must proceed from a given input. This is true even for computer programs that use pseudo-randomness.
No. Both "may" and "must" are declaratives. Computer programs are "do". They are inherently goal-oriented. It's the difference between me suggesting that a restaurant is good and me telling the restaurant to do a good job.

Or me telling you to work at the restaurant.
Once we define what constitutes "working at a restaurant", then we can determined whether you have achieved the "working at a restaurant" state.
 

Related Threads on Computer languages as examples in formal logic

Replies
1
Views
736
  • Last Post
Replies
6
Views
2K
Replies
14
Views
2K
Replies
7
Views
2K
Replies
0
Views
2K
Replies
3
Views
881
Replies
2
Views
936
  • Last Post
Replies
2
Views
614
  • Last Post
Replies
14
Views
3K
Top