3
$\begingroup$

I have been working in the Welder theorem prover for some time now. But I'm confused in the way they handle data-types. I'm not familiar with the terminology of sorts and constructors. Here is how one defines a list data-type in the system:

val list = mkSort("A")(Seq(cons, nil))
val nil = mkConstructor("A")(Some(list))(_ => Seq())
val cons = mkConstructor("A")(Some(list)) { case Seq(aT) =>
  Seq((head, aT), (tail, list(aT)))
}

So essentially one defines a sort for the abstract class list and then instantiates this sort with concrete classes or constructors. My question is where does this terminology come from?

To finish, would you have an idea how can I model a mathematical field using this notation? I tried:

  val element = mkSort(Seq(zero, one, notZeroOne))
  val zero = mkConstructor(Some(element)) {_ => Seq()}
  val oneADT = mkConstructor(oneID)()(Some(element)) {_ => Seq()}
  val notZeroOneADT = mkConstructor(Some(element)) {_ => Seq()}

But this says that an element has zero, one or a non-zero and not-one element. Someone suggested me to use a natural index as identifier but this would limit me to countable fields.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.