Здесь я кое-что определю с самого нуля, а потом спрошу.
Языком назовём разрешимое подмножество

чего-то фиксированного.
Правилом вывода (в

) назовём вычислимую функцию

, где

разрешимо.
Системой вывода назовём пару

, где

— конечное множество правил вывода над

.
Слово
выводится из (конечного числа) слов

в

, или

, если существует
вывод 
из

в

— последовательность слов

такая, что слово по каждому индексу

содержится в

или получается применением какого-нибудь элемента

к какому-нибудь набору слов, встречающихся в

с индексами меньше

.
Теперь будут определения с вопросом.
Пускай существует
конечное разрешимое множество

с функцией

, и для данного языка

существуют вычислимые функции

,

,

где

,

,
![$\mathsf{depth}(a) = 1+\max\{\mathsf{depth}(\mathsf{args}(a)[ i ]) : i\in1..\mathsf{arity}(\mathsf{head}(a))\}$ $\mathsf{depth}(a) = 1+\max\{\mathsf{depth}(\mathsf{args}(a)[ i ]) : i\in1..\mathsf{arity}(\mathsf{head}(a))\}$](https://dxdy-03.korotkov.co.uk/f/e/8/7/e875ce095e2eef79c355dcfb2827f4c782.png)
, и существует также функция

, где

, такая что

,

и

. Короче говоря,

представляет собой все возможные термы над

; из этого также, если я ничего не забыл, должно следовать

. Назовём набор из всего этого, а так же и просто

,
свободным языком над 
. (1)
Систему вывода

, где

— сводобный язык над

, а

, назовём… э-э, хотя бы,
свободной системой вывода над 
. (2)
Вопрос, собственно, в наличии
канонических распространённых названий для 1 и 2, и, если они есть, самих их.
-- Ср май 20, 2015 00:22:45 --P. S.

везде содержит ноль, хотя индексы там, где они есть, получились 1-based, чего я не люблю, но иначе тут было бы совсем страшно.
-- Ср май 20, 2015 00:30:13 --P. P. S. Сначала хотел представить (1) в виде набора конечных деревьев с узлами из

и упорядоченными потомками, но забыл, как их определяют проще.