Questions tagged [recursion]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
3 votes
0 answers
46 views

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. https://leetcode.com/problems/diameter-of-binary-tree/...
Hath995's user avatar
  • 131
0 votes
2 answers
233 views

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
91 views

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
270 views

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
109 views

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