LARGE-SIZE MESSAGE CONSTRUCTION FOR ETI Non-deterministic typing and symbolic computation in LINCOS

摘要

The problem of constructing messages for ETI concerned with mathematical modelling of physical phenomena is considered. The Lingua Cosmica (LINCOS) for interstellar communication advocated by the present author in a number of papers, is based on constructive logic. Therefore the primary purpose of using UNCOS in message construction is to achieve guaranteed correct logical reasoning. The Lingua Cosmica in pure form is, however, not immediately applicable for describing mathematical modelling of physical reality because it has only limited computational power. The present paper discusses a slight modification to the underlying logic, introducing some aspects of computational nature. At the same time the concept of strict typing in constructive logic is modified by introducing non-determinism in definitions. The way these new elements can be put to use is illustrated by showing how the basics of Einstein's Special Relativity Theory (SRT) can be formulated in logic terms.