feat: Remove period support from formal notation

docs/mts/formal-notation.md

@@ -46,7 +46,7 @@
 
 ```ebnf
 File      = { Stmt } ;
-Stmt      = Expr , "." ;
+Stmt      = Expr , [ "," ] ;  (* comma separator is optional *)
 
 Expr      = DefExpr | EqExpr | NeqExpr | Term ;
 
@@ -100,9 +100,9 @@ Ctx       = "[" , AbitSeq , "]" ;
 У тебя явно зафиксированы: ориентированность, единственность, порождение равенства, guarded recursion.
 
 ```mts
-(s : F) != (F : s).
-(s : F) : (s = F).
-{ s : F, s : G } : (F = G).
+(s : F) != (F : s)
+(s : F) : (s = F)
+{ s : F, s : G } : (F = G)
 ```
 
 > Заметь: это ровно твой тезис “`:` и `=` — разные онтологические категории, но `:` порождает `=`”. 
@@ -112,20 +112,20 @@ Ctx       = "[" , AbitSeq , "]" ;
 Ты формулируешь её как “равенство сложных сводится к равенству компонентов” и даёшь схемы через `{…}`.
 
 ```mts
-((a -> b) = (c -> d)) : { a = c, b = d }.
-{ a = c, b = d } : ((a -> b) = (c -> d)).
+((a -> b) = (c -> d)) : { a = c, b = d }
+{ a = c, b = d } : ((a -> b) = (c -> d))
 
-(♂a = ♂b) : (a = b).
-(a = b) : (♂a = ♂b).
+(♂a = ♂b) : (a = b)
+(a = b) : (♂a = ♂b)
 
-(a♀ = b♀) : (a = b).
-(a = b) : (a♀ = b♀).
+(a♀ = b♀) : (a = b)
+(a = b) : (a♀ = b♀)
 
-(¬a = ¬b) : (a = b).
-(a = b) : (¬a = ¬b).
+(¬a = ¬b) : (a = b)
+(a = b) : (¬a = ¬b)
 
-(!a = !b) : (a = b).
-(a = b) : (!a = !b).
+(!a = !b) : (a = b)
+(a = b) : (!a = !b)
 ```
 
 ### 3.3 Кванторы форм: `∞`, `♂`, `♀`, `->`
@@ -134,20 +134,20 @@ Ctx       = "[" , AbitSeq , "]" ;
 “Фундаментальная теорема” про `r -> v : (r -> v)` тоже есть. 
 
 ```mts
-∞ : (∞ -> ∞).
+∞ : (∞ -> ∞)
 
-♂x : (♂x -> x).
-x♀ : (x -> x♀).
+♂x : (♂x -> x)
+x♀ : (x -> x♀)
 
-(r -> v) : (r -> v).
+(r -> v) : (r -> v)
 ```
 
 А “уникальность” акорня ты формулируешь как эквивалентность `x = (x -> x)` и `x = ∞`.
 Без введения отдельного `⇔` даём как две направленные аксиомы через `:`:
 
 ```mts
-(x = (x -> x)) : (x = ∞).
-(x = ∞) : (x = (x -> x)).
+(x = (x -> x)) : (x = ∞)
+(x = ∞) : (x = (x -> x))
 ```
 
 ### 3.4 Инверсия направления `¬` (замена твоего `-`)
@@ -157,14 +157,14 @@ x♀ : (x -> x♀).
 Чтобы не повторить внутреннюю несогласованность “и просто переворот, и совместимость”, фиксирую **одну когерентную схему**: инверсия переворачивает связь и рекурсивно применяется к компонентам (контравариантно):
 
 ```mts
-¬(a -> b) : (¬b -> ¬a).
-¬(a !-> b) : (¬b !-> ¬a).
+¬(a -> b) : (¬b -> ¬a)
+¬(a !-> b) : (¬b !-> ¬a)
 
-¬(♂x) : (x♀).
-¬(x♀) : (♂x).
-¬∞ : ∞.
+¬(♂x) : (x♀)
+¬(x♀) : (♂x)
+¬∞ : ∞
 
-¬¬x = x.
+¬¬x = x
 ```
 
 ### 3.5 Несвязь `!->` и смысловая дуальность `!`, `0/1`
@@ -175,23 +175,23 @@ x♀ : (x -> x♀).
 Делаем `!->` определением “негации связи”:
 
 ```mts
-!(a -> b) : (a !-> b).
-!(a !-> b) : (a -> b).
+!(a -> b) : (a !-> b)
+!(a !-> b) : (a -> b)
 
-!!x = x.
+!!x = x
 ```
 
 Определяем `1` как “единицу смысла” (у тебя это `♂∞ -> ∞♀`).
 
 ```mts
-1 : (♂∞ -> ∞♀).
+1 : (♂∞ -> ∞♀)
 ```
 
 А `0` задаём как дуал `1` через `!` (и тем самым выполняем твои пункты 4–5):
 
 ```mts
-!1 : 0.
-!0 : 1.
+!1 : 0
+!0 : 1
 ```
 
 (Отсюда, через “(s:F) : (s = F)” + симметрию равенства в ядре прувера, получатся привычные записи `0 = !1`, `1 = !0`.)
@@ -203,17 +203,17 @@ x♀ : (x -> x♀).
 Фиксируем новую пару:
 
 ```mts
-[ : (♂∞ -> ∞).
-] : (∞ -> ∞♀).
+[ : (♂∞ -> ∞)
+] : (∞ -> ∞♀)
 ```
 
 ### 3.7 Акс. левоассоциативности цепочек
 
 У тебя это отдельный “онтологический принцип группировки”.
 
 ```mts
-(a -> b -> c) = ((a -> b) -> c).
-(a -> (b -> c)) != ((a -> b) -> c).
+(a -> b -> c) = ((a -> b) -> c)
+(a -> (b -> c)) != ((a -> b) -> c)
 ```
 
 ---

docs/mts/specification-v0.1.md

@@ -67,7 +67,7 @@ EBNF:
 
 File      ::= { Stmt } ;
 
-Stmt      ::= Expr "." ;
+Stmt      ::= Expr [ "," ] ;  // comma separator is optional
 
 Expr      ::= DefExpr
             | EqExpr

examples/basic.mtl

@@ -8,32 +8,32 @@
 // ========================================
 
 // Тождественность акорня самому себе
-∞ = ∞.
+∞ = ∞
 
 // Акорень равен связи с самим собой
-∞ = ∞ -> ∞.
+∞ = ∞ -> ∞
 
 // ========================================
 // А5. Самозамыкание начала
 // ♂x : (♂x -> x)
 // ========================================
 
 // Мужской оператор определяет самозамыкание начала
-♂v = ♂v -> v.
+♂v = ♂v -> v
 
 // Вложенность мужского оператора
-♂♂v = ♂♂v -> ♂v.
+♂♂v = ♂♂v -> ♂v
 
 // ========================================
 // А6. Самозамыкание конца
 // x♀ : (x -> x♀)
 // ========================================
 
 // Женский оператор определяет самозамыкание конца
-r♀ = r -> r♀.
+r♀ = r -> r♀
 
 // Вложенность женского оператора
-r♀♀ = r♀ -> r♀♀.
+r♀♀ = r♀ -> r♀♀
 
 // ========================================
 // А7. Аксиома инверсии
@@ -42,57 +42,57 @@ r♀♀ = r♀ -> r♀♀.
 // ========================================
 
 // Инверсия мужского оператора
-!♂x = x♀.
+!♂x = x♀
 
 // Инверсия женского оператора
-!x♀ = ♂x.
+!x♀ = ♂x
 
 // Инверсия акорня
-!♂∞ = ∞♀.
-!∞♀ = ♂∞.
+!♂∞ = ∞♀
+!∞♀ = ♂∞
 
 // ========================================
 // А11. Левоассоциативность связи
 // (a -> b -> c) = ((a -> b) -> c)
 // ========================================
 
 // Цепочка связей левоассоциативна
-a -> b -> c = (a -> b) -> c.
+a -> b -> c = (a -> b) -> c
 
 // Более длинная цепочка
-a -> b -> c -> d = ((a -> b) -> c) -> d.
+a -> b -> c -> d = ((a -> b) -> c) -> d
 
 // ========================================
 // Степенной оператор
 // a^n разворачивается в n применений связи
 // ========================================
 
 // a^2 = (a -> a)
-a^2 = a -> a.
+a^2 = a -> a
 
 // a^3 = ((a -> a) -> a)
-a^3 = (a -> a) -> a.
+a^3 = (a -> a) -> a
 
 // a^4 = (((a -> a) -> a) -> a)
-a^4 = ((a -> a) -> a) -> a.
+a^4 = ((a -> a) -> a) -> a
 
 // ========================================
 // Комбинированные выражения
 // ========================================
 
 // Применение ♂ к ∞
-♂∞ = ♂∞ -> ∞.
+♂∞ = ♂∞ -> ∞
 
 // Применение ♀ к ∞
-∞♀ = ∞ -> ∞♀.
+∞♀ = ∞ -> ∞♀
 
 // Комбинация ♂ и ♀
-♂∞♀ = (♂∞)♀.
+♂∞♀ = (♂∞)♀
 
 // ========================================
 // Неравенства
 // ========================================
 
 // Различные выражения не равны
-♂∞♀ != ∞.
-♂∞ != ∞♀.
+♂∞♀ != ∞
+♂∞ != ∞♀

examples/test-issue-48-error.mtl

@@ -2,21 +2,21 @@
 // Примеры аксиом и формул
 
 // А4. Смысл (акорень): ∞ : (∞ -> ∞)
-∞ = ∞ -> ∞.
+∞ = ∞ -> ∞
 
 // А5. Самозамыкание начала: ♂x : (♂x -> x)
-♂v = ♂v -> v.
+♂v = ♂v -> v
 
 // А6. Самозамыкание конца: x♀ : (x -> x♀)
-r♀ = r -> r♀.
+r♀ = r -> r♀
 
 // А7. Инверсия
-!♂x = x♀.
-!x♀ = ♂x.)   // тут некорректная закрывающая скобка
+!♂x = x♀
+!x♀ = ♂x)   // тут некорректная закрывающая скобка
 
 // А11. Левоассоциативность
-a -> b -> c = (a -> b) -> c.
+a -> b -> c = (a -> b) -> c
 
 // Степени
-a^2 = a -> a.
-a^3 = (a -> a) -> a.
+a^2 = a -> a
+a^3 = (a -> a) -> a

examples/test-issue-48.mtl

@@ -2,21 +2,21 @@
 // Пример из issue #48 с ошибкой парсинга
 
 // А4. Смысл (акорень): ∞ : (∞ -> ∞)
-∞ = ∞ -> ∞.
+∞ = ∞ -> ∞
 
 // А5. Самозамыкание начала: ♂x : (♂x -> x)
-♂v = ♂v -> v.
+♂v = ♂v -> v
 
 // А6. Самозамыкание конца: x♀ : (x -> x♀)
-r♀ = r -> r♀.
+r♀ = r -> r♀
 
 // А7. Инверсия
-!♂x = x♀.
-!x♀ = ♂x.)   // тут некорректная закрывающая скобка
+!♂x = x♀
+!x♀ = ♂x)   // тут некорректная закрывающая скобка
 
 // А11. Левоассоциативность
-a -> b -> c = (a -> b) -> c.
+a -> b -> c = (a -> b) -> c
 
 // Степени
-a^2 = a -> a.
-a^3 = (a -> a) -> a.
+a^2 = a -> a
+a^3 = (a -> a) -> a

experiments/test-error-location.ts

@@ -2,7 +2,7 @@
 import { readFileSync } from 'fs'
 
 const input = readFileSync('examples/test-issue-48-error.mtl', 'utf-8')
 console.log('Input file:')
 console.log(input)
 console.log('\n=== Parsing ===\n')
 
@@ -33,7 +33,12 @@
 
   console.log('\nError context:')
   console.log('Line', errorLine + 1, ':', lines[errorLine])
-  console.log('Error at column', errorCol, '-> character:', JSON.stringify(lines[errorLine][errorCol]))
+  console.log(
+    'Error at column',
+    errorCol,
+    '-> character:',
+    JSON.stringify(lines[errorLine][errorCol])
+  )
 
   // Show visual pointer
   const pointer = ' '.repeat(errorCol) + '^'