Home

Main pages

• Motivation
• Bigger Examples
• Suslik bugs and limitations

Summary of functional specs status

(summarized from here)

Symbol	Meaning
✔️	Synthesizes apparently correct code
❌	Does not synthesize
❔	Synthesizes "incorrect" code
🔶	Partially working
N/A	See notes

In the directory examples/functional-specs

Name	Status	Notes	Haskell
append.sus	✔️	([1,2,3], [10,100,1000]) ➡️ [1,2,3,10,100,1000]	xs ++ ys
concat.sus	✔️	Flatten a list of lists into a list	concat xs
cons_map.syn	❔	(-23, [[1,2,3], [4,5,6]]) ➡️ [[-23,1,2,3],[-23,4,5,6]]	map (x:)
filter.sus	✔️	Limitation: AbduceBranch only generates the conditions where both lhs and rhs are variables.	filter (>7) xs
fold.sus	✔️	(can only produce a single int) [1,2,3] ➡️ 6	foldr (+) 0 xs
foldMap.sus	✔️	[1,2,3] ➡️ 12	foldr (+) 0 (map (*2) xs)
foldScanr.sus	✔️	Demonstration of composition	sum (scanr (+) 0 xss)
intToNat.sus	N/A	Spec not yet done (ints to unary naturals)	replicate n 0
map-times2.sus	✔️	The code is partially given in the file. Synthesis fills in the hole	map (*2)
map-sum.syn	✔️	[[1,2], [3,4]] ➡️ [3, 7]	map sum xss
map_single.sus	✔️	[1, 2, 3] ➡️ [[1], [2], [3]]	map (:[]) xs
maximum.syn	✔️		maximum xs
maximum_map_sum.syn	❔	Synthesizes "incorrect" code (no summing)	maximum (map sum xss)
maximum_map_sum_seq.sus	✔️	Demonstration of composition	maximum (map sum xss)
min_height.sus	N/A	Spec not yet done
mkSingletonList.sus	✔️	7 ➡️ [7]	x : []
natToInt.sus	✔️	"Unary naturals" to int (essentially a length function, using foldI)	length xs
replicate.sus	✔️	4 ➡️ [7, 7, 7, 7]	replicate n 7
running_sum.sus	🔶	Demonstrates scanr which partially working (see this issue)	scanr (+) 0 xs
self_append.syn	❌	[1,2,3] ➡️ [1,2,3,1,2,3]	xs ++ xs
spatial_append.syn	✔️		xs ++ ys
subseq.sus	✔️	Uses subseq_of predicate. [1,2,3,4] ➡️ [[1,2,3],[1,2],[1,3],[1],[2,3],[2],[3],[]]	foldr (\x xss -> map (x:) ++ xss) [[]]
take.syn	❔	Synthesized code seems incorrect	take n xs
zero-le7.sus	✔️	While this synthesizes something that is spec-correct, its behavior might be unexpected
zip.sus	✔️	([1,2,3], [10,100,1000]) ➡️ [[1,10], [2,100], [3,100]]	zip xs ys
zipWith_add.sus	✔️	([1,2,3], [10,100,1000]) ➡️ [11, 102, 1003]	zipWith (+) xs ys

Structure of "fun-SuSLik" and the intermediate language

Intermediate language

top-level ::= ε | def top-level | ty-decl top-level
n ::= 0 | 1 | 2 | ...
e ::= n | v | let v = e in e | e e | e op e | comb
op ::= + | * | . | ...
args ::= ε | v args
def ::= v args := e | v args := ??
ty-decl ::= v : ty

where the . operator is function composition and comb is the list of combinators and primitives (TODO: Organize):

foldr : (a -> b -> b) -> b -> List a -> b
scanr : (a -> b -> b) -> b -> List a -> List b
map : Functor f => (a -> b) -> f a -> f b
(::) : a -> List a -> List a
[] : List a
fst : Pair a b -> a
snd : Pair a b -> b
pair : a -> b -> Pair a b
dup : a -> Pair a a
swap : Pair a b -> Pair b a
unmaybe : Maybe a -> a -> a
Just : a -> Maybe a
Nothing : Maybe a
uncons : List a -> Maybe (Pair a (List a))
True : Bool
False : Bool
ifThenElse : Bool -> a -> a -> a

Examples translated to "fun-SuSLik"

Status	Haskell	fun-SuSLik	Spec
📖 🔶	xs ++ ys	foldr cons ys xs	foldr f e (app xs ys) = foldr f (foldr f e ys) xs
📖 🔶	map sum	map sum	...
📖 🔶	reverse	...	rev (append xs ys) = append (rev ys) (rev xs) & rev (rev xs) = xs
📖 🔶	sort	...	(srt . srt) = srt & srt = flatten . mkTree
📖 🔶	subseqs	foldr (\x xss -> append (map (cons x) xss) xss) [[]]	implies (ifElemThenBefore x y zs) (all (ifElemThenBefore x y) (subseqs zs))
📖	concat xs	foldr append [] xs
📖	filter (>7) xs	foldr (\x acc -> ifThenElse (x > 7) (x :: acc) acc) [] xs
📖	sum xs	foldr (+) 0 xs