Полиморфное пустое отношение в сплаве?

Question

я запускаю команду сплава, который включает в себя поиск свидетелей для некоторых экзистенциалов, как этот:

pred foo { 
    some x, y : E -> E | 
    baz[x,y] || qux[x,y] 
} 

сплава приходит с моделью, в которой foo верно. Я смотрю на модель в Visualizer и обнаруживаю, что y оказывается пустым отношением. Я хочу углубиться в модель и посмотреть, действительно ли baz или qux. Поэтому я запускаю окно Evaluator и набираю baz[$foo_x, ???]. Но что я могу напечатать для ???? Поскольку y пуст, нет переменной с именем $foo_y. И ввод none или {} дает ошибку проверки типа.

Имеет ли сплав пустое отношение, которое может использоваться в любом типе? Или есть ли какой-нибудь способ получить в свидетеле y, хотя он пуст?

Answer 1

I belive baz [$ foo_x, none-> none] должен работать. Соотношение нет имеет значение 1, и с помощью кросс-произведения вы можете получить пустые отношения желаемой ясности. Объяснение этому можно найти в статье «Система типов для объектных моделей» Джонатана Эдвардса, Даниэля Джексона и Эмины Торлак.