Questions tagged [recursion]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
3 votes
0 answers

Verify maximal diameter of a tree in Dafny

I am trying to learn formal methods and have been learning Dafny and practicing by verifying Leetcode problems. I have gotten stuck on this one.
Hath995's user avatar
  • 131
0 votes
2 answers

Is there a multiway system which is equivalent to taking ZFC as axioms?

My understanding is that Stephen Wolfram's concept of a multiway system begins with certain rules and then generates all possible combinations of those rules. There are many distinct mathematical ...
Julius Hamilton's user avatar
1 vote
2 answers

Defining a Recursive Function decreasing on one argument with < and another structurally

I want to define a function which decreases in one argument using < and on another structurally. What is the least painful way to do this? Among the many options (Function, Program Fixpoint, ...
Agnishom Chattopadhyay's user avatar
0 votes
2 answers

What is the meta-language of ZFC?

This is a good post which says that all proof assistants are founded in HOL, first order logic, or dependent types. Does this mean that the axioms of ZFC are just expressions obtainable from the ...
Julius Hamilton's user avatar
2 votes
1 answer

Recursive definition of a sum of squares

I am trying to formalise in Lean3 the notion of sum of squares in a ring. If $ A $ is a ring, $ n $ is an integer and $ f $ is a function from $$ F_n:= \{ i \in \...
Matematiflo's user avatar