SVI Добавление кода парсера и интерпретатора

docs/disser_ktn/pub_02.md

@@ -0,0 +1,102 @@
+**Анти-теорема о полноте (привет Гёделю)**
+
+
+**Пусть** Σ — формальная система, конечная по:
+
+
+- множеству аксиом |A| = n \< ∞
+
+- множеству правил вывода |R| = m \< ∞
+
+- длине вывода l ≤ L \< ∞ (максимальное число шагов)
+
+- размеру формулы s ≤ S \< ∞ (максимальная длина строки)
+
+**Тогда** Σ полна и непротиворечива.
+
+
+## **Доказательство**
+
+### **1. Конечность множества утверждений**
+
+Все формулы ограничены длиной S, алфавит конечен → множество всех синтаксически корректных формул **конечно**.
+
+Обозначим: |F| = N \< ∞.
+
+### **2. Перечислимость выводов**
+
+Для каждой формулы f ∈ F можно проверить:
+
+- Является ли f аксиомой? (перебор A, конечный)
+
+- Выводима ли f за ≤ L шагов? (перебор всех последовательностей длины ≤ L, конечный)
+
+Число возможных выводов длины ≤ L: m^L · n — **конечно**.
+
+### **3. Разрешимость**
+
+Для любой формулы f:
+
+- Перебираем все выводы длины ≤ L
+
+- Если найден вывод f — f доказуема (истинна в Σ)
+
+- Если найден вывод ¬f — f опровержима (ложна в Σ)
+
+- Если ни то, ни другое — f **неразрешима в рамках ресурсов**, но не **принципиально недоказуема**
+
+Поскольку перебор конечен, для каждой f результат получается за конечное время.
+
+### **4. Полнота**
+
+Для любой f ∈ F:
+
+- Либо f выводима (истинна)
+
+- Либо ¬f выводима (ложна)
+
+- Либо ни одно не выводимо за ≤ L шагов
+
+Но третий случай — не "недоказуемость", а **ограничение ресурса L**. Увеличим L — получим результат.
+
+В пределе (теоретическом, при L → ∞, но конечном для каждой конкретной f) — каждая f разрешима.
+
+### **5. Непротиворечивость**
+
+Если Σ выводит f и ¬f — это обнаруживается за конечное время (перебор выводов).
+
+Такая Σ бракуется. Работаем только с непротиворечивыми.
+
+
+## **Ключевое отличие от Гёделя**
+
+|  | Гёдель | Антитеорема |
+| :-: | :-: | :-: |
+| Длина вывода | Не ограничена | Ограничена L |
+| Множество формул | Бесконечно (все конечные строки) | Конечно (ограниченные S) |
+| Результат | Существуют недоказуемые истинные | Все разрешимы (при достаточных ресурсах) |
+
+
+## **Интерпретация**
+
+**"Неполнота" Гёделя** — артефакт бесконечности.
+
+**"Полнота" конечной системы** — следствие конечности.
+
+В реальности: L и S огромны, но конечны. Перебор теоретически возможен, практически неосуществим.
+
+Но это **сложность**, не **принципиальная неразрешимость**.
+
+
+## **Следствие для машины Тьюринга**
+
+Конечная МТ (лента ограничена M ячеек, время ограничено T шагов):
+
+- Число состояний: |Q| · M^T · T — конечно
+
+- Либо остановится, либо войдёт в цикл длины ≤ |Q| · M^T
+
+- Цикл обнаруживается за конечное время
+
+**Проблема остановки разрешима** для конечной МТ.
+

lev2/vm/ctx_base/ctx_base.go

@@ -0,0 +1,26 @@
+// package ctx_base -- базовый контекст для всех контекстов
+package ctx_base
+
+import "strings"
+
+// CtxBase -- базовый контекст для всех контекстов
+type CtxBase struct {
+}
+
+// NewCtxBase -- возвращает новый базовый контекст
+func NewCtxBase() *CtxBase {
+	sf := &CtxBase{}
+	return sf
+}
+
+// StripOut -- удаляет из строки все паразитные символы
+func (sf *CtxBase) StripOut(out string) string {
+	out = strings.TrimSuffix(out, "\t")
+	out = strings.TrimSuffix(out, " ")
+	out = strings.TrimPrefix(out, "\t")
+	out = strings.TrimPrefix(out, " ")
+	out = strings.ReplaceAll(out, "\t", " ")
+	out = strings.ReplaceAll(out, "\n", " ")
+	out = strings.ReplaceAll(out, "  ", " ")
+	return out
+}

lev2/vm/ctx_int/ctx_int.go

@@ -0,0 +1,212 @@
+// package ctx_int -- контекст над целочисленным кварком
+package ctx_int
+
+import (
+	"fmt"
+	"log"
+	"strconv"
+	"strings"
+
+	"plt/lev2/vm/ctx_base"
+	"plt/lev2/vm/ctx_int/state_int"
+	"plt/lev2/vm/ctx_int/sym_int"
+	"plt/lev2/vm/pos"
+	"plt/lev2/vm/state_res"
+	"plt/lev2/vm/state_vm"
+)
+
+// IPrcInt -- интерфейс процесса инструкции ВМ
+type IPrcInt interface {
+	// Compile -- компилирует символ
+	Compile(begPosY, begPosX int, lstOut []string) func()
+}
+
+// CtxInt -- контекст над целочисленным значением
+type CtxInt struct {
+	*ctx_base.CtxBase
+	stateInt state_int.IStateInt
+	dictPrc  map[string]IPrcInt
+	vmState  *state_vm.StateVm
+	posCur   pos.IPosMut
+}
+
+var (
+	vmState = state_vm.VM_State
+	posCur  = pos.PosCur
+)
+
+// NewCtxInt -- возвращает новый контекст над целочисленным значением
+func NewCtxInt() *CtxInt {
+	log.Println("NewCtxInt()")
+	sf := &CtxInt{
+		CtxBase: ctx_base.NewCtxBase(),
+	}
+	sf.parse()
+	return sf
+}
+
+// CreateSym-- создает новый целочисленный символ
+func (sf *CtxInt) CreateSym() func() {
+	log.Println("CtxInt.CreatePrc()")
+	p := sym_int.NewSymInt()
+	return p.Run
+}
+
+// Парсит целочисленный контекст
+func (sf *CtxInt) parse() {
+	begPosX := 0
+	begPosY := 0
+	{ // Начать поиск выводимого значения
+		for vmState.StrCur() != "(" {
+			vmState.RuneInc()
+			if vmState.StrCur() == "\n" {
+				posCur.NextLine()
+			}
+			posCur.IncX()
+			begPosY = posCur.GetY()
+		}
+		// Сдвинуть позицию
+		vmState.RuneInc()
+		posCur.IncX()
+		begPosX = posCur.GetX()
+	}
+	out := ""
+	{ // Выбрать значение отладки
+		for vmState.StrCur() != ")" {
+			strCur := vmState.StrCur()
+			if strCur == "\n" {
+				posCur.NextLine()
+			}
+			out += vmState.StrNext()
+			posCur.IncX()
+			if vmState.IsEnd() {
+				break
+			}
+		}
+		vmState.RuneInc() // Сдвиг после скобки
+		out = strings.ReplaceAll(out, "\n\n", "\n")
+		sf.strOut = fmt.Sprintf("%v:%v\t%v", begPosY, begPosX, out)
+	}
+	{ // Теперь надо выяснить операцию
+		out = sf.StripOut(out)
+		lstOut := strings.Split(out, " ")
+		// lenLst := len(lstOut)
+		cmd := lstOut[0]
+		fnRun := sf.dictPrc[cmd].Compile(begPosY, begPosX, lstOut)
+		sf.stateInt.Append(fnRun)
+	}
+	// switch lenLst {
+	// case 3:
+	// 	switch cmd {
+	// 	case "new": // готовит инструкцию создания новой целочисленной переменной
+	// 		sf.compileNew()
+	// 	case "+": // Сложение
+	// 		sf.compileAdd(begPosY, begPosX, lstOut)
+	// 	default:
+	// 		panic("PrcInt(): unknown command for case=3")
+	// 	}
+	// case 2:
+	// 	switch cmd {
+	// 	case "++":
+	// 		sf.compileInc(begPosY, begPosX, lstOut)
+	// 	case "--":
+	// 		sf.compileDec(begPosY, begPosX, lstOut)
+	// 	default:
+	// 		panic("PrcInt(): unknown command for case=2")
+	// 	}
+	// }
+}
+
+// Декремент значения
+func (sf *CtxInt) compileDec(x, y int, lstOut []string) {
+	name := lstOut[1]
+	sf.Run = func() {
+		val := sf.DictRun[name]
+		val--
+		sf.DictRun[name] = val
+		fmt.Printf("%v:%v\ti(-- %v)\t#(val=%v)\n", x, y, name, val)
+	}
+}
+
+// Инкремент значения
+func (sf *CtxInt) compileInc(x, y int, lstOut []string) {
+	name := lstOut[1]
+	sf.Run = func() {
+		val := sf.DictRun[name]
+		val++
+		sf.DictRun[name] = val
+		fmt.Printf("%v:%v\ti(++ %v)\t#(val=%v)\n", x, y, name, val)
+	}
+}
+
+// Складывает два числа
+func (sf *CtxInt) compileAdd(x, y int, lstOut []string) {
+	var err error
+	name1 := lstOut[1]
+	var val1, val2 int
+	isOkName1 := sf.DictCompile[name1]
+	if !isOkName1 {
+		val1, err = strconv.Atoi(name1)
+		if err != nil {
+			err := fmt.Errorf("PrcInt.compileAdd(): in extract op1(%v), err=\n\t%w",
+				name1, err)
+			panic(err)
+		}
+	}
+
+	name2 := lstOut[2]
+	isOkName2 := sf.DictCompile[name2]
+	if !isOkName2 {
+		val2, err = strconv.Atoi(name2)
+		if err != nil {
+			err := fmt.Errorf("PrcInt.cmdAdd(): in extract new val(%v), err=\n\t%w",
+				name2, err)
+			panic(err)
+		}
+	}
+	switch {
+	case isOkName1 && isOkName2:
+		sf.Run = func() {
+			res := val1 + val2
+			vmState.ResRun().Set(state_res.ResTypeInt, res)
+			fmt.Printf("%v:%v\ti(+ %v %v)\t#(val=%v)\n", x, y, name1, name2, res)
+		}
+	case isOkName1 && !isOkName2:
+		sf.Run = func() {
+			val1 := sf.DictRun[name1]
+			res := val1 + val2
+			vmState.ResRun().Set(state_res.ResTypeInt, res)
+			fmt.Printf("%v:%v\ti(+ %v %v)\t#(val=%v)\n", x, y, name1, val2, res)
+		}
+	case !isOkName1 && isOkName2:
+		sf.Run = func() {
+			val2 := sf.DictRun[name2]
+			res := val1 + val2
+			vmState.ResRun().Set(state_res.ResTypeInt, res)
+			fmt.Printf("%v:%v\ti(+ %v %v)\t#(val=%v)\n", x, y, val1, name2, res)
+		}
+	case !isOkName1 && !isOkName2:
+		sf.Run = func() {
+			res := val1 + val2
+			vmState.ResRun().Set(state_res.ResTypeInt, res)
+			fmt.Printf("%v:%v\ti(+ %v %v)\t#(val=%v)\n", x, y, val1, val2, res)
+		}
+	}
+}
+
+// Создаёт новую целочисленную переменную
+func (sf *CtxInt) compileNew(x, y int, lstOut []string) {
+	name := lstOut[1]
+	strVal := lstOut[2]
+	val, err := strconv.Atoi(strVal)
+	if err != nil {
+		err := fmt.Errorf("PrcInt.compileNew(): in extract new val(%v), err=\n\t%w",
+			strVal, err)
+		panic(err)
+	}
+	sf.DictCompile[name] = true
+	sf.Run = func() {
+		sf.DictRun[name] = val
+		fmt.Printf("%v:%v\ti(New %v %v)\n", x, y, name, val)
+	}
+}

lev2/vm/ctx_int/prc_int_dec/prc_int_dec.go

@@ -0,0 +1,7 @@
+// package prc_int_dec -- процесс декремента целого
+package prc_int_dec
+
+// PrcIntDec -- процесс декремента целого
+type PrcIntDec struct {
+	Run func() // Run -- запускает процесс (над целым числом)
+}

lev2/vm/ctx_int/state_int/state_int.go

@@ -0,0 +1,26 @@
+// package state_int -- состояние ВМ для целых чисел
+package state_int
+
+import (
+	"log"
+)
+
+// IStateInt -- интерфейс состояния ВМ для целых чисел
+type IStateInt interface {
+}
+
+// stateInt -- состояние ВМ для целых чисел
+type stateInt struct {
+	dictRun     map[string]int  // Словарь переменных времени исполнения
+	dictCompile map[string]bool // Словарь имён времени компиляции
+}
+
+// NewStateInt -- возвращает новый статус ВМ для целых чисел
+func NewStateInt() IStateInt {
+	log.Println("NewStateInt()")
+	sf := &stateInt{
+		dictRun:     make(map[string]int),
+		dictCompile: make(map[string]bool),
+	}
+	return sf
+}

lev2/vm/prc_int/prc_int.go → lev2/vm/ctx_int/sym_int/sym_int.go

@@ -1,5 +1,5 @@
-// package prc_int -- процесс над целочисленным кварком
-package prc_int
+// package sym_int -- символ целого числа
+package sym_int
 
 import (
 	"fmt"
@@ -7,38 +7,27 @@ import (
 	"strconv"
 	"strings"
 
-	"plt/lev2/vm/pos"
-	"plt/lev2/vm/prc_base"
+	"plt/lev2/vm/ctx_base"
 	"plt/lev2/vm/state_res"
-	"plt/lev2/vm/state_vm"
 )
 
-// PrcInt -- процесс над целочисленным значением
-type PrcInt struct {
-	prc_base.PrcBase
+// SymInt -- символ целого числа
+type SymInt struct {
+	ctx_base.CtxBase
 	strOut string
 	Run    func() // Run -- запускает процесс (над целым числом)
 }
 
-var (
-	// DictRun -- словарь переменных времени исполнения
-	DictRun = map[string]int{}
-	// DictCompile -- словарь имён времени компиляции
-	DictCompile = map[string]bool{}
-	vmState     = state_vm.VM_State
-	posCur      = pos.PosCur
-)
-
-// NewPrcInt -- возвращает новый процесс над целочисленным значением
-func NewPrcInt() *PrcInt {
-	log.Println("NewPrcInt()")
-	sf := &PrcInt{}
+// NewSymInt -- возвращает новый символ целого числа
+func NewSymInt() *SymInt {
+	log.Println("NewSymInt()")
+	sf := &SymInt{}
 	sf.parse()
 	return sf
 }
 
 // Парсит инструкции, вырезает действие
-func (sf *PrcInt) parse() {
+func (sf *SymInt) parse() {
 	begPosX := 0
 	begPosY := 0
 	{ // Начать поиск выводимого значения
@@ -102,7 +91,7 @@ func (sf *PrcInt) parse() {
 }
 
 // Декремент значения
-func (sf *PrcInt) compileDec(x, y int, lstOut []string) {
+func (sf *SymInt) compileDec(x, y int, lstOut []string) {
 	name := lstOut[1]
 	sf.Run = func() {
 		val := DictRun[name]
@@ -113,7 +102,7 @@ func (sf *PrcInt) compileDec(x, y int, lstOut []string) {
 }
 
 // Инкремент значения
-func (sf *PrcInt) compileInc(x, y int, lstOut []string) {
+func (sf *SymInt) compileInc(x, y int, lstOut []string) {
 	name := lstOut[1]
 	sf.Run = func() {
 		val := DictRun[name]
@@ -124,7 +113,7 @@ func (sf *PrcInt) compileInc(x, y int, lstOut []string) {
 }
 
 // Складывает два числа
-func (sf *PrcInt) compileAdd(x, y int, lstOut []string) {
+func (sf *SymInt) compileAdd(x, y int, lstOut []string) {
 	var err error
 	name1 := lstOut[1]
 	var val1, val2 int
@@ -179,7 +168,7 @@ func (sf *PrcInt) compileAdd(x, y int, lstOut []string) {
 }
 
 // Создаёт новую целочисленную переменную
-func (sf *PrcInt) compileNew(x, y int, lstOut []string) {
+func (sf *SymInt) compileNew(x, y int, lstOut []string) {
 	name := lstOut[1]
 	strVal := lstOut[2]
 	val, err := strconv.Atoi(strVal)

lev2/vm/pos/pos.go

@@ -35,7 +35,7 @@ type pos struct {
 }
 
 // NewPos -- возвращает новую позицию в коде
-func NewPos(x, y int) *pos {
+func NewPos(x, y int) IPosMut {
 	return &pos{x, y}
 }
 

lev2/vm/prc_base/prc_base.go

@@ -1,20 +0,0 @@
-// package prc_base -- базовый процесс для всех процессов
-package prc_base
-
-import "strings"
-
-// PrcBase -- базовый процесс для всех процессов
-type PrcBase struct {
-}
-
-// StripOut -- удаляет из строки все паразитные символы
-func (sf *PrcBase) StripOut(out string) string {
-	out = strings.TrimSuffix(out, "\t")
-	out = strings.TrimSuffix(out, " ")
-	out = strings.TrimPrefix(out, "\t")
-	out = strings.TrimPrefix(out, " ")
-	out = strings.ReplaceAll(out, "\t", " ")
-	out = strings.ReplaceAll(out, "\n", " ")
-	out = strings.ReplaceAll(out, "  ", " ")
-	return out
-}

lev2/vm/prc_res/prc_res.go

@@ -7,16 +7,16 @@ import (
 	"strconv"
 	"strings"
 
+	"plt/lev2/vm/ctx_base"
+	"plt/lev2/vm/ctx_int"
 	"plt/lev2/vm/pos"
-	"plt/lev2/vm/prc_base"
-	"plt/lev2/vm/prc_int"
 	"plt/lev2/vm/state_res"
 	"plt/lev2/vm/state_vm"
 )
 
 // PrcRes -- обработка результата
 type PrcRes struct {
-	prc_base.PrcBase
+	ctx_base.CtxBase
 	Run func() // Функция процесса инструкций ВМ
 }
 
@@ -83,7 +83,7 @@ func (sf *PrcRes) parse() {
 // Готовит инструкцию присвоения целочисленного значения
 func (sf *PrcRes) compileInt(x, y int, op1 string) {
 	// Проверить на наличие имени
-	_, isOk := prc_int.DictCompile[op1]
+	_, isOk := ctx_int.DictCompile[op1]
 	{ // Если это значение
 		if !isOk { // Проверяем на число
 			val, err := strconv.Atoi(op1)
@@ -110,9 +110,9 @@ func (sf *PrcRes) compileInt(x, y int, op1 string) {
 				err := fmt.Errorf("PrcRes.compileInt(): for name(%v),  resType=%v, not int", op1, resType)
 				panic(err)
 			}
-			val := prc_int.DictRun[op1]
+			val := ctx_int.DictRun[op1]
 			val = vmState.ResRun().Get().(int)
-			prc_int.DictRun[op1] = val
+			ctx_int.DictRun[op1] = val
 			fmt.Printf("%v:%v\tr(%v)\t#(val=%v)\n", x, y, op1, val)
 		}
 	}

lev2/vm/state_vm/state_vm.go

@@ -2,6 +2,7 @@
 package state_vm
 
 import (
+	"plt/lev2/vm/pos"
 	"plt/lev2/vm/state_res"
 	"strings"
 )
@@ -13,6 +14,7 @@ type StateVm struct {
 	indRune  int                 // Указатель на текущую руну в промежуточном языке
 	resComp  *state_res.StateRes // Результат при компиляции
 	resRun   *state_res.StateRes // Результат при исполнении
+	posCur   pos.IPosMut        // Текущая позиция
 
 }
 
@@ -20,6 +22,7 @@ var (
 	VM_State = &StateVm{
 		resComp: state_res.NewStateRes(),
 		resRun:  state_res.NewStateRes(),
+		posCur:  pos.PosCur,
 	}
 )
 
@@ -51,7 +54,14 @@ func (sf *StateVm) IndRune() int {
 
 // StrCur - литера по текущемй индексу
 func (sf *StateVm) StrCur() string {
-	return string(sf.codeRune[sf.indRune])
+	out := ""
+	for _, indRune := range sf.codeRune {
+		if indRune == '(' {
+			break
+		}
+		out += string(indRune)
+	}
+	return out
 }
 
 // StrNext -- возвращает следующую литеру

lev2/vm/vm.go

@@ -7,19 +7,25 @@ import (
 	"os"
 
 	// "plt/lev0/spec"
+	"plt/lev2/vm/ctx_int"
 	"plt/lev2/vm/pos"
 	"plt/lev2/vm/prc_comment"
 	"plt/lev2/vm/prc_debug"
-	"plt/lev2/vm/prc_int"
 	"plt/lev2/vm/prc_res"
 	"plt/lev2/vm/state_vm"
 )
 
 // Vm -- интерпретатор промежуточного языка
 type Vm struct {
-	lstPrc []func() // Функция процесса инструкций ВМ
+	lstPrc []func()        // Функция процесса инструкций ВМ
+	ctxInt *ctx_int.CtxInt // Контекст целых чисел
 }
 
+var (
+	vmState = state_vm.VM_State // Статус ВМ
+	posCur  = pos.PosCur        // Текущая позиция в коде
+)
+
 // NewVm -- возвращает новый интерпретатор промежуточного языка
 func NewVm() *Vm {
 	log.Println("NewVm()")
@@ -36,8 +42,8 @@ func NewVm() *Vm {
 	}
 	sf := &Vm{
 		lstPrc: []func(){},
+		ctxInt: ctx_int.NewCtxInt(),
 	}
-	vmState := state_vm.VM_State // Статус ВМ
 	vmState.CodeStrSet(string(binCode))
 	sf.parse() // парсинг кода, заполнение структуры s
 	return sf
@@ -45,10 +51,7 @@ func NewVm() *Vm {
 
 // Парсит код на промежуточном языке
 func (sf *Vm) parse() {
-	vmState := state_vm.VM_State // Статус ВМ
 	log.Printf("Vm.parse(): len=%v,\n", vmState.RuneLen())
-	posCur := pos.PosCur // Текущая позиция в коде
-	fmt.Println("")
 	for vmState.RuneLen() > vmState.IndRune() {
 		r := vmState.StrCur()
 		// fmt.Printf("%v", string(r))
@@ -57,13 +60,13 @@ func (sf *Vm) parse() {
 			vmState.RuneInc()
 			prcComment := prc_comment.NewPrcComment()
 			sf.lstPrc = append(sf.lstPrc, prcComment.Run)
-		case "d": // Поиск отладки
+		case "debug": // Поиск отладки
 			prcDebug := prc_debug.NewPrcDebug()
 			sf.lstPrc = append(sf.lstPrc, prcDebug.Run)
-		case "i": // Поиск операции с целым числым
-			prcInt := prc_int.NewPrcInt()
-			sf.lstPrc = append(sf.lstPrc, prcInt.Run)
-		case "r": // Установка результата
+		case "int": // Поиск операции с целым числым
+			symInt := sf.ctxInt.CreateSym()
+			sf.lstPrc = append(sf.lstPrc, symInt.Run)
+		case "reg": // Установка результата
 			prcRes := prc_res.NewPrcRes()
 			sf.lstPrc = append(sf.lstPrc, prcRes.Run)
 		case "\n": // Поиск перевода строки

plt/main.pli

@@ -5,9 +5,9 @@
 
 	игнорируются)
 
-d(Программа запущена)
+debug(Программа запущена)
 
-d(А тут
+debug(А тут
 
 	вывод
 
@@ -17,17 +17,17 @@ d(А тут
 	мы это можем
 )
 
-i(New
+int(new
 	ябл 23)
 
-i(++ ябл)
-i(++ ябл)
-i(-- ябл)
+int(++ ябл)
+int(++ ябл)
+int(-- ябл)
 #(Далее операции без присвоения)
-i(+ ябл 10)
-i(+ 20 ябл)
-i(+ 45 10)
+int(+ ябл 10)
+int(+ 20 ябл)
+int(+ 45 10)
 #(Установить результат как значение яблока,
 	если не имя, то устанавливается результат)
-r(ябл)
-r(-10)
+res(ябл)
+res(-10)