Ищу названия для двух объектов [выводимость, термы]

[arseniiv]

Здесь я кое-что определю с самого нуля, а потом спрошу.

Языком назовём разрешимое подмножество $L$ чего-то фиксированного. Правилом вывода (в $L$) назовём вычислимую функцию $r\colon L_r\to L$, где $L_r\subset L^n$ разрешимо. Системой вывода назовём пару $(L,R)$, где $R$ — конечное множество правил вывода над $L$.

Слово $a\in L$ выводится из (конечного числа) слов $\Gamma\subset L$ в $L$, или $\Gamma\vdash_{(L,R)} a$, если существует вывод $a\in L$ из $\Gamma\subset L$ в $L$ — последовательность слов $u = (u_1,\ldots,u_{n-1},u_n=a)$ такая, что слово по каждому индексу $i$ содержится в $\Gamma$ или получается применением какого-нибудь элемента $R$ к какому-нибудь набору слов, встречающихся в $u$ с индексами меньше $i$.

Теперь будут определения с вопросом.

Пускай существует конечное разрешимое множество $H$ с функцией $\mathsf{arity}\colon H\to\mathbb N$, и для данного языка $L$ существуют вычислимые функции $\mathsf{head}\colon L\to H$, $\mathsf{args}\colon L\to L^*$, $\mathsf{depth}\colon L\to\mathbb N$ где $\mathsf{args}(a)\in L^{\mathsf{arity}(\mathsf{head}(a))}$, $\mathsf{depth}(a) = 0 \Leftrightarrow \mathsf{args}(a) = ()$, $\mathsf{depth}(a) = 1+\max\{\mathsf{depth}(\mathsf{args}(a)[ i ]) : i\in1..\mathsf{arity}(\mathsf{head}(a))\}$, и существует также функция $\mathsf c\colon HL\to L$, где $HL = \{(h,s) : h\in H, s\in L^{\mathsf{arity}(\mathsf{head}(a))}\}$, такая что $\mathsf c(\mathsf{head}(a),\mathsf{args}(a)) = a$, $\mathsf{head}(\mathsf c(h,s)) = h$ и $\mathsf{args}(\mathsf c(h,s)) = s$. Короче говоря, $L$ представляет собой все возможные термы над $H$; из этого также, если я ничего не забыл, должно следовать $\exists h\in H.\;\mathsf{arity}(h) = 0$. Назовём набор из всего этого, а так же и просто $L$, свободным языком над $H$. (1)

Систему вывода $(L,R)$, где $L$ — сводобный язык над $H$, а $R = \{s\mapsto\mathsf c(h,s) : h\in H\}$, назовём… э-э, хотя бы, свободной системой вывода над $H$. (2)

Вопрос, собственно, в наличии канонических распространённых названий для 1 и 2, и, если они есть, самих их.

-- Ср май 20, 2015 00:22:45 --

P. S. $\mathbb N$ везде содержит ноль, хотя индексы там, где они есть, получились 1-based, чего я не люблю, но иначе тут было бы совсем страшно.

-- Ср май 20, 2015 00:30:13 --

P. P. S. Сначала хотел представить (1) в виде набора конечных деревьев с узлами из $h$ и упорядоченными потомками, но забыл, как их определяют проще.

[Xaositect]

(1) эрбрановский универсум(Herbrand universe) или алгебра термов(term algebra).
(2) не видел. Это обычно представляется как рекурсивное определение терма.

[arseniiv]

Вот спасибо!

(Притом про алгебру термов я когда-то слышал, но забыл.)