Jestem na następującym ćwiczeniu w zakresie podstaw oprogramowania :
(** **** Exercise: 2 stars (baz_num_elts) *)
(** Consider the following inductive definition: *)
Inductive baz : Type :=
| x : baz -> baz
| y : baz -> bool -> baz.
(** How _many_ elements does the type [baz] have?
(* FILL IN HERE *)
[] *)
Wszystkie odpowiedzi, które widziałem w Internecie, mówią, że odpowiedź to 2, a elementy to xiy. Jeśli tak jest, to nie jest dla mnie jasne, co oznaczają elementy . Z pewnością istnieją dwa konstruktory, ale nie można w rzeczywistości utworzyć wartości typu baz .
Nie można utworzyć wartości typu, baz
ponieważ x
ma ona typ baz -> baz
. y
ma typ baz -> bool -> baz
. W celu uzyskania wartości typu baz
musimy przekazać wartość typu baz
albo x
albo y
. Nie możemy uzyskać wartości typu, baz
jeśli nie mamy już wartości typu baz
.
Do tej pory interpretowałem elementy jako wartości średnie . Tak więc (cons nat 1 nil)
i (cons nat 1 (cons nat 2 nil))
oba byłyby elementami typu list nat
i byłaby nieskończona liczba elementów typu list nat
. Byłyby dwa elementy typu bool
, które są true
i false
. Zgodnie z tą interpretacją twierdziłbym, że nie ma elementów typu zero baz
.
Czy mam rację, czy ktoś może wyjaśnić to, co źle zrozumiałem?
baz
.baz
.Odpowiedzi:
Zgadzam się z Tobą. Istnieje bijection między
baz
iFalse
.źródło