Идея геометрического языка

[caxap]

gris заставил меня мечтать о гемоетрическом языке, чтобы можно было опытно решать/проверять геометрические задачки. Например:
1) Нужна иллюстрация к задачке (мол дан параллелограмм, такие-то точки делят стороны в таком соотношении, такие-то линии, бубубу...): написал эти условия и программа выводит картинку (хотя бы в metapost или postscript, это легче реализовать).
2) Проверить перебором разные случаи, вот шутка от gris'а:

try(10000) {
  eval(max(abs(diff(DQ,QC)))) for config {
    main: circ(0:O; random);
    P(random);
    intercept(tangent(P,main),main):{A,B);
    intercept(line(P;random),main):{C,D};
    intercept(parallel(B,CD),main):E;
    intercept(line(CD),line(EA):Q
  };
  picture(config.last,gif(500,400,72,transparent))
}

3) Опытно решить задачку. Например взять произвольный треугольник, провести медианы и опытно проверить, в каком соотношении деляться медианы. Это пример, а в реальности может понадобится проверить сложную задачку.
...

Я не программист и не представляю как реализовать что-то даже отдалённо напоминающее такой язык, но для профессионалов, я думаю, это будет не так сложно. Может кто-нибудь напишет что-то подобное?

-- Пн сен 27, 2010 19:39:04 --

Т. е. в общем идея языка такая: есть некая доска, типа board. На неё помещаем разные объекты (точки, линии и т. п.). Можно определять их либо произвольно (random), либо явно (координаты и т. п.), либо через уже заданные объекты (напр. точку как пересечение двух прямых).
Затем эту доску можно много раз перерисовать, если есть вызов random, с целью получить какое-то значение (собрать всю статистику или выделить макс., минимальное значение). Можно доску вывести в граф. файл.

[arseniiv]

caxap в сообщении #356716 писал(а):

Т. е. в общем идея языка такая: есть некая доска, типа board. На неё помещаем разные объекты (точки, линии и т. п.). Можно определять их либо произвольно (random), либо явно (координаты и т. п.), либо через уже заданные объекты (напр. точку как пересечение двух прямых).
Затем эту доску можно много раз перерисовать, если есть вызов random, с целью получить какое-то значение (собрать всю статистику или выделить макс., минимальное значение). Можно доску вывести в граф. файл.

Думаю, можно написать программу, реализующую разные геометрические штуки и вывод этой board ещё и прикрутить к ней какой-нибудь язык сценариев, например, Lua, внести в него функции из этой программы, будет самое то. Но сам не возьмусь.

-- Пн сен 27, 2010 23:14:03 --

(А никто не хочет сделать программу для доказательства геометрических теорем? Аксиоматик разных много, какую хочешь выбирай. Кстати, интересно, в Прологе такое можно составить? Вроде можно, но не знаю Пролога и сколько это он будет считать.)

[maxal]

caxap в сообщении #356716 писал(а):

gris заставил меня мечтать о гемоетрическом языке, чтобы можно было опытно решать/проверять геометрические задачки.

см. topic12655.html

[мат-ламер]

maxal в сообщении #356995 писал(а):

caxap в сообщении #356716 писал(а):

gris заставил меня мечтать о гемоетрическом языке, чтобы можно было опытно решать/проверять геометрические задачки.

см. topic12655.html

Это не совсем то. Попробуйте взять систему геометрического моделирования SolidWorks. В нём есть развитая система программирования, использующая геометрические примитивы и отношения.

[caxap]

мат-ламер в сообщении #357072 писал(а):

. Попробуйте взять систему геометрического моделирования SolidWorks.

Да, мы в ней работали в универе -- разрабатывали 3D модель печатной платы. Но уж очень она тяжеловесная и работает только из под виндовса.

maxal в сообщении #356995 писал(а):

см. topic12655.html

Спасибо. Но это не совсем то, что надо. Я имел ввиду язык, чтобы можно было написать прогу, скормить интерпретатору (без всяких ГУИ) и он посчитал нужное. Напр.

board:            # "доска"
  tr = triangle (0,0) (0,10) (5,10)      # создаем треугольник "tr" по трем точкам
  circ = incircle tr        # вписываем окружность "circ"

find:               # "что программа должна найти"
  area circ       # площадь впис. окружности
  area tr         # площадь треугольника
  radius circ     # радиус впис. окружности
  center circ     # центр впис. окружности

plot board metapost "picture.mp"  # рисуем в metapost картинку

-- Вт сен 28, 2010 20:37:31 --

Это лишь простой пример, здесь и вручную можно посчитать. Но если сложная задача (стереометрическая), то имхо такая штука будет полезна.

-- Вт сен 28, 2010 20:42:32 --

Может реализовать как библиотеку к какому-нибудь матпакету (maxima, Mathematica), т.к., по-моему, там придётся иногда непростые уравнения решать (пересечения сложных фигур, площади и т.п.). Тогда надо будет реализовать только "внешнюю" часть, а все расчеты отправить матпакету.

[arseniiv]

Кстати, как-то в Mathematica делал что-то примитивно-геометрическое, надо было только задавать координаты точек, хотел проверить расположение четырёх замечательных точек треугольника; но что-то незаладилось и при решении получались бесконечности, где-то в конце. Искал-искал ошибки, так и не нашёл. Были функции для прямой по двум точкам, точки пересечения прямых, перпендикуляра к прямой через точку, биссектрисы угла по двум прямым (какого-то из двух, точно не помню, какой брался). Может, найду определения.

[Dandan]

arseniiv в сообщении #356731 писал(а):

(А никто не хочет сделать программу для доказательства геометрических теорем? Аксиоматик разных много, какую хочешь выбирай. Кстати, интересно, в Прологе такое можно составить? Вроде можно, но не знаю Пролога и сколько это он будет считать.)

я для курсача пробовал такое сделать на Прологе используя аксиоматику Гильберта. Если для доказательства какого-то утверждения не требуется дополнительных построений, то прога вроде как работала =), правда работать она могла очень долго, так как там мог быть очень очень долгий перебор. Однако, для доказательства даже самых простых геометрических утверждений, в основном требуются дополнительные построения. Короче, такой метод, имхо, бесперспективен.

Для автоматического доказательства теорем геометрии лучше всего использовать алгоритм Тарского.

п.с. вернее нужны не столько дополнительные построения, как рассмотрение дополнительных объектов, которые не участвовали в определении задачи. Скажем, можно сформулировать какое-то утверждение о треугольнике используя вершины A,B,C, а для доказательства придется использовать стороны a,b,c.
Для произвольного утверждения какие доп. объекты вводить и рассматривать - вообще говоря не понятно.

[arseniiv]

1. (* 
2. Неопределяемое: 
3.   P[{x, y}] - точка 
4.   SLine[{x0, y0}, {kx, ky}] - направленная прямая 
5. SLine потому что Line занято, хотя здесь можно было бы и его использовать. 
6. *) 
7.  
8. PV[x_P] := x[[1]] 
9. L0[x_SLine] := x[[1]] 
10. LK[x_SLine] := x[[2]] (* это для удобства *) 
11.  
12. SLine[a_P, b_P] := SLine[PV[a], PV[b] - PV[a]] (* прямая по точкам в направлении второй *) 
13.  
14. ParallelQ[a_SLine, b_SLine] := Abs[LK[a]] == Abs[LK[b]] (* параллельны? *) 
15. CodirectionalQ[a_SLine, b_SLine] := LK[a] == LK[b] (* сонаправлены? *) 
16. AntidirectionalQ[a_SLine, b_SLine] := LK[a] == -LK[b] (* ну ясно *) 
17. PerpendicularQ[a_SLine, b_SLine] := LK[a] . LK[b] == 0 (* тоже ясно) *) 
18.  
19. AngleCos[a_SLine, b_SLine] := (LK[a] . LK[b]) / (Norm[a] Norm[b]) (* косинус угла, не забудем о направленности прямых *) 
20. AngleValue[a_SLine, b_SLine] := ArcCos[AngleCos[a, b]] (* сам угол *) 
21.  
22. P[a_SLine, b_SLine] := LK[a] ((L0[b] - L0[a]) / (LK[a] - LK[b])) + L0[a] (* точка по пересечению прямых *) 
23.  
24. MidPoint[a_P, b_P] := P[(PV[a] + PV[b]) / 2] (* середина отрезка *) 
25. Perpendicular[l_SLine, p_P] := SLine[PV[P], LK[l] . {{0, 1}, {-1, 0}}] (* перпендикулярная прямая через точку *) 
26. Bisectrix[a_SLine, b_SLine] := SLine[P[a, b], LK[a] + LK[b]] (* "биссектрисная прямая" *) 
27. Antidirectional[a_SLine] := SLine[L0[a], -LK[a]] (* прямая с противоположным направлением *) 
28. Len[a_P, b_P] := Norm[b - a] (* расстояние *) 
29.  
30. Unprotect[Times]; (* это всё для красоты, чтобы -SLine[...] дало прямую, направленную противоположно *) 
31. SLine /: Times[-1, a_SLine] := Antidirectional[a] 
32. Protect[Times]; 

Вроде всё подкорректировал правильно. Больше наработок у меня нет.
UPD: Добавил комментарии к этой каше.
UPD2: Как здесь видно, я даже не касался площади фигур, построения окружностей, разных движений. Движения, наверно, наиболее просто сделать. Но т. к. с треугольником даже не всё в порядке получилось, и я не понял, что именно, лучше относиться к этому коду с осторожностью. Может даже, кто-нибудь найдёт здесь ошибки, было бы приятно узнать, где они.

Dandan в сообщении #357106 писал(а):

Для автоматического доказательства теорем геометрии лучше всего использовать алгоритм Тарского.

Не расскажете о нём подробнее? Он основан на его аксиоматике, наверно, да?

[Dandan]

arseniiv в сообщении #357113 писал(а):

Dandan в сообщении #357106 писал(а):

Для автоматического доказательства теорем геометрии лучше всего использовать алгоритм Тарского.

Не расскажете о нём подробнее? Он основан на его аксиоматике, наверно, да?

Я думаю лучше это расскажет Матиясевич =) http://lektorium.tv/course/?id=22752

[4th-otaku]

arseniiv в сообщении #356731 писал(а):

Думаю, можно написать программу, реализующую разные геометрические штуки и вывод этой board ещё и прикрутить к ней какой-нибудь язык сценариев, например, Lua, внести в него функции из этой программы, будет самое то. Но сам не возьмусь.

Если нравится Lua - возможно, есть смысл попробовать добавить нужные функции в GSL Shell?

Цитата:

(А никто не хочет сделать программу для доказательства геометрических теорем? Аксиоматик разных много, какую хочешь выбирай. Кстати, интересно, в Прологе такое можно составить? Вроде можно, но не знаю Пролога и сколько это он будет считать.)

Пролог - не панацея. Существуют и более продвинутые системы.

[arseniiv]

(Оффтоп)

Спасибо за ссылки!